LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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 sequential abelian colimit is the cokernel of one minus shift

Statement

For any sequence of abelian groups $G_{0} \overset{u_{0}}{\to} G_{1} \overset{u_{1}}{\to} \dots$ , let $D = ⨁_{i \geq 0} G_{i}$ and let $s : D \to D$ send the $i$ th coordinate by $u_{i}$ into coordinate $i + 1$ . Then $0 ⟶ D \overset{1 - s}{\to} D ⟶ {colim}_{i} G_{i} ⟶ 0$ is exact, where the last map sums the canonical maps to the colimit. The maps $u_{i}$ need not be injective.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

Proof

1.1

If $(1 - s) x = 0$ , its coordinate zero is $x_{0} = 0$ . Recursively its coordinate $i$ is $x_{i} - u_{i - 1} x_{i - 1} = 0$ , forcing $x_{i} = 0$ for every $i$ . Thus $1 - s$ is injective, even if some or all transition maps vanish.

givenalgebra

2.1

The quotient $D / im (1 - s)$ imposes the relations $ι_{i} (g) = ι_{i + 1} (u_{i} g)$ . A homomorphism from this quotient to any abelian group $B$ is exactly a family of homomorphisms $v_{i} : G_{i} \to B$ satisfying $v_{i + 1} u_{i} = v_{i}$ : define the map on a finite-support tuple by the finite sum $\sum_{i} v_{i} (x_{i})$ . This proves the colimit universal property, so the quotient is the colimit and the last map is surjective with the stated kernel. Zero groups and a sequence supported at only one index are included.

step 1.1algebra∎

Used by

Additivity and compact cell support control the infinite cw colimit Lemma

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

May, A Concise Course in Algebraic Topology, 14§6, algebraic lemma p.114 (standard reference, not scraped)
Hatcher, Algebraic Topology, Theorem 3F.8 proof pp.314–315 (standard reference, not scraped)