TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-09-01

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 cone long exact sequence

Statement

For every chain map $f : C_{∙} \to D_{∙}$ in an abelian category, there is an exact sequence $\dots \to H_{n} (C) \overset{H_{n} (f)}{\to} H_{n} (D) \to H_{n} (Cone (f)) \to H_{n - 1} (C) \overset{H_{n - 1} (f)}{\to} H_{n - 1} (D) \to \dots .$

Facts & Assumptions

Given: A chain map $f : C_{∙} \to D_{∙}$ .

[L1]

The canonical cone sequence $0 \to D_{∙} \to Cone (f)_{∙} \to C [1]_{∙} \to 0$ is degreewise split short exact (The canonical mapping-cone sequence is degreewise split short exact).

[L2]

Homology of a shift satisfies $H_{n} (C [1]) ≅ H_{n - 1} (C)$ (Homology of a shift is shifted homology).

[L3]

A chain map induces a well-defined map on homology (A chain map induces a well-defined map on homology).

[L4]

Every short exact sequence of complexes yields a long exact homology sequence (The long exact sequence in homology).

[L5]

The cone differential on $D_{n} \oplus C_{n - 1}$ is $d (y, x) = (d_{D} y + f (x), - d_{C} x)$ (The mapping cone of a chain map).

[L6]

In the weaker snake construction, the connecting morphism is obtained from a pullback $P$ with maps $π : P \to \ker (γ)$ and $r : P \to U$ and is characterized by $δ π = q_{α} r$ (Snake lemma under the weaker Stacks hypotheses).

Proof

technique · direct

1.1L1L4givenconstruct

Apply [L4] to the short exact sequence from [L1]. This gives an exact sequence $\dots \to H_{n} (D) \to H_{n} (Cone (f)) \to H_{n} (C [1]) \overset{δ_{n}}{\to} H_{n - 1} (D) \to \dots .$

2.1L1L2L3L5L6step 1.1constructalgebra∎

Apply the weaker snake construction [L6] to the quotient-kernel diagram of the cone sequence from [L1] in degree $n + 1$ . Let $z_{C} : Z_{n} (C) \to C_{n}$ be the cycle inclusion and let $s : Z_{n} (C) \to Cone (f)_{n + 1}$ have components $(0, z_{C})$ . Its projection to $C [1]_{n + 1} = C_{n}$ is $z_{C}$ , so $s$ and the quotient $q_{C} : Z_{n} (C) \to H_{n} (C)$ induce a morphism $t : Z_{n} (C) \to P$ into the pullback used in [L6], with $π t = q_{C}$ . By [L5], $d^{Cone (f)} s = j_{n} f_{n} z_{C},$ and the defining equation for $r$ in the snake construction therefore gives $r t = Z_{n} (f)$ . Consequently [L6] yields $δ_{n + 1} q_{C} = δ_{n + 1} π t = q_{D} r t = q_{D} Z_{n} (f) = H_{n} (f) q_{C} .$ The last equality is the defining square for [L3]. Since $q_{C}$ is epic, $δ_{n + 1} = H_{n} (f)$ . Reindexing step 1.1 by [L2] gives the displayed cone long exact sequence.

Depends on

Used by

Dependency tree · two levels

29 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)
The Stacks Project, Section 12.13: Complexes (standard reference, not scraped)