A Serre fibration has the homotopy lifting property for disks: for every , a map and a homotopy starting at its composite with admit a compatible lift . Equivalently, it has that lifting property for CW complexes. Relative lifting for CW pairs follows by attaching cells.
Let be the inclusion of the chosen fiber. The long exact sequence of homotopy groups of a fibration is
Its low-dimensional end is
The maps and are induced by inclusion and projection on based maps; at degree zero they send a path component to its containing or image component. The last part is an exact sequence of pointed sets, not in general a sequence of groups.
For , represent a class by a based cube , constant at on its boundary. Lift it from the constant map on the bottom and side faces, using relative disk lifting. Its top face lands in and is constant on that face's boundary; its class is . The choice of lifts does not change the resulting class. For , lift a based loop starting at and take the path component of its endpoint in . This fixes the boundary-map convention and defines every map in the displayed sequence.
For the splitting assertion, first take . We use the cohomological Serre spectral sequence with coefficient group :
Since is simply connected, these coefficient systems are constant. The Eilenberg–MacLane space has for , and
For this uses , with abelian; for it follows from the Hurewicz theorem and the universal coefficient theorem for cohomology. Let correspond to , the universal cohomology class of an Eilenberg–MacLane space.
In bidegree there are no incoming differentials. For , an outgoing differential lands in a vanishing fiber-cohomology row. The only remaining possible differential is
Thus survives. The edge map, which is restriction to , supplies a class
By representability of cohomology by Eilenberg–MacLane spaces, choose a based map representing . On , induces the identity on and is an isomorphism on every homotopy group, since the other positive groups vanish.
Consider . This is a map of fibrations over , whose map on the fiber is the weak equivalence just obtained. The map on the base is the identity. Comparing the two instances of the long exact sequence of homotopy groups of a fibration and applying exactness, or the Five lemma in the group-valued range, shows that induces all homotopy isomorphisms. The spaces are path-connected because the base and fiber are. Hence the splitting of a simply connected Eilenberg–MacLane fibration gives
The crucial use of is to lift the fiber's identity class; existence of a section alone was not assumed to prove a product splitting.
If is allowed, its components have trivial positive homotopy groups. The simply connected base has no monodromy on this discrete set. Obstruction theory on the CW base gives a section in each fiber component, since all positive-dimensional fiber obstructions vanish and the component system is constant. Together these sections give , a weak equivalence on each component. Thus the same conclusion also covers that interpretation.