Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
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.

The normal Stiefel-Whitney class is the multiplicative inverse of the tangent class

Statement

Assume AC. Let M be a closed smooth m-manifold, let (ν,φ) be a stable normal inverse of M with φ:TM⊕ν→εN, and let w(E)=∑iwi(E) denote the total Stiefel-Whitney class in the ring H∗(M;F2) (Stiefel–Whitney classes from the projective-bundle relation, Singular cohomology ring). Then w(TM) w(ν)=1in H∗(M;F2). Hence w(ν) is the unique two-sided inverse of w(TM), and the classes wi(ν) depend only on M, not on the chosen stable normal inverse (ν,φ). Equivalently the total normal class is w(ν)=w(TM)−1=:wˉ(M), the Whitney-duality form of the normal Stiefel-Whitney class.

Facts & Assumptions

Given: A closed smooth m-manifold M, a stable normal inverse (ν,φ) with φ:TM⊕ν→εN a smooth bundle isomorphism, and AC (Stable normal inverse of the tangent bundle, The Axiom of Choice).

[F1]

Stiefel-Whitney classes are defined for numerable real bundles over a paracompact Hausdorff CGWH base of CW homotopy type, with w0=1, wi=0 for i>rank⁡, and total class w(E)=∑iwi(E)∈H∗(B;F2) (Stiefel–Whitney classes from the projective-bundle relation, Singular cohomology ring).

[F2]

The Whitney sum formula w(E⊕F)=w(E)w(F) holds for numerable bundles over such a base, and adjoining a trivial summand does not change the classes: w(E⊕εr)=w(E), so w(εr)=1 (Whitney sum formula for Stiefel–Whitney classes).

[F3]

The classes depend only on the isomorphism class of the bundle (Naturality of Stiefel–Whitney classes).

[F4]

A closed smooth manifold is a paracompact Hausdorff CGWH space of CW homotopy type, and every smooth bundle over it, in particular TM, ν and the trivial bundle, is numerable (Smooth manifolds have CW homotopy type); this puts M and these bundles in the scope of [F1]–[F3]. AC is the hypothesis of those suppliers.

[F5]

Singular cohomology is graded commutative; over F2 the signs are 1, so H∗(M;F2) is a commutative unital ring (Singular cohomology ring, Singular cohomology is graded commutative). If uv=1=uw, then v=v(uw)=(vu)w=w, so inverses are unique.

Proof

1.1F2F3F4F5

By [F3] the isomorphism φ gives w(TM⊕ν)=w(εN); by [F2], w(TM⊕ν)=w(TM)w(ν) and w(εN)=1, the latter because εN is trivial and adjoining trivial summands does not change the classes. Hence w(TM)w(ν)=1in H∗(M;F2). The computation happens in the unital ring of [F5], and the bundles involved are numerable over the closed smooth manifold M by [F4], so the cited Whitney and naturality theorems apply.

2.1F2F5step 1.1∎

Equation w(TM)w(ν)=1 exhibits w(ν) as a two-sided inverse of w(TM), and by [F5] the inverse of a unit is unique; in particular if (ν0,φ0) and (ν1,φ1) are two stable normal inverses then w(ν0)=w(TM)−1=w(ν1), so each wi(ν) depends only on M. This justifies the notation wˉ(M):=w(TM)−1=w(ν). The argument uses no property of φ beyond its being a bundle isomorphism, no orientation of M, and only the choice assumed in AC, inherited through the AT suppliers [F1]–[F3].

Depends on

Used by

Dependency tree · two levels

53 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