TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Cartan formula for Steenrod squares

Statement

For $x \in H^{p} (X; F_{2})$ , $y \in H^{q} (X; F_{2})$ , and every integer $k$ , the Steenrod squares satisfy the Cartan formula

S q^{k} (x ⌣ y) = \sum_{i + j = k} S q^{i} (x) ⌣ S q^{j} (y) .

Only finitely many terms are nonzero. More generally, for classes on two spaces the external formula is

S q^{k} (x \times y) = \sum_{i + j = k} S q^{i} (x) \times S q^{j} (y) .

Facts & Assumptions

Given: Mod-two cocycles $a, b$ representing classes of degrees $p, q$ .

[F1]

Squares vanish above the degree of their input (Steenrod normalization, instability, suspension, and top square).

[F2]

The before-Alexander--Whitney and convolution families have the coherent homotopy with its exact $(1 + Q) H_{i - 1}$ correction (Cartan coherence for higher diagonals).

[F3]

Squares are independent of the coherent higher-diagonal system (Steenrod squares are well-defined and natural).

[F4]

A square of a degree- $n$ class is represented by $a ⌣_{n - k} a$ in its defining range (Steenrod squares from cup-i).

[F5]

The Alexander--Whitney external cochain represents the cohomology cross product, and its pullback along the diagonal is the cup product (Singular cup product on cochains).

[F6]

Alexander--Whitney and shuffle are chain-homotopy inverses (Alexander--Whitney and shuffle are natural chain-homotopy inverses).

[F7]

Squares are natural for maps of spaces (Steenrod squares are well-defined and natural).

Proof

Proof technique: evaluate Cartan coherence and pull back the external formula along the diagonal.

1.1

Reduce to the normalized face-formula system. [F1, F3, F4, F5, F6] Because of [F3], compute all squares with the explicit system in Medina--Mardones, Definition 7 and Theorem 10 (printed pages 8--9). It has $D_{r} (s) = 0$ when $r$ exceeds the dimension of the simplex $s$ . By [F5], the external class $[a] \times [b]$ is represented by the Alexander--Whitney external cochain. Since shuffle induces the inverse cohomology isomorphism by [F6], it suffices to compare the two sides after precomposition with shuffle. If $k < 0$ , every square in the formula is zero by definition. If $k > p + q$ , at least one of $i > p$ or $j > q$ holds in each summand, so [F1] makes both sides zero. Hence assume $0 \leq k \leq p + q$ and put $ℓ = p + q - k$ .

2.1

Evaluate the coherent comparison. [F2, step 1.1] Pair the equation for $L_{ℓ} - R_{ℓ}$ in [F2] with $λ = a \otimes b \otimes a \otimes b$ . Since $a, b$ are cocycles, $λ d = 0$ . Also $λ Q = λ$ , so the two evaluations of $Q H_{ℓ - 1}$ and $H_{ℓ - 1}$ cancel in characteristic two. Therefore

λ L_{ℓ} - λ R_{ℓ} = δ (λ H_{ℓ}) .

The left term is the shuffled cochain representing $S q^{k} ([a] \times [b])$ ; the right term is cohomologous to it.

3.1

Identify every convolution term. [F4, step 2.1] For $r + s = ℓ$ , regrouping the four factors gives

λ τ (D_{r} \otimes T^{r} D_{s}) = (a ⌣_{r} a) \otimes (b ⌣_{s} b),

because $(b \otimes b) T^{r} = b \otimes b$ . The normalized face formula makes the first factor zero when $r > p$ and the second zero when $s > q$ : on the only chain degree where it could be evaluated, respectively $2 p - r$ or $2 q - s$ , the higher-diagonal index exceeds the simplex dimension. For the remaining terms put $i = p - r$ and $j = q - s$ . Then $i, j \geq 0$ , $i + j = k$ , and [F4] identifies their classes as $S q^{i} [a]$ and $S q^{j} [b]$ . Step 2.1 and the shuffle isomorphism prove the external Cartan formula.

4.1

Pull back along the diagonal. [F5, F7, step 3.1] For two classes $x, y$ on $X$ , [F5] gives $x ⌣ y = Δ^{*} (x \times y)$ . Naturality [F7] and step 3.1 give

S q^{k} (x ⌣ y) = Δ^{*} S q^{k} (x \times y) = \sum_{i + j = k} Δ^{*} (S q^{i} x \times S q^{j} y) = \sum_{i + j = k} S q^{i} x ⌣ S q^{j} y .

Instability [F1] leaves at most $(p + 1) (q + 1)$ possible pairs, so the sum is finite. Empty spaces, zero classes, degree-zero factors, one-point spaces, and degenerate singular simplices were retained throughout. Every formula is a specified finite sum, and no AC is used. ∎

Depends on

Used by

Total Steenrod square Definition
Steenrod squares on complex projective space mod two Example
Steenrod squares on real projective space Example
Adem relations for Steenrod squares Theorem

Dependency tree · two levels

21 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)
Medina-Mardones, New formulas for cup-i products and fast computation of Steenrod squares (standard reference, not scraped)