PropositionStatement: AI-adaptedProof: Literature-sourcedPipeline-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.

Cones preserve chain-homotopy equivalences of arrows

Statement

Let $f : C_{∙} \to D_{∙}$ and $g : C_{∙}^{'} \to D_{∙}^{'}$ be chain maps in an abelian category $A$ . Assume there are chain homotopy equivalences $u : C \to C^{'}$ and $v : D \to D^{'}$ , homotopy inverses $u^{'}$ and $v^{'}$ , and a chain homotopy $t : g u ≃ v f .$ Then the upper-triangular block map $Φ_{n} (y, x) : = (v_{n} (y) - t_{n - 1} (x), u_{n - 1} (x))$ is a chain-homotopy equivalence $Cone (f) \to Cone (g) .$

Facts & Assumptions

Given: Data as in the statement.

[L1]

A chain homotopy equivalence is a chain map with a homotopy inverse (A chain homotopy equivalence).

[L2]

A chain homotopy satisfies the commutator identity between the two maps it connects (A chain homotopy).

[L3]

The cone differential is $d (y, x) = (d^{D} (y) + f (x), - d^{C} (x))$ for $Cone (f)$ , and analogously for $g$ (The mapping cone of a chain map).

[L4]

The cone of a chain map belongs to the cone triangle consisting of the map, the canonical inclusion, and the canonical projection (The cone triangle of a chain map).

[L5]

Morphisms in the homotopy category $K (A)$ are homotopy classes of chain maps (The homotopy category of chain complexes).

[L6]

The Stacks Project, Lemma 13.9.13, states that if $(a, b, c)$ is a morphism between two cone triangles in $K (A)$ and $a, b$ are chain-homotopy equivalences, then $c$ is a chain-homotopy equivalence.

Proof

technique · direct

1.1

By [L2], the homotopy convention gives $g u - v f = d t + t d$ . Using [L3], direct expansion yields $d^{Cone (g)} Φ (y, x) = (v d^{D} y - d t (x) + g u (x), - u d^{C} x) = (v d^{D} y + v f (x) + t d^{C} (x), - u d^{C} x) = Φ d^{Cone (f)} (y, x) .$ Thus $Φ$ is a chain map.

L2L3givenconstructalgebra

2.1

Let $j_{f}, j_{g}$ and $q_{f}, q_{g}$ denote the inclusions and projections in the cone triangles from [L4]. The block formula gives $Φ j_{f} = j_{g} v$ and $q_{g} Φ = u [1] q_{f}$ strictly, while the first square commutes in $K (A)$ because $t : g u ≃ v f$ . Hence $(u, v, [Φ])$ is a morphism from the cone triangle of $f$ to the cone triangle of $g$ in the homotopy category.

L2L4L5step 1.1algebra

3.1

The maps $u$ and $v$ are chain-homotopy equivalences by hypothesis, so [L6] applied to the morphism of cone triangles from step 2.1 shows that $Φ$ is a chain-homotopy equivalence. This is the asserted conclusion.

L1L6step 2.1∎

Depends on

Used by

Dependency tree · two levels

14 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

The Stacks Project, Section 13.9: Cones and termwise split sequences (standard reference, not scraped)