TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-08-31

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 of an identity map is contractible

Statement

For every chain complex $C_{∙}$ , the mapping cone $Cone (1_{C})$ is contractible.

Facts & Assumptions

Given: A chain complex $C_{∙}$ .

[L1]

A complex is contractible exactly when its identity map is null-homotopic (A contractible complex).

[L2]

The cone differential for $1_{C}$ is $d_{n} (y, x) = (d_{n}^{C} (y) + x, - d_{n - 1}^{C} (x))$ (The mapping cone of a chain map).

[L3]

A chain homotopy is a degree-one family whose commutator with the differential is the difference of two chain maps (A chain homotopy).

Proof

technique · direct

1.1

Define $h_{n} : Cone (1_{C})_{n} \to Cone (1_{C})_{n + 1}$ by $h_{n} (y, x) : = (0, y) .$ Using [L2], one computes $d_{n + 1} h_{n} (y, x) = (y, - d_{n}^{C} (y)), h_{n - 1} d_{n} (y, x) = (0, d_{n}^{C} (y) + x) .$

L2givenconstructalgebra

2.1

Adding the two displayed terms yields $d_{n + 1} h_{n} + h_{n - 1} d_{n} = 1_{Cone (1_{C})} .$ Thus [L3] makes $h$ a null-homotopy of the identity, and then [L1] shows that $Cone (1_{C})$ is contractible.

L1L3step 1.1algebra∎

Depends on

Used by

A degreewise split cone sequence with no chain splitting Counterexample
The cone of zero and of the identity Example
The three-cone calculation for a composite chain map Lemma
A chain map is a homotopy equivalence exactly when its cone is contractible 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

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