PropositionStatement: 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.

Steenrod normalization, instability, suspension, and top square

Statement

For $x \in H^{n} (X; F_{2})$ ,

S q^{0} x = x, S q^{k} x = 0 if k > n, S q^{n} x = x ⌣ x .

The same assertions hold relatively. On reduced cohomology of based CW complexes, every square commutes with the standard cohomology suspension:

S q^{k} (σ x) = σ (S q^{k} x) .

Facts & Assumptions

Given: A mod-two class $x = [a]$ of degree $n$ and an integer $k$ ; for the suspension calculation put $j = n - k$ .

[F1]

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

[F2]

For $0 \leq k \leq n$ , $S q^{k} [a]$ is represented by $a ⌣_{n - k} a$ , and its outside-range values are zero (Steenrod squares from cup-i).

[F3]

Cup- $0$ is the ordinary cup product, negative cup indices are zero, and the products restrict to relative cochains (Higher cup-i products).

[F4]

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

[F5]

In the pair sequence the connector sends $[a]$ to $[δ \tilde{a}]$ for any cochain extension $\tilde{a}$ (Long exact sequence of a pair in singular cohomology).

[F6]

For a well-pointed based space $(X, x_{0})$ , use the reduced cone $C X = (X \times I) / (X \times {1} \cup {x_{0}} \times I)$ and define its reduced suspension as the quotient $Σ X = C X / X$ , where $X$ is the height-zero cone base.

[F7]

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

[F8]

Homotopic maps induce the same singular-cohomology map for every abelian coefficient group (Homotopic maps induce equal maps in singular cohomology).

[F9]

Singular cohomology satisfies excision for a closed set contained in the interior of the relative subspace (Excision for singular cohomology).

Proof

Proof technique: an explicit normalized cup- $i$ system and a cone-pair cochain calculation.

1.1

First prove $S q^{0} = id$ . [F1, F2] Use the standard face-formula system of Medina--Mardones, Definition 7 and Theorem 10 (printed pages 8--9). On an $m$ -simplex $s$ it is

D_{i}^{s t d} (s) = \sum_{U} d_{U^{0}} s \otimes d_{U^{1}} s,

where $U = {u_{1} < \dots < u_{m - i}} \subseteq {0, \dots, m}$ and $U^{0}, U^{1}$ partition $U$ according to the parity of $u_{r} - r$ . Its proof uses only the face identities, so the same formula applies to the simplicial set of singular simplices, including its degenerate simplices. Example 8 identifies $D_{0}^{s t d}$ with Alexander--Whitney, while for $i = m$ the only index set is $U = \emptyset$ , giving

D_{m}^{s t d} (s) = s \otimes s .

Thus, for an $n$ -cochain $a$ and every singular $n$ -simplex $s$ , $(a ⌣_{n} a) (s) = a (s)^{2} = a (s)$ in $F_{2}$ . By [F2] this cochain represents $S q^{0} [a]$ , and [F1] permits the computation with this normalized system. Hence $S q^{0} x = x$ .

1.2

Instability and the top square follow at the two definition endpoints. [F2, F3] If $k > n$ , [F2] declares $S q^{k} x = 0$ . If $k = n$ , its representing cochain is $a ⌣_{0} a$ , which is the ordinary cup product by [F3]. Therefore $S q^{n} x = x ⌣ x$ . The same argument uses the relative products when $x$ is relative.

1.3

Represent the cone-pair connector without a choice. [F5, F6] Extend the cocycle $a$ from the cone base $X \subset C X$ to a cochain $b$ on $C X$ by setting it to zero on every singular simplex not lying in $X$ . Then $c : = δ b$ vanishes on chains in $X$ and so is a relative cocycle in $C^{n + 1} (C X, X; F_{2})$ . By [F5], $[c] = \partial [a]$ . This extension is a specified function, not an application of AC.

2.1

The connector commutes with every square. [F2, F3, F4, F5, step 1.3] For $0 \leq k \leq n$ , set $j = n - k$ and define

b^{'} : = b ⌣_{j + 1} δ b + b ⌣_{j} b .

Because $b ∣_{X} = a$ and $(δ b) ∣_{X} = 0$ , its restriction is $b^{'} ∣_{X} = a ⌣_{j} a$ , a representative of $S q^{k} [a]$ . Applying [F4] twice and using $δ^{2} b = 0$ gives

\begin{aligned} δ b^{'} & = δ b ⌣_{j + 1} δ b + b ⌣_{j} δ b + δ b ⌣_{j} b \\ + δ b ⌣_{j} b + b ⌣_{j} δ b + b ⌣_{j - 1} b + b ⌣_{j - 1} b \\ = δ b ⌣_{j + 1} δ b . \end{aligned}

The last cochain is the relative representative for $S q^{k} [c]$ , since $c$ has degree $n + 1$ . Hence [F5] gives $\partial S q^{k} [a] = S q^{k} \partial [a]$ . There is one further endpoint: if $k = n + 1$ , then $S q^{n + 1} [a] = 0$ , while $b ⌣_{0} δ b$ restricts to zero on $X$ and

δ (b ⌣_{0} δ b) = δ b ⌣_{0} δ b

by the ordinary mod-two Leibniz rule, the $i = 0$ case of [F4]. Thus the top square of $[c]$ is also zero. For $k < 0$ or $k > n + 1$ , both sides are zero by [F2]; negative cup indices in the preceding calculation are zero by [F3].

3.1

The cone-pair connector is the reduced suspension after the quotient comparison. [F5, F6, F7, F8, F9, step 2.1] Take a based CW complex. If its basepoint lies inside a positive-dimensional open cell, radially subdivide that characteristic disk there and keep the higher attaching maps; this finite refinement makes it a vertex without changing the based space. For every nonbasepoint $n$ -cell of $X$ , its product with the open height interval in [F6] gives an $(n + 1)$ -cell of $C X$ ; the height-zero cells form the copy of $X$ , while $X \times {1}$ and the basepoint track collapse to one vertex. The product characteristic disks supply the attaching maps, and each has finite boundary-cell support because its $X$ -cell does. Their quotient map-out test and the CW weak topology give the cone its CW structure, with $X$ a closed subcomplex. The cellwise radial collar of this subcomplex gives an open neighborhood $V$ that strongly deformation retracts onto $X$ : extend the collar and its radial flow over each characteristic disk, and assemble the compatible extensions using the CW weak topology. Since $X \subset V$ is the entire collapsed fibre of $q : C X \to Σ X$ , $V$ is saturated; hence $q (V)$ is open and the flow descends to a retraction onto the quotient vertex.

The pair sequences and [F8] make $H^{*} (V, X; F_{2})$ and $H^{*} (q (V), {*}; F_{2})$ zero. Restriction of cochains gives short exact sequences for the triples $(C X, V, X)$ and $(Σ X, q (V), {*})$ ; zero-extension proves their surjectivity. Their long exact sequences therefore identify the relative groups for $X$ and $V$ , and for ${*}$ and $q (V)$ . Apply [F9] with removed sets $X$ and ${*}$ , respectively. After removal the map $q : C X \to Σ X$ is a homeomorphism of the two remaining pairs, so the excision squares give an isomorphism $q^{*} : H^{*} (Σ X, {*}; F_{2}) \overset{≅}{\to} H^{*} (C X, X; F_{2}) .$ Thus the standard reduced suspension is $(q^{*})^{- 1}$ followed by the cone-pair connector [F5]. The quotient maps are natural, and [F7] makes squares natural for them. Step 2.1 therefore yields $S q^{k} σ = σ S q^{k}$ . Empty or one-point reduced groups, the zero class, degree zero, and degenerate singular simplices were all included above, and no choice principle was used. ∎

Depends on

Used by

Top squares do not determine lower squares Counterexample
Total Steenrod square Definition
Wu classes of a closed manifold Definition
Bockstein detects integral two-torsion in real projective space Example
Steenrod squares on complex projective space mod two Example
Steenrod squares on real projective space Example
Wu classes of a closed surface Example
Sq¹ is the mod-two Bockstein Proposition
Adem relations for Steenrod squares Theorem
Cartan formula for Steenrod squares Theorem

Dependency tree · two levels

18 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)