TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedaudited 2026-09-14

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.

Steenrod squares are well-defined and natural

Statement

For every integer $k$ , $S q^{k}$ is independent of the cocycle representative and of the chosen coherently carried higher-diagonal system. It is additive and natural for maps of spaces and pairs. Thus

S q^{k} ⁣ : H^{n} (X, A; F_{2}) ⟶ H^{n + k} (X, A; F_{2})

is a natural homomorphism, with the outside-range values fixed to zero by the definition.

Facts & Assumptions

Given: Degree- $n$ cocycles $a, b$ and the index $j = n - k$ .

[F1]

For $0 \leq k \leq n$ , the proposed square is represented by $a ⌣_{n - k} a$ ; for $k < 0$ or $k > n$ , it is the zero operation (Steenrod squares from cup-i).

[F2]

The cup- $i$ coboundary formula has the two transposed $⌣_{i - 1}$ terms (Cup-i coboundary identity).

[F3]

The maps $D_{i}$ are natural (Natural higher diagonal approximations).

[F4]

They carry chains of a subspace into the tensor square of that subspace (Natural higher diagonal approximations).

[F5]

Two systems have natural $K_{i}$ satisfying $D_{i} - D_{i}^{'} = d K_{i} + K_{i} d + (1 + T) K_{i - 1}$ (Natural higher diagonal approximations).

Proof

technique · explicit polarization and coherent chain homotopy

1.1F1F2

If $k < 0$ or $k > n$ , [F1] makes $S q^{k}$ the zero homomorphism, so independence, additivity, and naturality are immediate. Hence assume $0 \leq k \leq n$ , so $j = n - k \geq 0$ . The operation is additive. Expanding $(a + b) ⌣_{j} (a + b)$ leaves, besides the two individual squares, the cross term $a ⌣_{j} b + b ⌣_{j} a$ . Since $a, b$ are cocycles, [F2] says

$a ⌣_{j} b + b ⌣_{j} a = δ (a ⌣_{j + 1} b) .$

Hence the cross term vanishes in cohomology.

1.2F1F5

The class is independent of the coherently carried system. Pair $D_{j} - D_{j}^{'} = d K_{j} + K_{j} d + (1 + T) K_{j - 1}$ with $a \otimes a$ . The $d K_{j}$ term vanishes because $a \otimes a$ is a cocycle, the $K_{j} d$ term is the coboundary of $c \mapsto (a \otimes a) K_{j} c$ , and the final term is zero because $(a \otimes a) T = a \otimes a$ and $2 = 0$ .

1.3F3F4

The representing cochains are natural for spaces and pairs. For $f ⁣ : X \to Y$ , naturality of $D_{j}$ makes $(f^{*} a \otimes f^{*} a) D_{j}^{X} = (a \otimes a) D_{j}^{Y} f_{#}$ , so the representing cochains agree. For a map of pairs, [F4] makes the same equation descend to relative cochains.

2.1F1F2step 1.1

The class is independent of its cocycle representative. If $a^{'} = a + δ h$ , expansion and two applications of [F2] give

$a^{'} ⌣_{j} a^{'} - a ⌣_{j} a = δ (a ⌣_{j + 1} δ h + h ⌣_{j} δ h + h ⌣_{j - 1} h) .$

Indeed the first summand differentiates to the two $a, δ h$ cross terms, while the last two differentiate to $(δ h) ⌣_{j} (δ h)$ ; all remaining terms occur twice. Negative cup indices are zero, so this calculation also covers the endpoints. Together with steps 1.1--1.3, this proves every assertion. ∎

Depends on

Used by

The mod-two square algebra, admissible sequences, and excess Definition
Total Steenrod square Definition
Wu classes of a closed manifold Definition
Steenrod squares on complex projective space mod two Example
Steenrod squares on real projective space Example
A Bockstein class on RP-two times RP-four has nonzero integral Sq-three Lemma
Admissible square actions have distinct leading monomials Lemma
Bockstein parity recurrence for Steenrod squares Lemma
Metastable cohomology of mod-two Eilenberg–Mac Lane spaces Lemma
Relative lifts produce cohomological transgressions Lemma
Stable Steenrod squares on universal Thom cohomology Lemma
Stable Thom cohomology is a square-module coalgebra Lemma
The universal mod-two class detects admissible composites in the strict range Lemma
Polynomial mod-two cohomology of Eilenberg–Mac Lane spaces Proposition
Steenrod normalization, instability, suspension, and top square Proposition
Adem relations for Steenrod squares Theorem
Cartan formula for Steenrod squares Theorem
The admissible square algebra is a connected bialgebra Theorem
Thom identity for Stiefel–Whitney classes Theorem

Dependency tree · two levels

6 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

Mosher and Tangora, Cohomology Operations and Applications (standard reference, not scraped)