LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Reduction of the integral Bockstein is the first Steenrod square

Statement

For the integral Bockstein $β_{Z} : H^{n} (X; F_{2}) \to H^{n + 1} (X; Z)$ of the coefficient sequence $0 \to Z \overset{2}{\to} Z \to F_{2} \to 0$ , reduction modulo two satisfies $ρ_{2} β_{Z} (x) = S q^{1} (x)$ for every space $X$ , every $n \geq 0$ and every $x \in H^{n} (X; F_{2})$ . No choice principle is needed.

Facts & Assumptions

[F1]

For the cyclic coefficient sequences, least nonnegative residues give a specified cochain lift without AC. If $c \in C^{n} (X; F_{2})$ is a cocycle, its integral residue lift $\tilde{c}$ has $δ \tilde{c} = 2 a$ for a unique integral cochain $a$ , and the resulting class is the integral Bockstein of $0 \to Z \overset{2}{\to} Z \to F_{2} \to 0$ once its independence of the cocycle representative is checked (Bockstein connecting operation).

[F2]

The mod-two Bockstein $β$ of $0 \to F_{2} \overset{2}{\to} Z / 4 \to F_{2} \to 0$ satisfies $S q^{1} (x) = β (x)$ for every $x \in H^{n} (X; F_{2})$ , and the identification requires no AC (Sq^1 is the mod-two Bockstein).

Proof

technique · direct

Given: An integer $n \geq 0$ , a class $x \in H^{n} (X; F_{2})$ , and a mod-two cocycle $c$ representing $x$ .

1.1

Lift $c$ coefficientwise to the integral cochain $\tilde{c}$ given by the least nonnegative residues. Then $δ \tilde{c}$ is coefficientwise divisible by $2$ because $δ c = 0$ modulo two, so there is a unique integral cochain $a$ with $δ \tilde{c} = 2 a$ . Moreover $δ a = 0$ , since $2 δ a = δ^{2} \tilde{c} = 0$ in the torsion-free group of integral cochains.

F1given

1.2

Reducing $\tilde{c}$ modulo four gives a $Z / 4$ -cochain whose image modulo two is $c$ and whose coboundary is the reduction of $2 a$ , namely $2 a$ modulo four; hence the mod-two Bockstein of the sequence $0 \to F_{2} \to Z / 4 \to F_{2} \to 0$ assigns to $x$ the class of $δ (\tilde{c}) / 2 = a$ modulo two.

F1given

2.1

The residue construction descends without any choice. If $c^{'} = c + δ u$ modulo two, let ${\tilde{c}}^{'}, \tilde{c}, \tilde{u}$ be their integral residue lifts. The integral cochain ${\tilde{c}}^{'} - \tilde{c} - δ \tilde{u}$ reduces to zero modulo two, so it equals $2 h$ for a unique integral cochain $h$ . If $δ {\tilde{c}}^{'} = 2 a^{'}$ , applying $δ$ gives $2 a^{'} = 2 a + 2 δ h$ , hence $a^{'} = a + δ h$ . Thus $[a]$ depends only on $x$ , using no simultaneous selection from fibres. Reducing $a$ modulo two gives the mod-two Bockstein by step 1.2, so $ρ_{2} β_{Z} (x) = β (x) = S q^{1} (x)$ by [F2].

F1F2step 1.1step 1.2

3.1

Steps 1.1, 1.2 and 2.1 prove the stated identity for every space and every degree; both the residue lift and the comparison cochain $h$ are uniquely specified coefficientwise, so no choice principle is used.

step 2.1∎

Source notes

Compare Hatcher, §3.E, printed pp. 303–305, for the integral Bockstein $\tilde{β}$ , the reduction identity $β = ρ \circ \tilde{β}$ and the derivation property.

Depends on

Used by

A Bockstein class on RP-two times RP-four has nonzero integral Sq-three Lemma

Dependency tree · two levels

7 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

Allen Hatcher, Algebraic Topology, §3.E, printed pp. 303–305 (standard reference, not scraped)