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.

Thom identity for Stiefel–Whitney classes

Statement

Assume AC. Let EB be a numerable real vector bundle of rank n0 over a paracompact Hausdorff CGWH base of CW type (the admissible bases of this page), with its canonical F2-orientation and normalized mod-two Thom class uEHn(D(E),S(E);F2). Then Sq(uE)=w(E)uE, equivalently Sqi(uE)=wi(E)uEfor every i0, with both sides vanishing for i>n.

Facts & Assumptions

Given: The bundle and base of the statement. Coefficients below are F2. For a relative class of degree d0, Sq denotes the finite sum i=0dSqi.

[A1]

AC is assumed for the Thom, classification, splitting and universal-cohomology suppliers. (The Axiom of Choice).

[F1]

Steenrod squares are natural homomorphisms on cohomology of pairs. They satisfy Sq0=id, instability and the top-square formula, also relatively. The Cartan formula used here is only the absolute formula on cohomology of a space. The absolute total square is the finite graded sum. (Steenrod squares are well-defined and natural, Steenrod normalization, instability, suspension, and top square, Cartan formula for Steenrod squares, Total Steenrod square).

[F2]

For a canonically mod-two oriented numerable bundle in this base class, Φ(a)=πau is the Thom isomorphism in every degree. The fiberwise normalized Thom class is unique and natural under bundle pullback; the Euler class is e2=sju. The normalized rank-zero Thom class is 1. (Thom isomorphism for oriented vector bundles, Naturality and uniqueness of Thom classes, Euler class by zero-section pullback of the Thom class, Thom class by fiberwise normalization).

[F3]

The classes wi are natural, satisfy the Whitney product formula, w0=1 and wi=0 above the rank. Also e2(E)=wn(E) for a rank-n bundle in the stated scope. (Naturality of Stiefel–Whitney classes, Whitney sum formula for Stiefel–Whitney classes, Stiefel–Whitney classes from the projective-bundle relation, The mod-two Euler class is the top Stiefel–Whitney class).

[F4]

The real flag bundle has admissible base, splits the pulled-back bundle into line bundles, and induces an injective map in mod-two cohomology. (Real splitting principle with mod-two injective pullback).

[F5]

For n1, H(BO(n);F2)=F2[w1,,wn], with the generators the classes of the tautological bundle γn. Numerable real rank-n bundles on the given bases are classified by maps into BO(n)=Grn(R). This Grassmannian carries its Schubert CW structure. (Mod-two cohomology of BO(n), Real and complex vector bundles are classified by stable Grassmannians, Schubert cells give the stable Grassmannian CW structure).

[F6]

Homotopic maps give the same singular cohomology pullback with any abelian coefficients. Relative cup products are natural for excisive triples, including the absolute-relative module action and forgetting the relative subspace; the pairs of subspaces ,S are open in their union S. Absolute cup products are graded commutative. (Homotopic maps induce equal maps in singular cohomology, Relative cup product for an excisive triad, Relative cup products are natural and connector-compatible, Singular cohomology is graded commutative).

[F7]

The universal Grassmannian is an admissible base and its tautological bundle is numerable. The finite-dimensional compact Grassmannians give its compact exhaustion; numerability follows from Hatcher, Vector Bundles & K-Theory, Proposition 1.19, printed p.36, https://pi.math.cornell.edu/~hatcher/VBKT/VB.pdf . Its CW structure is also in [F5].

Proof

technique · direct, detecting the universal relative identity in absolute cohomology
1.1

An absolute identity. For a rank-n bundle E, n1, take its flag map q from [F4], and write qE=j=1nLj, tj=w1(Lj). The rank convention and Whitney formula give qwn(E)=jtj and qw(E)=j(1+tj). Since tj has degree one, [F1] gives Sq(tj)=tj+tj2. Absolute Cartan and commutativity over F2 therefore give Sq(qwn(E))=j(tj+tj2)=(j(1+tj))(jtj)=q(w(E)wn(E)). Naturality of each square and injectivity of q give Sq(wn(E))=w(E)wn(E). All sums and products here are finite and all classes are absolute.

F1F3F4F6algebra
1.2

Forgetting the relative subspace. For any bundle in [F2], put D=D(E), S=S(E), let π:DB be projection, let s be its zero section, and write j:H(D,S)H(D) for the forgetful map induced by (D,)(D,S). Radial contraction gives sπidD and πs=idB. Thus [F6] and the Euler definition imply ju=πe2(E). Naturality of the relative module product, with triples (D;,)(D;,S), gives jΦ(a)=πaju=π(ae2(E)). The relevant cup comparisons exist because and S are open in S; no Cartan assertion for a relative product is involved.

F2F6algebra
2.1

Universal injectivity. Let E=γn, n1. The hypotheses of [F2] hold by [F5] and [F7]. In the polynomial ring of [F5], multiplication by the variable wn is injective: it shifts the exponent of that variable in each distinct monomial. By [F3] it is multiplication by e2(γn). The identity in step 1.2, the isomorphism Φ and the isomorphism π show that j:Hk(D(γn),S(γn))Hk(D(γn)) is injective in every degree. Explicitly, write any relative class as Φ(a); if its image is zero then awn=0, hence a=0. This also covers zero groups in degrees below n.

F2F3F5F6F7step 1.2algebra
3.1

Universal Thom identity. Write u=uγn. Naturality of the squares for the pair map defining j and for the space map π gives jSq(u)=Sq(ju)=Sq(πwn)=πSq(wn)=π(w(γn)wn)=j(πw(γn)u). The third equality uses step 1.2 and [F3], the fourth uses step 1.1, and the last uses step 1.2. Injectivity in step 2.1, degree by degree, proves the identity for γn.

F1F3step 1.1step 1.2step 2.1algebra
4.1

Pull back to the given bundle. For n1, choose a classifying map c:BBO(n) and an isomorphism Ecγn by [F5]. Use the pulled-back metric through this isomorphism to obtain a map c~:(D(E),S(E))(D(γn),S(γn)) over c. Changing a supplied metric does not change the identity: the fiberwise radial map sending a nonzero vector v to voldv/vnew is a homeomorphism of the old and new disk-sphere pairs over B, extends continuously by zero, and preserves the mod-two fiber generator; its inverse interchanges the two norms. By normalized Thom naturality, c~uγn=uE. Pull back step 3.1, using pair naturality of Sq, naturality of w, and relative cup naturality. This gives Sq(uE)=πw(E)uE, with the base pullback suppressed in the statement's usual module notation.

F1F2F3F5F6step 3.1algebra
5.1

Degrees and boundaries. For n=0 the disk-sphere pair is (B,), u=1 and w(0B)=1. Normalization and instability give Sq0(1)=1 and Sqi(1)=0 for i>0, proving the identity separately, without multiplying by a nonexistent polynomial variable w0. Over the empty base all groups and classes are zero. For n1 step 4.1 and for n=0 the preceding calculation give the total identity; comparison of degree n+i components gives the stated formula for every i0. Both sides are zero for i>n by instability and the rank convention. The sums are finite even for infinite-dimensional bases. AC enters exactly through the Thom, splitting, classification and universal-cohomology suppliers and the numerability assertion; the subsequent polynomial and cohomology calculations require no further choices.

A1F1F2F3F5F7step 4.1algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

79 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