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

Dependency tree · 2 levels

Sources

Mosher and Tangora, Cohomology Operations and Applications