LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passverified 2026-11-04 (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.

Wu formula for a closed smooth manifold

Statement

Assume full AC. Let $M$ be a connected compact smooth $n$ -manifold without boundary. Let $v_{k} (M)$ be the Wu classes defined by the mod-two Poincare pairing and let $w_{i} (T M)$ be the Stiefel–Whitney classes of the real tangent bundle. For the total classes $v = \sum_{k = 0}^{n} v_{k}$ and $w = \sum_{i = 0}^{n} w_{i}$ , with $S q = \sum_{j \geq 0} S q^{j}$ , the identity is $w = S q (v) in H^{*} (M; F_{2}) .$

Statement references

Wu classes of a closed manifold

Thom identity for Stiefel–Whitney classes

Facts & Assumptions

Given: Full AC and a connected closed smooth $n$ -manifold $M$ , with its canonical mod-two fundamental class $[M]_{2}$ .

[A1]

Full AC is The Axiom of Choice, as inherited from the Wu-class and Poincare-duality suppliers.

[F1]

The Wu classes are characterized by $⟨ v_{k} x, [M]_{2} ⟩ = ⟨ S q^{k} x, [M]_{2} ⟩$ for $x \in H^{n - k} (M; F_{2})$ ; the mod-two cup pairing is nonsingular (Wu classes of a closed manifold, Poincaré duality gives a nonsingular cup pairing).

[F2]

The canonical mod-two orientation makes $M$ an $F_{2}$ -oriented closed manifold. The perfect mod-two Poincare pairing supplied by Poincaré duality gives a nonsingular cup pairing also gives finite-dimensional cohomology groups, so homogeneous bases and their Poincare-dual bases exist.

[F3]

The diagonal $Δ : M ↪ M \times M$ is a closed smooth embedding whose normal bundle is canonically isomorphic to $T M$ by $(u, v) \mapsto v - u$ . Its mod-two Poincare-dual class $u_{Δ} \in H^{n} (M \times M; F_{2})$ is the image of its normal Thom class and satisfies $u_{Δ} \cap [M \times M]_{2} = Δ_{*} [M]_{2}$ (The normal Thom class realizes the Poincare dual of a closed submanifold). The Kronecker pairing is compatible with cap-duality, cap-cup products, and pushforward under $Δ$ (The cap-duality map of an oriented manifold, Kronecker evaluation pairing, Cap naturality and projection formula).

[F4]

The cohomological Künneth theorem makes the external product a graded-ring isomorphism when $R$ is a PID and one factor has finite-free homology in every degree (Cohomological Kunneth cross product is a ring isomorphism). Here $R = F_{2}$ is a field, hence a PID, and the finite-generation part of the Poincaré-duality supplier's proof gives finite-dimensional $H_{j} (M; F_{2})$ for every $j$ ; finite-dimensional vector spaces are finite free, so the Künneth hypotheses hold. For external products the evaluation formula is $⟨ x \times y, [M \times M]_{2} ⟩ = ⟨ x, [M]_{2} ⟩ ⟨ y, [M]_{2} ⟩$ : it follows by evaluating external cochains on the singular chain cross product representing $[M]_{2} \times [M]_{2}$ , which is the local mod-two fundamental class of $M \times M$ . Thus the product cup pairing pairs decomposable classes by the product of the pairings on the factors, with signs trivial over $F_{2}$ (Poincaré duality gives a nonsingular cup pairing).

[F5]

The Thom identity gives $S q^{i} (u_{Δ}) = w_{i} (ν_{Δ}) ⌣ u_{Δ}$ , and the Whitney formula identifies the characteristic classes of the diagonal normal bundle with those of $T M$ (Thom identity for Stiefel–Whitney classes, Whitney sum formula for Stiefel–Whitney classes, Stiefel–Whitney classes from the projective-bundle relation).

[F6]

Steenrod squares are natural and satisfy the Cartan formula for external products; $S q^{0}$ is the identity and positive squares of the degree-zero unit vanish (Cartan formula for Steenrod squares, Steenrod normalization, instability, suspension, and top square).

Proof

technique · identify the diagonal class by dual bases, then apply the Thom identity and Cartan formula

1.1A1F1F2choose

If $M = \emptyset$ , its cohomology groups are zero, so $w = S q (v) = 0$ and the identity holds. Henceforth suppose $M$ is nonempty. For each $d$ , choose a basis ${b_{d, r}}_{r}$ of $H^{d} (M; F_{2})$ and its Poincare-dual basis ${b^{d, r}}_{r} \subseteq H^{n - d} (M; F_{2})$ , so $⟨ b^{d, r} ⌣ b_{e, s}, [M]_{2} ⟩ = δ_{d e} δ_{r s}$ . The finite-dimensionality in [F2] makes these finite bases, and nonsingularity gives the dual bases.

2.1F1F3F4step 1.1algebra

The Künneth isomorphism in [F4] and diagonal identity in [F3] give $u_{Δ} = \sum_{d, r} b^{d, r} \times b_{d, r} .$ Indeed, for any decomposable $a \times b$ of complementary degree, the evaluation formula in [F4] shows that pairing the right side with it gives $⟨ a ⌣ b, [M]_{2} ⟩$ : the dual-basis identities contract the two finite sums. This equals $⟨ u_{Δ} ⌣ (a \times b), [M \times M]_{2} ⟩$ because $u_{Δ} \cap [M \times M]_{2} = Δ_{*} [M]_{2}$ and cap-product naturality gives $Δ^{*} (a \times b) = a ⌣ b$ . Decomposables span by [F4], and the product pairing is nonsingular by [F1].

3.1F2F4step 2.1algebra

Define the linear map $λ : H^{*} (M \times M; F_{2}) \to H^{*} (M; F_{2})$ by $λ (a \times b) = ⟨ b, [M]_{2} ⟩ a$ and linear extension through the Kunneth isomorphism. This is well-defined by the tensor-product description in [F4]. Applying it to step 2.1 retains only $d = n$ ; connectedness makes $H^{n} (M; F_{2}) = F_{2}$ with its generator evaluating to $1$ , whose dual in $H^{0}$ is $1$ . Thus $λ (u_{Δ}) = 1$ . Also $λ ((c \times 1) z) = c ⌣ λ (z)$ for every $c \in H^{*} (M; F_{2})$ and $z \in H^{*} (M \times M; F_{2})$ , first on decomposables and then by linearity.

4.1F3F5step 3.1algebra

The normal bundle identification in [F3] and Thom identity [F5] give $S q^{i} (u_{Δ}) = (w_{i} (T M) \times 1) ⌣ u_{Δ}$ . Applying $λ$ and using step 3.1 yields $λ (S q^{i} (u_{Δ})) = w_{i} (T M)$ . Summing the finite nonzero components gives $λ (S q (u_{Δ})) = w (T M)$ .

4.2F1F4F6step 1.1step 3.1algebra

By Cartan and naturality in [F6], $S q (u_{Δ}) = \sum_{d, r} S q (b^{d, r}) \times S q (b_{d, r})$ . Therefore step 3.1 gives $λ (S q (u_{Δ})) = \sum_{d, r} ⟨ S q (b_{d, r}), [M]_{2} ⟩ S q (b^{d, r}) .$ The dual-basis expansion and the defining Wu pairing in [F1] say $v = \sum_{d, r} ⟨ S q (b_{d, r}), [M]_{2} ⟩ b^{d, r}$ : for each homogeneous degree, pairing this expression with any basis element of complementary degree recovers exactly the defining Steenrod-square functional. Hence the preceding sum is $S q (v)$ .

5.1F1F3F5F6step 4.1step 4.2∎

Steps 4.1 and 4.2 identify the same class $λ (S q (u_{Δ}))$ as $w (T M)$ and $S q (v)$ , respectively. Thus $w (T M) = S q (v)$ in mod-two cohomology. The empty case was settled in step 1.1, and connectedness excludes more than one nonempty component; degrees above $n$ vanish by the rank convention, all sums are finite, and signs in the diagonal and product formulas disappear over $F_{2}$ . This proves the asserted identity without an orientation choice.

Depends on

Dependency tree · 2 levels

Sources

John W. Milnor and James D. Stasheff, Characteristic Classes