ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 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 detects integral two-torsion in real projective space

Example

Assume AC. Let $n \geq 2$ be an integer and let $a \in H^{1} ({R P}^{n}; F_{2})$ be the unique nonzero class. For the integral and mod-two coefficient sequences, respectively, write

$β_{Z} : H^{1} ({R P}^{n}; F_{2}) ⟶ H^{2} ({R P}^{n}; Z), β_{2} : H^{1} ({R P}^{n}; F_{2}) ⟶ H^{2} ({R P}^{n}; F_{2}) .$

Then $β_{Z} (a)$ generates $H^{2} ({R P}^{n}; Z) ≅ Z / 2$ , and

$β_{2} (a) = S q^{1} (a) = a^{2} .$

In particular, $a^{2}$ is the nonzero element of $H^{2} ({R P}^{n}; F_{2})$ .

Facts & Assumptions

Given: An integer $n \geq 2$ , the space $X = {R P}^{n}$ , and its unique nonzero class $a \in H^{1} (X; F_{2})$ .

[F1]

For $0 \to Z \overset{2}{\to} Z \to F_{2} \to 0$ , Bockstein connecting operation represents the integral Bockstein by lifting a cocycle $c$ to an integral cochain $\hat{c}$ , writing $δ \hat{c} = 2 h$ , and taking $[h]$ .

[F2]

This Bockstein class is independent of the lift and representative by The Bockstein is independent of lift and representative.

[F3]

The choice-free integral clause of Real projective space cellular homology and the pinch map gives, for $n \geq 2$ ,

$H_{0} (X; Z) = Z, H_{1} (X; Z) = Z / 2, H_{2} (X; Z) = 0.$

[F4]

Under AC, Topological universal coefficient short exact sequence for cohomology gives the integral cohomology sequence with its Ext term computed in the first variable.

[F5]

Under AC, Mod-two cohomology ring of infinite real projective space gives

$H^{*} ({R P}^{\infty}; F_{2}) ≅ F_{2} [a_{\infty}], ∣ a_{\infty} ∣ = 1,$

and restriction to $X = {R P}^{n}$ is an isomorphism through degree $n$ . For $n \geq 2$ it sends $a_{\infty}$ to $a$ and $a_{\infty}^{2}$ to $a^{2}$ , so $a$ and $a^{2}$ are the unique nonzero classes in degrees one and two.

[F6]

The mod-two Bockstein is $S q^{1}$ by Sq^1 is the mod-two Bockstein.

[F7]

The top-square identity in Steenrod normalization, instability, suspension, and top square says $S q^{r} (x) = x ⌣ x$ for a class $x$ of degree $r$ .

[A1]

The Axiom of Choice is assumed for the present combined argument. [F1], [F2], [F4], and [F5] are cited under their published AC hypotheses; the integral cellular calculation in [F3], the canonical residue lift, and the finite Ext calculations below introduce no further choice.

Verification

technique · direct lift-and-divide calculation

1.1givenF1F2

Choose a mod-two singular cocycle $c$ representing $a$ . Let $\hat{c}$ be its valuewise lift with values zero or one. Since $c$ is a cocycle, every value of $δ \hat{c}$ is even. Hence there is a unique integral cochain $h$ with $δ \hat{c} = 2 h$ , and [F1]--[F2] give $β_{Z} (a) = [h]$ .

1.2F5F6F7

For the mod-two coefficient sequence, the Bockstein is the square of $a$ . Indeed, [F6] and the degree-one instance of [F7] give

$β_{2} (a) = S q^{1} (a) = a ⌣ a = a^{2} .$

Since $n \geq 2$ , [F5]'s restriction isomorphism in degree two carries the nonzero polynomial class $a_{\infty}^{2}$ to $a^{2}$ , so $a^{2}$ is the unique nonzero degree-two mod-two class.

1.3F3F4

The two required integral cohomology groups follow from the A-level cellular calculation. In UCT degree one, the outside terms are

${Ext}_{Z}^{1} (Z, Z) = 0, {Hom}_{Z} (Z / 2, Z) = 0.$

The first equality holds because $Z$ is free, and the second because $Z$ is torsion-free. Hence $H^{1} (X; Z) = 0$ . In degree two, the Hom term is zero because $H_{2} (X; Z) = 0$ , while the free resolution

$0 ⟶ Z \overset{2}{\to} Z ⟶ Z / 2 ⟶ 0$

computes ${Ext}_{Z}^{1} (Z / 2, Z)$ as the cokernel of multiplication by two on $Z$ , namely $Z / 2$ . Exactness therefore gives $H^{2} (X; Z) ≅ Z / 2$ .

2.1F5step 1.1step 1.3

The integral class $[h]$ is nonzero. Suppose instead that $h = δ k$ for an integral degree-one cochain $k$ . Then

$δ (\hat{c} - 2 k) = 2 h - 2 δ k = 0.$

By $H^{1} (X; Z) = 0$ in step 1.3, there is an integral degree-zero cochain $ℓ$ with $\hat{c} - 2 k = δ ℓ$ . Reduction modulo two would give $c = δ (ℓ m o d 2)$ , contrary to the nonzero class $a = [c]$ in [F5].

3.1step 1.3step 2.1

The integral Bockstein class is a generator. Indeed, step 1.3 identifies $H^{2} (X; Z)$ with a group having exactly one nonzero element, step 2.1 makes $β_{Z} (a)$ that element and therefore a generator of its integral two-torsion.

4.1F3F4F5A1step 1.1step 1.2step 1.3step 2.1step 3.1∎

The endpoint and excluded cases introduce no missing assertion. The endpoint $n = 2$ is included: the two degree-two groups in step 1.3 and [F5] are still nonzero, whereas $n = 0, 1$ are excluded because the promised integral degree-two target is absent. The zero degree-one class is explicitly excluded because its Bockstein is zero and cannot generate. Real projective spaces are nonempty, and their point and degree-zero cases do not enter the claim. The calculation uses ordinary singular cochains, including degenerate simplices, and makes no cellular-to-singular cochain identification. AC occurs through [F1], [F2], [F4], and [F5]; the zero/one lift itself is canonical. No biconditional or converse is asserted.

Depends on

Used by

Top squares do not determine lower squares Counterexample

Dependency tree · two levels

34 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

Hatcher, Algebraic Topology (standard reference, not scraped)