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

Natural higher diagonal approximations

Statement

Work over $F_{2}$ . For every space $X$ there are natural maps of degree $i$

D_{i}^{X} ⁣ : C_{n} (X) ⟶ (C_{*} (X) \otimes C_{*} (X))_{n + i} (i \geq 0)

such that $D_{0}$ is the Alexander--Whitney diagonal, and, with $T (a \otimes b) = b \otimes a$ and $D_{- 1} = 0$ ,

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

If $A \subseteq X$ , then $D_{i} (C_{*} (A)) \subseteq C_{*} (A) \otimes C_{*} (A)$ . Moreover, two such carried systems with the same $D_{0}$ are coherently homotopic: there are natural degree- $(i + 1)$ maps $K_{i}$ , with $K_{- 1} = 0$ , for which

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

Facts & Assumptions

Given: Ordinary unnormalized singular chains over $F_{2}$ .

[F1]

The Alexander--Whitney diagonal is a natural chain map, is finite on each generator, and requires no chosen filling (Alexander–Whitney map and diagonal approximation).

[F2]

Alexander--Whitney and the signed shuffle are natural augmentation- preserving chain-homotopy inverses, without AC (Alexander--Whitney and shuffle are natural chain-homotopy inverses).

Proof

technique · induction on the resolution degree and simplex dimension

1.1

Fix an explicit contraction on every standard diagonal carrier. [F2] The straight-line contraction of $Δ^{n} \times Δ^{n}$ to $(v_{0}, v_{0})$ has the standard finite singular-prism chain homotopy $s_{n}$ . Transport $s_{n}$ through the specified shuffle and Alexander--Whitney maps and add the specified homotopy from their composite to the identity. This gives a fixed map $h_{n}$ on $C_{*} (Δ^{n}) \otimes C_{*} (Δ^{n})$ satisfying

d h_{n} + h_{n} d = 1 - η ϵ,

where $η ϵ$ projects to the tensor of the distinguished vertex. Every map in this formula is an explicit finite sum, so choosing all $h_{n}$ uses no choice principle.

2.1

Construct $D_{i}$ recursively. [F1, step 1.1] Let $W$ be the free $F_{2} [C_{2}]$ -resolution with one generator $e_{i}$ in each degree and $d e_{i} = (1 + T) e_{i - 1}$ for $i > 0$ . Put $D_{0} = AW Δ_{#}$ as in [F1]. Suppose lexicographically that $D_{i}$ is known on lower-dimensional simplices and that $D_{i - 1}$ is known. For the identity simplex $ι_{n}$ set

z_{i, n} : = D_{i} (d ι_{n}) + (1 + T) D_{i - 1} (ι_{n}) .

The earlier recursion gives $d z_{i, n} = 0$ : the two copies of $(1 + T) D_{i - 1} (d ι_{n})$ cancel and $(1 + T)^{2} = 0$ over $F_{2}$ . Its positive-degree augmentation is zero, so step 1.1 gives $d (h_{n} z_{i, n}) = z_{i, n}$ . Define $D_{i} (ι_{n}) = h_{n} z_{i, n}$ and, for a singular simplex $σ ⁣ : Δ^{n} \to X$ , define $D_{i}^{X} (σ) = (σ_{#} \otimes σ_{#}) D_{i} (ι_{n})$ . The equation $d D_{i} + D_{i} d = (1 + T) D_{i - 1}$ now holds on each generator and hence on all chains.

3.1

The construction is natural and preserves subspaces. [step 2.1] Postcomposition sends the formula for a simplex $σ$ to the formula for $f σ$ , proving naturality. If the image of $σ$ lies in $A$ , both tensor factors in step 2.1 lie in $C_{*} (A)$ , proving the carrier assertion. This also includes degenerate singular simplices; none was quotiented out.

4.1

The same induction one degree higher proves coherent uniqueness. [step 1.1, step 2.1, step 3.1] For two systems, subtract their recursive equations and suppose that $K_{i - 1}$ is known while $K_{i}$ is already defined on every chain below the current dimension. On the identity simplex $ι_{n}$ put

ω = (D_{i} - D_{i}^{'}) (ι_{n}) + (1 + T) K_{i - 1} (ι_{n}) + K_{i} (d ι_{n}) .

The recursion $d (D_{i} - D_{i}^{'}) + (D_{i} - D_{i}^{'}) d = (1 + T) (D_{i - 1} - D_{i - 1}^{'})$ for the two systems, the induction hypothesis for $K_{i - 1}$ , and the induction hypothesis for $K_{i}$ on the lower-dimensional chain $d ι_{n}$ give $d ω = 0$ : the two copies of $(1 + T) d K_{i - 1} (ι_{n})$ cancel, while $(D_{i} - D_{i}^{'}) (d ι_{n}) + (1 + T) K_{i - 1} (d ι_{n})$ and the explicit $d K_{i} (d ι_{n})$ agree by that second induction hypothesis. The element $ω$ is therefore a cycle in the same standard carrier, and it has positive degree, so applying $h_{n}$ fills it and defines $K_{i} (ι_{n})$ ; postcomposition extends it naturally. Taking the boundary of that defining filling gives exactly $D_{i} - D_{i}^{'} = d K_{i} + K_{i} d + (1 + T) K_{i - 1}$ . ∎

Depends on

Used by

Higher cup-i products Definition
Bockstein parity recurrence for Steenrod squares Lemma
Cartan coherence for higher diagonals Lemma
Finite-cellular cyclic squares agree with singular cup-i squares Lemma
Cup-i coboundary identity Theorem
Steenrod squares are well-defined and natural Theorem

Dependency tree · two levels

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