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

A degreewise split exact complex with compatible splittings is contractible

Statement

Let $C_{∙}$ be an acyclic chain complex. Suppose that for every $n$ there is an isomorphism $ϕ_{n} : C_{n} \tilde{\to} Z_{n} (C) \oplus Z_{n - 1} (C)$ such that $i_{n} = ϕ_{n}^{- 1} j_{1},$ where $i_{n} : Z_{n} (C) ↪ C_{n}$ is the cycle inclusion and $j_{1}$ is the first summand inclusion, and such that the differential is $d_{n} = i_{n - 1} π_{2} ϕ_{n},$ where $π_{2}$ is the second projection. Then $C_{∙}$ is contractible.

Facts & Assumptions

Given: An acyclic chain complex $C_{∙}$ and isomorphisms $ϕ_{n}$ as in the statement.

[L1]

A contractible complex is one whose identity map is null-homotopic (A contractible complex).

[L2]

Acyclic means exact at every degree (Exactness of a complex at a degree and acyclic complexes).

Proof

technique · direct

1.1givenalgebra

Define $s_{n - 1} : C_{n - 1} \to C_{n}$ by $s_{n - 1} : = ϕ_{n}^{- 1} j_{2} π_{1} ϕ_{n - 1},$ where $j_{2}$ is the second inclusion and $π_{1}$ is the first projection. Then $d_{n} s_{n - 1} = i_{n - 1} π_{1} ϕ_{n - 1} = ϕ_{n - 1}^{- 1} j_{1} π_{1} ϕ_{n - 1}$ by the formula for $d_{n}$ and the compatibility of $i_{n - 1}$ with $ϕ_{n - 1}$ .

2.1L1L2step 1.1algebra∎

Likewise $s_{n - 2} d_{n - 1} = ϕ_{n - 1}^{- 1} j_{2} π_{2} ϕ_{n - 1},$ so $d_{n} s_{n - 1} + s_{n - 2} d_{n - 1} = ϕ_{n - 1}^{- 1} (j_{1} π_{1} + j_{2} π_{2}) ϕ_{n - 1} = 1_{C_{n - 1}} .$ Thus the identity map is null-homotopic, and [L1] makes $C_{∙}$ contractible.

Depends on

Used by

Dependency tree · two levels

8 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)