LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30

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 differential descends to a quotient complex

Statement

Let $S_{∙} ↪ C_{∙}$ be a subcomplex in an abelian category. For every $n$ the differential $d_{n}^{C}$ induces a unique morphism ${\overset{ˉ}{d}}_{n} : C_{n} / S_{n} \to C_{n - 1} / S_{n - 1},$ and these induced morphisms satisfy ${\overset{ˉ}{d}}_{n - 1} {\overset{ˉ}{d}}_{n} = 0$ .

Facts & Assumptions

Given: A subcomplex $S_{∙} ↪ C_{∙}$ with quotient maps $q_{n} : C_{n} \to C_{n} / S_{n}$ .

[L1]

In a subcomplex, the differential restricts to $S_{n} \to S_{n - 1}$ (Subcomplex).

[L2]

A cokernel is universal among arrows vanishing on the given subobject (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

[L3]

In a chain complex, consecutive differentials compose to zero (Chain complex in an abelian category).

Proof

technique · constructive

1.1L1L2givenconstruct

By [L1], the composite $q_{n - 1} d_{n}^{C}$ kills $S_{n}$ , because $d_{n}^{C} (S_{n})$ lands in $S_{n - 1}$ and $q_{n - 1}$ kills $S_{n - 1}$ . Hence [L2] gives a unique map ${\overset{ˉ}{d}}_{n} : C_{n} / S_{n} \to C_{n - 1} / S_{n - 1}$ with ${\overset{ˉ}{d}}_{n} q_{n} = q_{n - 1} d_{n}^{C} .$

2.1L2L3step 1.1algebradischarge-construct∎

Composing the identity from step 1.1 twice and using [L3], ${\overset{ˉ}{d}}_{n - 1} {\overset{ˉ}{d}}_{n} q_{n} = q_{n - 2} d_{n - 1}^{C} d_{n}^{C} = 0.$ Since $q_{n}$ is epic as a cokernel map, ${\overset{ˉ}{d}}_{n - 1} {\overset{ˉ}{d}}_{n} = 0$ .

Depends on

Used by

Quotient complex Definition
E zero is the associated graded complex Proposition
The associated graded of a filtered complex is a bigraded complex Proposition

Dependency tree · two levels

7 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

Charles A. Weibel, Chapter 1 of An Introduction to Homological Algebra (standard reference, not scraped)