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.1

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. [F1, F2] 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.2

The class is independent of the coherently carried system. [F1, F5] 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.3

The representing cochains are natural for spaces and pairs. [F3, F4] 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.1

The class is independent of its cocycle representative. [F1, F2, step 1.1] 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

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
Bockstein parity recurrence for Steenrod squares Lemma
Steenrod normalization, instability, suspension, and top square Proposition
Adem relations for Steenrod squares Theorem
Cartan formula for Steenrod squares 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)