LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30

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 chain map carries cycles to cycles and boundaries to boundaries

Statement

Let $f : C_{∙} \to D_{∙}$ be a chain map. For every $n \in Z$ there are induced morphisms $Z_{n} (f) : Z_{n} (C) \to Z_{n} (D), B_{n} (f) : B_{n} (C) \to B_{n} (D),$ compatible with the canonical inclusions into $C_{n}$ and $D_{n}$ .

Facts & Assumptions

Given: A chain map $f : C_{∙} \to D_{∙}$ and an integer $n$ .

[L1]

A chain map satisfies $d_{n}^{D} f_{n} = f_{n - 1} d_{n}^{C}$ (Chain map).

[L2]

Kernels are universal among arrows killed by the given morphism (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

[L3]

Write $d_{n + 1}^{C} = i_{C} e_{C}$ and $d_{n + 1}^{D} = i_{D} e_{D}$ as epic-monic factorizations, where $i_{C}$ and $i_{D}$ are the boundary inclusions (Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism).

[L4]

In an abelian category, every monomorphism is the kernel of its cokernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).

Proof

technique · direct

1.1L1L2givenconstruct

Let $k_{C} : Z_{n} (C) \to C_{n}$ and $k_{D} : Z_{n} (D) \to D_{n}$ be the cycle inclusions. Using [L1], $d_{n}^{D} f_{n} k_{C} = f_{n - 1} d_{n}^{C} k_{C} = 0,$ so [L2] yields a unique map $Z_{n} (f) : Z_{n} (C) \to Z_{n} (D)$ with $k_{D} Z_{n} (f) = f_{n} k_{C}$ .

2.1L1L2L3L4givenalgebraconstructdischarge-construct∎

By [L3], $f_{n} i_{C} e_{C} = f_{n} d_{n + 1}^{C} = d_{n + 1}^{D} f_{n + 1} = i_{D} e_{D} f_{n + 1} .$ Let $c_{D}$ be a cokernel of $i_{D}$ . Then $c_{D} f_{n} i_{C} e_{C} = c_{D} i_{D} e_{D} f_{n + 1} = 0.$ Since $e_{C}$ is epic, this implies $c_{D} f_{n} i_{C} = 0$ . By [L4], the monomorphism $i_{D}$ is a kernel of $c_{D}$ , so [L2] gives a unique morphism $B_{n} (f) : B_{n} (C) \to B_{n} (D)$ with $i_{D} B_{n} (f) = f_{n} i_{C} .$ This is the required boundary map.

Depends on

Used by

Dependency tree · two levels

17 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)
Romyar Sharifi, Homological Algebra, Lemma 2.7.10 (standard reference, not scraped)