LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Bockstein parity recurrence for Steenrod squares

Statement

Let $β : H^{*} (-; F_{2}) \to H^{* + 1} (-; F_{2})$ be the Bockstein of

$0 ⟶ F_{2} \overset{2}{\to} Z / 4 ⟶ F_{2} ⟶ 0.$

If $x \in H^{p} (X; F_{2})$ and $0 \leq j \leq p$ , then

$β S q^{j} (x) = {\begin{cases} S q^{j + 1} (x), & j even, \\ 0, & j odd . \end{cases}$

The value $S q^{p + 1} (x)$ at the endpoint $j = p$ is zero by the outside-range convention. The proof uses canonical residue lifts and makes no use of AC.

Facts & Assumptions

Given: A mod-two class $x$ of degree $p \geq 0$ and an index $0 \leq j \leq p$ .

[F1]

Natural mod-two higher diagonals are coherently unique once their Alexander--Whitney term is fixed (Natural higher diagonal approximations).

[F2]

Mod-two cup- $i$ is tensor evaluation on those diagonals (Higher cup-i products).

[F3]

The class $S q^{j} (x)$ is represented by $a ⌣_{p - j} a$ and is independent of the chosen coherent system (Steenrod squares from cup-i, Steenrod squares are well-defined and natural).

[F4]

The mod-two cup- $i$ coboundary identity has the two transposed cup- $(i - 1)$ terms (Cup-i coboundary identity).

[F5]

For the displayed cyclic coefficient sequence, least residue lifts compute the Bockstein without AC (Bockstein connecting operation).

[F6]

Alexander--Whitney and shuffle are augmentation-preserving chain-homotopy inverses over arbitrary coefficients (Alexander--Whitney and shuffle are natural chain-homotopy inverses).

Proof

Proof technique: lift the higher diagonals integrally, divide the signed cup- $i$ coboundary by two, and reduce the resulting parity calculation.

1.1

Construct a compatible signed integral cup- $i$ system. [F1, F2, F3, F6] Let $W_{Z}$ be the standard free $Z [C_{2}]$ -resolution with one generator $e_{i}$ in degree $i$ and

$d e_{i} = (1 + (- 1)^{i} T) e_{i - 1} (i > 0) .$

On tensor chains, let $T (c \otimes d) = (- 1)^{∣ c ∣ ∣ d ∣} d \otimes c$ . For every standard simplex, [F6] and the integral prism contraction give a specified augmentation contraction of its tensor-square chain complex. Induction first on $i$ and then on simplex dimension therefore extends the Alexander--Whitney diagonal to a natural equivariant chain map

$W_{Z} \otimes C_{*} (X; Z) ⟶ C_{*} (X; Z) \otimes C_{*} (X; Z) .$

Write $D_{i}$ for its $e_{i}$ -coordinate. The chain-map equation is

$d D_{i} - (- 1)^{i} D_{i} d = (1 + (- 1)^{i} T) D_{i - 1} .$

Every filling takes place in one fixed finite standard-simplex carrier, so this induction makes no arbitrary choice. Reduction modulo two is a natural higher-diagonal system with Alexander--Whitney term. By [F1] and [F3], it computes the same Steenrod-square classes as the fixed mod-two system.

2.1

Derive the signed integral coboundary formula. [F4, step 1.1] For integral cochains $u$ of degree $r$ and $v$ of degree $s$ , define $u ⌣_{i} v = (u \otimes v) D_{i}$ . Evaluating the equation of step 1.1 and the signed tensor differential gives

$δ (u ⌣_{i} v) = (- 1)^{i} δ u ⌣_{i} v + (- 1)^{i + r} u ⌣_{i} δ v - (- 1)^{i} u ⌣_{i - 1} v - (- 1)^{r s} v ⌣_{i - 1} u .$

The convention is $⌣_{- 1} = 0$ . Reducing this equality modulo two gives the identity in [F4], so the integral and mod-two conventions agree exactly.

3.1

Compute the lifted Bockstein representative. [F3, F5, step 2.1] Choose a mod-two cocycle $a$ representing $x$ , and let $c$ be its specified integral lift taking only the values zero and one. Since $δ a = 0$ , there is a unique integral cochain $h$ with $δ c = 2 h$ ; moreover $δ h = 0$ because integral singular cochain groups are torsion-free. Put $i = p - j$ . By [F3], the reduction of $c ⌣_{i} c$ represents $S q^{j} (x)$ . Use its reduction modulo four as the lift in [F5]. Step 2.1 gives

$δ (c ⌣_{i} c) = 2 (- 1)^{i} h ⌣_{i} c + 2 (- 1)^{i + p} c ⌣_{i} h - ((- 1)^{i} + (- 1)^{p}) c ⌣_{i - 1} c .$

After division by two and reduction modulo two, the Bockstein is represented by

$\overset{ˉ}{h} ⌣_{i} a + a ⌣_{i} \overset{ˉ}{h} + ϵ_{j} (a ⌣_{i - 1} a),$

where $ϵ_{j} = 1$ exactly when $i$ and $p$ have the same parity, equivalently when $j$ is even, and $ϵ_{j} = 0$ when $j$ is odd.

4.1

Remove the two lift-error terms. [F3, F4, step 3.1] Both $a$ and $\overset{ˉ}{h}$ are mod-two cocycles. Apply [F4] to $a ⌣_{i + 1} \overset{ˉ}{h}$ :

$δ (a ⌣_{i + 1} \overset{ˉ}{h}) = a ⌣_{i} \overset{ˉ}{h} + \overset{ˉ}{h} ⌣_{i} a .$

Thus the first two terms in step 3.1 form a coboundary. Since $i - 1 = p - (j + 1)$ , [F3] identifies the remaining term with $S q^{j + 1} (x)$ . This proves the displayed parity recurrence.

5.1

Check endpoints, degeneracies, and choice. [F3, F4, F5, step 1.1, step 2.1, step 3.1, step 4.1] For the empty space or zero class, all cochains displayed above are zero. If $p = 0$ , then $j = 0$ , $i = 0$ , and the right side is the prescribed $S q^{1} = 0$ on a degree-zero class. At $j = 0$ , the argument retains $⌣_{p - 1}$ ; at $j = p$ , it has $i = 0$ and $⌣_{- 1} = 0$ , so $S q^{p + 1} (x) = 0$ exactly as stated. Both even and odd $j$ were computed rather than inferred. The integral standard-simplex construction and its reduction retain degenerate singular simplices. The zero/one lift of every value, division of an even integer, and every carrier contraction are specified; [F5] confirms that the cyclic Bockstein lift is choice-free. No AC, converse implication, or unproved integral use of the mod-two identity occurs. ∎

Depends on

Used by

Sq¹ is the mod-two Bockstein Proposition

Dependency tree · two levels

17 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 in Homotopy Theory (standard reference, not scraped)