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.

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

Statement

Assume AC. Let $u \in H^{1} ({R P}^{2}; F_{2})$ and $v \in H^{1} ({R P}^{4}; F_{2})$ be the nonzero degree-one generators; viewed on the product by the two projection pullbacks. They generate the mod-two cohomology of ${R P}^{2} \times {R P}^{4}$ with relations $u^{3} = 0 = v^{5}$ . For $z = β_{Z} (u v) \in H^{3} ({R P}^{2} \times {R P}^{4}; Z)$ one has $S q_{Z}^{3} (z) = β_{Z} (u v^{4}) \neq 0.$ Here the integral operation is defined by $S q_{Z}^{3} : = β_{Z} S q^{2} ρ_{2}$ .

Facts & Assumptions

Given: AC, the product $Y = {R P}^{2} \times {R P}^{4}$ , the projection pullbacks $u, v$ of its degree-one generators, and $z = β_{Z} (u v)$ . The operation here is defined by $S q_{Z}^{3} = β_{Z} S q^{2} ρ_{2}$ .

[F1]

For every space and nonnegative degree, $ρ_{2} β_{Z} = S q^{1}$ (Reduction of the integral Bockstein is the first Steenrod square).

[F2]

Under AC, $H^{*} ({R P}^{\infty}; F_{2}) = F_{2} [a]$ , and restriction to ${R P}^{m}$ is an isomorphism through degree $m$ (Mod-two cohomology ring of infinite real projective space).

[F3]

The finite space ${R P}^{m}$ has one cell in degrees $0, \dots, m$ , with cellular incidence numbers zero or two (Real projective space cellular homology and the pinch map). Cellular homology with any coefficient group computes singular homology (Cellular homology computes singular homology). Under AC, cohomology over a field is the full dual of homology over that field (Cohomology over a field is dual to homology over that field).

[F4]

Under AC the cohomological Künneth cross product is a graded-ring isomorphism over a PID if every homology group of one factor is finite free over that PID (Cohomological Kunneth cross product is a ring isomorphism).

[F5]

Squares are additive and natural; $S q^{0} x = x$ , $S q^{k} x = 0$ for $k > ∣ x ∣$ , and $S q^{∣ x ∣} x = x^{2}$ ; Cartan computes squares of products (Steenrod squares are well-defined and natural, Steenrod normalization, instability, suspension, and top square, Cartan formula for Steenrod squares).

[A1]

AC is assumed (The Axiom of Choice) through [F2], field duality in [F3] and the additive Künneth isomorphism in [F4]. The Bockstein and finite square calculations use no additional choices.

Proof

technique · direct

1.1

Reduce the cellular incidence numbers in [F3] modulo two. The cellular chain complex of ${R P}^{m}$ is then $F_{2}$ in degrees $0, \dots, m$ , zero elsewhere, with zero differential. Thus its mod-two singular homology is one-dimensional in that range and zero above $m$ . Field duality gives the same dimensions and vanishing for cohomology. By [F2], restriction sends $a^{j}$ to the nonzero power $a_{m}^{j}$ for $0 \leq j \leq m$ ; restriction preserves products. Higher powers vanish by the just-proved cohomological vanishing. Therefore the finite ring is exactly $F_{2} [a_{m}] / (a_{m}^{m + 1})$ .

F2F3A1algebra

1.2

For a degree-one class $t$ , [F5] gives $S q^{0} t = t$ , $S q^{1} t = t^{2}$ , and $S q^{i} t = 0$ for $i > 1$ . Repeated Cartan says that in $S q^{i} (t^{j})$ only choices of $i$ among the $j$ factors to receive $S q^{1}$ contribute; each contributes $t^{j + i}$ . Thus $S q^{i} (t^{j}) = (\binom{j}{i}) t^{j + i}$ , with the binomial coefficient reduced modulo two. This is a finite product computation, valid directly for the classes $u, v$ on $Y$ . In particular $S q^{1} (t^{2}) = 0$ , $S q^{2} (t^{2}) = t^{4}$ , and $S q^{1} (t^{4}) = 0$ . [F5, algebra] 2.1 The homology groups of both finite projective factors are finite free over $F_{2}$ by step 1.1, so the full hypothesis of [F4] holds. Its cross-product ring isomorphism gives $H^{*} (Y; F_{2}) = F_{2} [u, v] / (u^{3}, v^{5})$ , with basis $u^{i} v^{j}$ for $0 \leq i \leq 2$ , $0 \leq j \leq 4$ . In particular $u v$ , $u v^{4}$ and $u^{2} v^{4}$ are nonzero. The two summands $u^{2} v$ and $u v^{2}$ are distinct basis elements.

step 1.1F4A1algebra

3.1

Cartan gives $S q^{1} (u v) = u^{2} v + u v^{2}$ . Also $S q^{2} (u^{2} v) = u^{4} v + 0 + 0 = 0$ since $u^{3} = 0$ , whereas $S q^{2} (u v^{2}) = 0 + 0 + u v^{4} = u v^{4}$ . Additivity therefore gives $S q^{2} (u^{2} v + u v^{2}) = u v^{4}$ .

step 2.1step 1.2F5algebra

4.1

By [F1], $ρ_{2} z = S q^{1} (u v) = u^{2} v + u v^{2}$ , which is nonzero by step 2.1, so $z$ is also nonzero. Step 3.1 gives $S q^{2} ρ_{2} z = u v^{4}$ , and the specified definition implies $S q_{Z}^{3} (z) = β_{Z} (u v^{4})$ . Finally $ρ_{2} β_{Z} (u v^{4}) = S q^{1} (u v^{4}) = u^{2} v^{4} + u S q^{1} (v^{4}) = u^{2} v^{4} \neq 0$ by steps 2.1 and 1.2 and Cartan. A zero integral class would have zero reduction, so this proves the claimed integral nonvanishing without asserting injectivity of reduction.

step 2.1step 1.2step 3.1F1F5given∎

Source notes

Compare Ji, §3.2.4 and Proposition 3.12, printed pp. 11–12, for the $d_{3}$ computation on ${R P}^{2} \times {R P}^{4}$ and the description of $d_{3}$ as the integral operation; the particular Bockstein class displayed here supplies the local calculation.

Depends on

Used by

A nonzero d-three in the K-AHSS for RP-two times RP-four Example

Dependency tree · two levels

50 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

Caleb Ji, The Atiyah–Hirzebruch Spectral Sequence, §3.2.4 and Proposition 3.12, printed pp. 11–12 (standard reference, not scraped)