Local path-fibration and cohomology inputs for mod-two Eilenberg–Mac Lane induction

The homotopy groups in the Eilenberg–Mac Lane definition give $(q-1)$-connectivity. Hurewicz gives $H_j(K_q;\mathbb{Z})=0$ for $0<j<q$ and $H_q(K_q;\mathbb{Z})={\mathbb{F}}_2$. The cohomological UCT then gives the claimed mod-two groups: in degree $q$ its Hom term is $\mathrm{Hom}({\mathbb{F}}_2,{\mathbb{F}}_2)={\mathbb{F}}_2$, its Ext term vanishes, and at degree one the possible $H_0$ Ext term also vanishes because $H_0=\mathbb{Z}$ is free. The normalized fundamental class is the identity evaluation class in the representability theorem. Apply the direct published mapping-path factorization to the marked inclusion $\ast \to K_q$. Its actual path-space total contracts by the supplier's explicit path reparametrization, and its strict fiber is $F=\mathrm{\Omega }{K}_q$. The fibration long exact sequence shows $F$ is path connected and its only nonzero positive homotopy group is $\mathbb{Z}\mathrm{/}2$ in degree $q-1$, marked by the connecting isomorphism. Apply the published CW approximation theorem to $F$, extending its marked basepoint as a one-point initial subcomplex. This gives a connected based CW complex $L$ and a based weak equivalence $\gamma :L\to F$. Transport the connecting marking to $L$; it is a marked CW $K(\mathbb{Z}\mathrm{/}2,q-1)$. The published marked uniqueness theorem supplies a homotopy equivalence $v:K_{q-1}\to L$ inducing that marking. If its marking uses basepoint transport, choose the corresponding path from $v$ of the marked point to the marked vertex of $L$, and use the published CW-point cofibration homotopy-extension property to homotope $v$ to a based map. The published moving-basepoint transport formula preserves the transported marking. (Choose the marked point of the CW source as a vertex.) Set $h=\gamma v$. It is a marked weak equivalence, and the published weak-equivalence homology lemma makes $h_{\ast }$ an isomorphism in integral homology in every degree. Naturality of coefficient UCT then makes $h_{\ast }$ an isomorphism in mod-two homology. Natural field evaluation duality makes $h^{\ast }$ an isomorphism in mod-two cohomology, and cup-product naturality makes it a unital graded-ring isomorphism. This chain of actual maps identifies the strict fiber's cohomology ring and fundamental class without an external CW-type-of-fibers theorem. The published multiplicative Serre theorem applies directly to the actual mapping-path fibration over the simply connected CW base; monodromy is trivial, and the just-proved ring isomorphism computes its strict fiber cohomology. Contractibility computes the positive-degree abutment as zero.

Important caveat. This lemma does not assert that every fiber class is transgressive or that taking its square commutes with a spectral-sequence differential in the manner required for the next induction. Those are additional claims, not consequences of ordinary Hurewicz or of spectral-sequence convergence alone.