LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)

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.

The total differential squares to zero

Statement

For the direct-sum totalisation of an anticommuting homological double complex, $d_{n - 1} d_{n} = 0$ for every integer $n$ .

Facts & Assumptions

[F1]

Direct sum total complex of a double complex defines $d_{n}$ by its composites with the diagonal coproduct injections.

[F2]

Homological double complex gives $h^{2} = 0$ , $v^{2} = 0$ and the indexed anticommuting-square identity.

[F3]

Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations gives uniqueness of an arrow out of a coproduct from its composites with all injections.

Proof

Given: Such a double complex $C$ and its existing diagonal coproducts $T_{n}$ , with injections $ι_{p, q}^{n}$ and differentials $d_{n}$ .

1.1

Fix $n$ and $p + q = n$ . Substitute the defining formula for $d$ twice and distribute composition over addition. This gives $d_{n - 1} d_{n} ι_{p, q}^{n} = ι_{p - 2, q}^{n - 2} h_{p - 1, q} h_{p, q} + ι_{p - 1, q - 1}^{n - 2} (v_{p - 1, q} h_{p, q} + h_{p, q - 1} v_{p, q}) + ι_{p, q - 2}^{n - 2} v_{p, q - 1} v_{p, q}$ . Each term is an arrow from $C_{p, q}$ to $T_{n - 2}$ .

F1algebra

2.1

The first and last composites vanish by the two square-zero axioms; the middle parenthesis vanishes by anticommutation. Therefore $d_{n - 1} d_{n} ι_{p, q}^{n} = 0$ for every $p + q = n$ , including when any of the source or target components is zero.

F2step 1.1

3.1

The zero arrow $T_{n} \to T_{n - 2}$ has these same composites with every injection. Coproduct uniqueness therefore gives $d_{n - 1} d_{n} = 0$ . Since $n$ was arbitrary, all chain identities hold. The argument also covers an all-zero or a single-supported diagonal and uses no exactness of infinite coproducts or representative selections.

F3step 2.1∎

Depends on

Used by

Sum and product totalisations can differ on infinite diagonals Counterexample
Row and column filtrations of a first quadrant double complex Definition
Sum and product totalisations agree on finite diagonal double complexes Proposition

Cited to discharge well-definedness by Direct sum total complex of a double complex.

Dependency tree · two levels

6 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

Stacks Project, Definition 12.18.3; direct verification with translated signs (standard reference, not scraped)