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.

Whitney sum formula for Stiefel–Whitney classes

Statement

Assume AC. Let E→B and F→B be numerable real vector bundles of ranks m,n≥0 over a paracompact Hausdorff CGWH base of CW homotopy type. Then the total Stiefel–Whitney classes satisfy w(E⊕F)=w(E)w(F),equivalentlywk(E⊕F)=∑i+j=kwi(E)wj(F)(k≥0). In particular w(0B)=1, and adjoining a trivial summand does not change the positive classes: w(E⊕εBr)=w(E) for r≥0.

Facts & Assumptions

Given: AC, numerable real bundles E,F→B of ranks m,n≥0 over a paracompact Hausdorff CGWH base of CW homotopy type, and the projective bundle X:=P(E⊕F) of their Whitney sum.

[F1]

The bundles E and F are subbundles of E⊕F in the first and second summand, and over a trivializing chart U the projective bundle is X∣U≅U×Pm+n−1 with P(E)∣U=U×Pm−1 and P(F)∣U=U×Pn−1; the tautological line of E⊕F over P(E) is the tautological line of E, and symmetrically (Real projective bundle and tautological line, Whitney sum, tensor, dual, Hom, and exterior-power bundles).

[F2]

The pair sequence is exact and natural: for A⊆X, ⋯→Hk(X,A;R)→Hk(X;R)→Hk(A;R)→∂Hk+1(X,A;R)→⋯, and a continuous map of pairs induces a map of sequences with commuting squares (Long exact sequence of a pair in singular cohomology, Naturality of the singular cohomology pair sequence).

[F3]

Homotopic maps induce the same singular cohomology map; consequently a homotopy equivalence induces isomorphisms on cohomology (Homotopic maps induce equal maps in singular cohomology).

[F4]

Relative cup products exist for subspaces A,B that are open in A∪B, take values in Hp+q(X,A∪B;R), and are natural: for f:X′→X with f(A′)⊆A and f(B′)⊆B one has f∗(u⌣v)=f∗u⌣f∗v; with A′=B′=∅ this says that the relative-to-absolute map carries u⌣v to the absolute product (Relative cup product for an excisive triad, Relative cup products are natural and connector-compatible).

[F5]

When m+n≥1, the projective-bundle theorem applies to X=P(E⊕F) over B: with x=xE⊕F, the classes 1,x,…,xm+n−1 are an H∗(B;F2)-basis and the unique monic degree-(m+n) relation determines the classes of E⊕F (Mod-two real projective bundle theorem, Stiefel–Whitney classes from the projective-bundle relation). When m+n=0, P(E⊕F)=∅ and the rank-zero convention is used instead; no tautological class or projective-bundle basis is asserted.

[F6]

Under the inclusion iE:P(E)↪P(E⊕F), the bundle projection satisfies piE=pE and the tautological line pulls back to the tautological line of E; hence naturality gives iE∗xE⊕F=xE, while iE∗p∗wj(E)=pE∗wj(E) (Real projective bundle and tautological line, Naturality of Stiefel–Whitney classes).

[A1]

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

Proof

1.1F1algebra

Suppose first m,n≥1 and put A=P(E), C=P(F) inside X=P(E⊕F), and U2=X∖A, U1=X∖C. Both A and C are closed subbundles and they are disjoint, since a line contained in both Eb and Fb would lie in Eb∩Fb=0. In a chart U⊆B write a line as [v:w] with v∈Rm, w∈Rn, not both zero; then A∣U={[v:0]}, C∣U={[0:w]}. The formula Ht[v:w]=[v:(1−t)w] for 0≤t≤1 is well defined and independent of the local chart because it is induced by the canonical linear map E⊕F→E⊕F, (v,w)↦(v,(1−t)w) on the complement of C; it is continuous there, fixes A pointwise, and satisfies H0=id⁡, H1(X∖C)⊆A. Hence U1=X∖C deformation retracts onto A, and symmetrically U2=X∖A deformation retracts onto C. Both are open, and U1∪U2=X∖(A∩C)=X.

1.2F5F6

The class ωE:=∑i=0mp∗wi(E)⌣xm−i restricts to zero on A, and ωF:=∑j=0np∗wj(F)⌣xn−j restricts to zero on C. Indeed A=P(E)⊆X and [F6] gives iE∗x=xE and iE∗p∗wi(E)=pE∗wi(E), so the restricted expression is exactly the defining projective-bundle relation of E. The argument for C is symmetric.

2.1F2F3step 1.1step 1.2

Each class lifts to the relative group of the corresponding complement. Since ωE restricts to zero on A, exactness of the pair sequence [F2] exhibits ωE as the image of a class ω~E∈Hm(X,A;F2). The inclusion of pairs (X,A)→(X,U1) is an isomorphism on relative cohomology: by step 1.1 the inclusion A↪U1 is a homotopy equivalence, so in the map of pair sequences [F2] the two vertical maps H∗(X)→H∗(X) and H∗(U1)→H∗(A) are isomorphisms, and the five lemma (equivalently, the long exact sequences split into commuting exact pieces with two isomorphisms out of three) gives that H∗(X,U1)→H∗(X,A) is an isomorphism; [F3] supplies the homotopy invariance of the restriction. Thus ωE has a preimage ω~E∈Hm(X,U1;F2). Symmetrically ωF has a preimage ω~F∈Hn(X,U2;F2).

3.1F4step 1.1step 2.1

The relative product vanishes. Both U1 and U2 are open in X and open in their union X, so [F4] applies to A=U1, B=U2 and defines ω~E⌣ω~F∈Hm+n(X,U1∪U2;F2)=Hm+n(X,X;F2)=0. Under the relative-to-absolute map, which by the naturality clause of [F4] with A′=B′=∅ sends the product to the absolute cup product of the images, this class maps to ωE⌣ωF∈Hm+n(X;F2). Hence ωEωF=0.

4.1F5step 3.1algebra

Expand the vanishing product: ωEωF=∑k=0m+n(∑i+j=kwi(E)wj(F))xm+n−k=0, with xm+n-coefficient w0(E)w0(F)=1, so this is a monic relation of degree m+n for x on X=P(E⊕F). By the uniqueness clause of [F5] it is the defining relation of E⊕F, so wk(E⊕F)=∑i+j=kwi(E)wj(F)(0≤k≤m+n), and for k>m+n both sides vanish by the rank conventions. Summing gives w(E⊕F)=w(E)w(F).

5.1F5F6step 1.1step 4.1

Degenerate ranks and trivial summands. If m=0 then E=0B, E⊕F≅F, and w(E)=1, so the formula holds; symmetrically for n=0. Taking F=εBr trivial of rank r: its classifying map is the constant map, so w(εBr)=1 by naturality [F6] and the rank conventions, and the formula gives w(E⊕εBr)=w(E). For r=1 this says the positive classes are unchanged by adding a trivial line. If m=n=1 then X=P(E⊕F) is a P1-bundle, A and C are two disjoint sections, and the argument reduces to the displayed computation with k≤2. The empty base gives zero groups and the zero relation, and the formulas hold in the zero ring with unit 1.

6.1F5A1step 1.2step 2.1step 3.1∎

Axiom audit. The argument uses AC only through the projective-bundle theorem [F5] for E⊕F; the pair sequences, the relative cup product and the deformation retraction of step 1.1 are choice-free, and the only geometry used is the canonical linear homotopy inside each fiber.

Depends on

Dependency tree · 2 levels

Sources