PropositionStatement: 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.

Isomorphic chain maps have isomorphic cones

Statement

Suppose $\begin{array}{ccc} C_{∙} & \overset{f}{\to} & D_{∙} \\ ↓_{\sim}^{u} & ↓_{\sim}^{v} \\ C_{∙}^{'} & \overset{f^{'}}{\to} & D_{∙}^{'} \end{array}$ is a strictly commuting square of chain maps with vertical chain isomorphisms. Then $Cone (f)$ and $Cone (f^{'})$ are isomorphic as chain complexes.

Facts & Assumptions

Given: A commuting square as displayed in the statement.

[L1]

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

[L2]

A chain map commutes with differentials (Chain map).

[L3]

Identities and composites of chain maps are chain maps (Identities and composites of chain maps are chain maps).

Proof

technique · direct

1.1

Define $Φ_{n} : Cone (f)_{n} \to Cone (f^{'})_{n}$ by $Φ_{n} (y, x) : = (v_{n} (y), u_{n - 1} (x)) .$ Using the commutative square together with [L1] and [L2], one gets $d^{Cone (f^{'})} Φ = Φ d^{Cone (f)},$ so $Φ$ is a chain map.

L1L2givenconstructalgebra

2.1

Because $u$ and $v$ are chain isomorphisms, their inverses are again chain maps by [L3], and the same block-diagonal formula with $u^{- 1}$ and $v^{- 1}$ defines the inverse chain map to $Φ$ . Hence $Φ$ is a chain isomorphism.

L3step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

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

Charles A. Weibel, Chapter 1 of An Introduction to Homological Algebra (standard reference, not scraped)
The Stacks Project, Section 13.9: Cones and termwise split sequences (standard reference, not scraped)