Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Mod-two real projective bundle theorem

Statement

Assume AC. Let E→B be a numerable real vector bundle of rank n≥1 over a paracompact Hausdorff CGWH base B of CW homotopy type; in particular B may be any CW complex. Let P(E)→B be its projective bundle and x=xE∈H1(P(E);F2) the tautological degree-one class. Then H∗(P(E);F2) is a free H∗(B;F2)-module with basis 1,x,…,xn−1; there are unique classes ci(E)∈Hi(B;F2) with xn+c1(E)xn−1+⋯+cn(E)=0in Hn(P(E);F2), and this monic relation generates all polynomial relations: the H∗(B;F2)-algebra homomorphism H∗(B;F2)[x]→H∗(P(E);F2) sending x to xE and coefficients by pullback has kernel exactly the principal ideal generated by xn+c1(E)xn−1+⋯+cn(E).

Facts & Assumptions

Given: AC, a numerable real rank-n bundle E→B with n≥1 over a paracompact Hausdorff CGWH base of CW homotopy type, and the classes x=xE of The tautological degree-one class is well defined and fiber generating.

[F1]

P(E)→B is a numerable locally trivial fiber bundle with fiber RPn−1 (Real projective bundle and tautological line), and a numerable fiber bundle is a Hurewicz fibration, hence in particular a Serre fibration (Numerable fiber bundles are hurewicz fibrations).

[F2]

The restrictions of 1,x,…,xn−1 to every fiber P(Eb)≅RPn−1 form an F2-basis of H∗(P(Eb);F2) (The tautological degree-one class is well defined and fiber generating).

[F3]

Let F→E′→pB′ be a Serre fibration over a path-connected CW complex and let finitely many homogeneous classes ei∈H∗(E′;R) restrict to an R-basis of H∗(F;R) on every fiber. Then Φ((ai))=∑ip∗ai⌣ei is an H∗(B′;R)-module isomorphism ⨁iH∗−∣ei∣(B′;R)→H∗(E′;R), natural in maps of such fibrations that pull the specified classes back to the specified classes (Leray–Hirsch module isomorphism).

[F4]

Pullback is a unital ring homomorphism and cup products are natural (Cup product is natural, unital and associative).

[F5]

The homotopy long exact sequence of a Serre fibration is exact and natural, including the component tail (Long exact sequence of homotopy groups of a fibration, Fibration sequence is natural).

[F6]

Under AC, for every space X, abelian group G and n≥0 there is a natural short exact sequence 0→Ext⁡Z1(Hn−1(X;Z),G)→Hn(X;G)→Hom⁡Z(Hn(X;Z),G)→0 (Topological universal coefficient short exact sequence for cohomology).

[F7]

Every weak homotopy equivalence induces isomorphisms on integral singular homology, with no choice principle and no CW hypothesis (Weak homotopy equivalences induce integral homology isomorphisms without choice).

[F8]

Pullback is canonically functorial: id⁡∗E≅E and f∗(g∗E)≅(gf)∗E (Vector-bundle pullback is canonically functorial).

[F9]

Under AC, a numerable bundle with compact Hausdorff CW-type fiber over a paracompact Hausdorff CW-type base has paracompact Hausdorff CW-type total space (Compact-fibre bundle totals preserve paracompactness, and CW type under CW-type hypotheses).

[A1]

AC is the Axiom of Choice in the form fixed by The Axiom of Choice.

[F10]

Homotopy equivalences induce cohomology isomorphisms (Homotopic maps induce equal maps in singular cohomology); the module five lemma applies to diagrams of the natural cohomological universal coefficient sequences (The Five Lemma for modules).

[F11]

Singular cohomology is graded-commutative; over F2 it is therefore commutative without degree restrictions (Singular cohomology is graded commutative).

Proof

1.1F1F2

The projection P(E)→B is a Serre fibration with fiber RPn−1 whose classes 1,x,…,xn−1 restrict to a basis of the fiber cohomology. This is [F1] combined with [F2]: the fiber over b is P(Eb) and the restrictions of the displayed classes are a basis.

1.2F1F5F8F9

Choose a homotopy equivalence g:K→B from a CW complex, put E′=g∗E, and form g′:P(E′)→P(E). Projectivization commutes with this pullback: in a pulled-back linear chart the identification sends (k,ℓ) to (k,(g(k),ℓ)), and the formulas agree on overlaps since both have the same pulled-back linear transitions. Hence P(E′)≅g∗P(E), with g′ restricting to the identity on each projective fiber. Both projective totals are paracompact Hausdorff of CW type by [F9]. Both projections are Serre fibrations by [F1]. In their natural homotopy sequences [F5], the fiber and base maps are isomorphisms on all homotopy groups. A direct exactness chase gives the same for the total map, including degree one: to lift a target total class, lift its base image by the base isomorphism; its fiber boundary vanishes by fiber injectivity, so it lifts to the source total group. Correct the difference using surjectivity on the fiber group. For injectivity, a source class killed in the target has zero base image, so comes from a fiber class. Its image is a target base boundary; lift that boundary through the base isomorphism and use fiber injectivity to see the original total class vanishes. The degree-one chase uses products rather than sums and the fact that the fiber is path connected, so the boundary to its component set is trivial. Path lifting with path-connected fibers identifies total components with base components. Thus g′ is a weak homotopy equivalence.

2.1F3A1step 1.1

Suppose first that B is a CW complex. Then [F3] applies to the Serre fibration of step 1.1 with the classes ei=xi, i=0,…,n−1, which are homogeneous of degree i and restrict to a basis by step 1.1, provided the base is path-connected. If B is path-connected, the conclusion is that Φ:⨁i=0n−1H∗−i(B;F2)⟶H∗(P(E);F2),(ai)⟼∑i=0n−1p∗ai⌣xi, is an H∗(B;F2)-module isomorphism, so H∗(P(E);F2) is free over H∗(B;F2) on 1,x,…,xn−1. If B is a general CW complex, its path components Bα are open and closed subcomplexes, because a CW complex is locally path-connected and cells are connected; restricting E gives a numerable bundle over the path-connected CW complex Bα, and P(E)=∐αP(E∣Bα). For a disjoint union X=∐αXα of open and closed pieces the singular chain complex is the direct sum of the piece complexes, since the connected simplex Δk maps into a single piece; dualising gives a product of cochain complexes, whose cycles are exactly the families of cycles and whose coboundaries are exactly the families of coboundaries, the latter using AC to select one primitive at each index. Hence Hk(X;R)≅∏αHk(Xα;R), and applying this to B and to P(E) turns the componentwise isomorphisms into the displayed H∗(B;F2)-module isomorphism.

3.1F2F3F4F6F7F10step 2.1step 1.2

By [F7], g′ is an integral homology isomorphism, and by [F6] and the module five lemma [F10], g′∗ is an isomorphism on F2-cohomology. Also g∗ is a cohomology isomorphism by [F10]. Apply Leray–Hirsch over each CW component of K using the specified classes ei=g′∗(xi), not an unproved identification with a separately defined tautological class on P(E′). They restrict to a fiber basis because g′ is the identity on each fiber and [F2] supplies that basis. The component argument of step 2.1 gives an isomorphism ΦK for these classes. Naturality [F4] gives g′∗ΦB=ΦK(⨁ig∗). The other three maps are isomorphisms, so ΦB is an isomorphism. Finite sums indexed by 0≤i<n commute with the degreewise component products. This proves the module claim on the stated general base.

4.1step 3.1algebra

Existence and uniqueness of the coefficients. By step 3.1 the elements 1,x,…,xn−1 form a module basis of H∗(P(E);F2) over H∗(B;F2). The class xn∈Hn(P(E);F2) therefore has a unique expansion xn=∑i=0n−1p∗bi⌣xi with bi∈Hn−i(B;F2). Setting ci(E):=bn−i∈Hi(B;F2), moving the terms to one side and using that the coefficient ring has characteristic two so that signs are trivial gives the unique relation xn+c1(E)xn−1+⋯+cn(E)=0, whose leading coefficient is 1.

5.1F4F11step 3.1step 4.1algebra

The relation generates all relations. Let φ:H∗(B;F2)[x]→H∗(P(E);F2) be the H∗(B;F2)-algebra homomorphism with φ(x)=x and φ(a)=p∗a; it is well defined because [F4] makes p∗ a unital ring homomorphism and [F11] makes all classes commute. By step 3.1 it is surjective, since the module basis lies in its image. Let f=xn+c1(E)xn−1+⋯+cn(E) be the monic relation of step 4.1, of degree n. Division with remainder by a monic polynomial is available over any commutative ring, so every element of H∗(B;F2)[x] has a unique representative ∑i=0n−1gixi modulo the principal ideal (f), and the classes 1,x,…,xn−1 are a module basis of H∗(B;F2)[x]/(f). The induced map φˉ:H∗(B;F2)[x]/(f)→H∗(P(E);F2) sends that basis to the module basis of step 3.1 and is H∗(B;F2)-linear, so it is an isomorphism and ker⁡φ=(f).

6.1F1F3F6A1step 2.1step 3.1∎

Boundary cases. For n=1 the basis is 1 alone and the relation is x+c1(E)=0, so the argument above applies verbatim. For a disconnected base the degreewise identification of cohomology with the product over components was recorded in step 2.1 and transferred in step 3.1. If B=∅ then P(E)=∅ and all groups are zero, so the statement is valid with the unique n zero coefficients. The one-point fiber RP0 enters only through the basis statement for n=1. AC is used through [F1], [F3], the componentwise primitives of step 2.1 and the universal coefficient sequence of step 3.1, as recorded.

Depends on

Dependency tree · 2 levels

Sources