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.

Naturality of Stiefel–Whitney classes

Statement

Assume AC. Let f:BB be a continuous map of paracompact Hausdorff CGWH bases of CW homotopy type and let EB be a numerable real bundle of rank n0. Then wi(fE)=fwi(E)for every i0,w(fE)=fw(E). Consequently the Stiefel–Whitney classes depend only on the isomorphism class of the bundle.

Facts & Assumptions

Given: AC, paracompact Hausdorff CGWH bases B,B of CW homotopy type, a continuous map f:BB, and a numerable real rank-n bundle EB.

[F1]

Projective bundles and their tautological lines are glued from the local models U×RPn1 and {(b,,v):v} with the transition matrices of the vector bundle. Their numerations and base-space properties are as in Real projective bundle and tautological line.

[F2]

The class xE is ca for any classifying map c of γE, and is independent of that choice (Tautological degree-one class on a real projective bundle, The tautological degree-one class is well defined and fiber generating).

[F3]

For n1, under AC, H(P(E);F2) is free over H(B;F2) on 1,xE,,xEn1, with unique monic relation xEn+w1(E)xEn1++wn(E)=0 (Stiefel–Whitney classes from the projective-bundle relation, Mod-two real projective bundle theorem). The definition also gives w0=1, wi=0 for i>n, and w(0)=1.

[F4]

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

[F5]

Canonical pullback comparisons: idEE and f(gE)(gf)E (Vector-bundle pullback is canonically functorial).

[A1]

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

Proof

1.1

Pulling back the defining relation. Assume first that n1. Let p:P(E)B and p:P(fE)B be the projections, and let f:P(fE)P(E) be the canonical map. In a chart EUU×Rn, it is (b,)(f(b),). These formulas commute with transition matrices, so they glue to a continuous map and identify P(fE) homeomorphically with B×BP(E), not generally with P(E). The corresponding formulas on vectors in give γfEfγE by [F1]. If c classifies γE, then cf classifies γfE by [F5], hence [F2] and [F4] give xfE=(cf)a=fxE. Applying the ring homomorphism f to the relation of [F3] and using [F4] together with pf=fp gives f(xEn+i=1npwi(E)xEni)=xfEn+i=1npfwi(E)xfEni=0, where the equality uses the just-proved naturality of x. Thus the displayed class is a monic degree-n relation for xfE over the base B.

F1F2F3F4F5
2.1

Comparing with the defining relation of fE. For n1, the pullback fE is a numerable real rank-n bundle over the admissible base B, so [F3] provides its unique monic relation xfEn+w1(fE)xfEn1++wn(fE)=0. By the uniqueness in [F3], comparing with step 1.1, the coefficients agree: wi(fE)=fwi(E)(1in). For i=0 both sides are the unit 1 by the conventions, and for i>n both sides are 0, since f0=0. Summing the finitely many nonzero terms gives w(fE)=ifwi(E)=fw(E) by [F4]. When n=0, neither projective bundle nor xE is used: both E and fE are rank-zero bundles and the defining convention gives w0=1 and wi=0 for i>0, so the same conclusions hold directly.

F3F4step 1.1
3.1

Isomorphism invariance. Let φ:EE be a bundle isomorphism over the identity of B. It induces a homeomorphism P(E)P(E) over B carrying tautological lines to tautological lines, write this homeomorphism as Pφ. The vector formula gives (Pφ)γEγE, so composition of a classifying map of γE with Pφ gives (Pφ)xE=xE, exactly as in step 1.1; the defining relation of E is therefore carried to the defining relation of E, and uniqueness of the monic relation gives wi(E)=wi(E) for all i. When n=0 both bundles are the zero bundle, and the conventions give w=1 on both sides.

F1F2F3F4F5step 1.1step 2.1
4.1

Boundary cases. For n=0 the bundle and its pullback are zero bundles, w=1 on both sides, and the identity w(f0)=fw(0)=f1=1 holds by [F4]. For n=1 the relation is x+w1=0 and the argument is the displayed one with i=1. If B is empty, both sides of every naturality equality lie in its zero cohomology ring and vanish. If B is empty, existence of f forces B empty too. The identity map is the case f=id, where [F5] identifies the pullback with E itself. AC is inherited through the projective-space, classification and relation interfaces [F1]–[F3].

F1F2F3F4F5A1step 2.1step 3.1

Depends on

Used by

Dependency tree · two levels

32 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources