Finite type and odd-primary acyclicity of K(F₂,q)

Proof of the base case. Take K_1=BO(1)=RP∞. Its orientation double cover is BSO(1)=V_1(R∞), contractible by the published stable-Stiefel theorem. The oriented-Grassmannian definition supplies this literal double cover. The covering homotopy lifting and fibration long exact sequence give π₁=Z/2 and no higher homotopy groups. The Schubert CW construction has one cell in each nonnegative degree (rank-one symbol a₁=d+1); thus its integral cellular chains are finite free in each degree. Cellular homology and Noetherian submodules give integral finite generation. The finite-cover transfer, with $d=2$, identifies its F-cohomology with that of its contractible cover, hence it vanishes in positive degrees. Field evaluation UCT identifies cohomology with the dual of homology; a nonzero vector has a nonzero functional under AC, so field homology also vanishes. Marked homotopy uniqueness transports all these facts to any chosen CW model.

Proof of the induction step. Use the actual mapping-path fibration ΩK_q→PK_q→K_q with contractible total space. Its fibration long exact sequence makes the strict loop fiber path connected and gives its only nonzero homotopy group as Z/2 in degree q−1. To compare its homology with that of K_{q-1}, no imported CW-type-of-fibers theorem is necessary: take the published weak CW approximation L→ΩK_q. It is connected and has precisely these homotopy groups, so the published marked CW-model uniqueness gives a homotopy equivalence K_{q-1}→L. Their composite is a weak equivalence to the strict loop fiber. The inspected weak-equivalence homology theorem identifies its integral homology with H_*(K_{q-1};Z), and coefficient UCT makes the same comparison over each field. This makes the strict-fiber comparison fully local: its only ingredients are the mapping-path fibration, its homotopy exact sequence, weak CW approximation, marked CW-model uniqueness and coefficient UCT. No CW-type-of-fibers theorem or strict-fiber homotopy equivalence is used. For q≥2 the base is simply connected, so the homological Serre system is constant. Suppose integral homology of K_{q-1} is finitely generated in every degree. Prove H_s(K_q;Z) finitely generated by induction on s. H₀=Z and H₁=0. For s>1 the bottom-row term E²_{s,0}=H_s(K_q;Z) has no incoming differentials. Its outgoing differential on page a has target E^a_{s-a,a-1}, 2≤a≤s. The target is a subquotient of H_{s-a}(K_q;H_{a-1}(K_{q-1};Z)). The coefficient UCT expresses this group as an extension of a tensor product involving H_{s-a}(K_q;Z) and a Tor group involving H_{s-a-1}(K_q;Z). Both base degrees are smaller than s, and both coefficient groups are finitely generated. The PID decomposition makes their tensor and Tor groups finitely generated; Noetherianity makes every target and image finitely generated. There are only finitely many such pages, and E∞_{s,0}=0 because the total space is contractible. The successive kernels therefore filter H_s(K_q;Z) with finitely generated image quotients and zero final kernel. Finite extensions prove the assertion. This is a reverse finite-generation argument, proved here; the published Serre finite-generation transfer alone does not assert it.

For coefficients in F, induction makes the fiber homology F in degree zero and zero elsewhere. The homological Serre sequence consequently has only its bottom row and no possible differential. Its contractible abutment forces the positive base homology to vanish. Field UCT gives the cohomology assertion. Integral homology UCT injects H_n(K_q;Z)⊗F into H_n(K_q;F). Taking F=Q removes the free part; taking every odd F_p removes each odd-primary summand in the finite abelian-group decomposition. Thus each positive group is finite 2-primary. Integral cohomology UCT and the cyclic free resolution show the same for positive integral cohomology. With F₂ coefficients tensor and Tor of finite groups are finite-dimensional; the first nonzero degree and lower vanishing follow from ordinary Hurewicz and evaluation UCT (for q=1, use abelianization). This completes the induction.

No mod-two metastable operation-basis theorem is proved by this item: identifying H^{q+i}(K_q;F₂) with admissible Steenrod operations for i<q remains a different supplier. Integral cohomology must not be identified with that F₂-vector space merely because the integral groups are 2-primary.