Sullivan fibre-model theorem (source code)

= Sullivan fibre-model theorem
{c}

For a map $f:E\to B$ with <simply connected> base and the usual finite-type hypotheses, choose a relative Sullivan algebra $M(B)\to M(B)\otimes\Lambda W$ modelling the path-space fibration, with acyclic total algebra. Tensor it over $M(B)$ with a model of $E$ via $f^*$. The resulting algebra models the <homotopy fibre>. Relative Sullivan extensions are cofibrant replacements, so this <tensor product> computes the derived algebraic pushout, contravariantly corresponding to the topological <homotopy pullback>. Linear differential pairs must be cancelled before reading <rational homotopy groups> from generators.