TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-29

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.

The kernel-cokernel sequence of a composite

Statement

For composable morphisms $A \overset{f}{\to} B \overset{g}{\to} C$ in an abelian category, there is an exact sequence $0 \to \ker (f) \to \ker (g f) \to \ker (g) \overset{q_{f} k_{g}}{\to} coker (f) \to coker (g f) \to coker (g) \to 0,$ where $k_{g} : \ker (g) \to B$ is a kernel of $g$ , $q_{f} : B \to coker (f)$ is a cokernel of $f$ , and the unlabeled arrows are the canonical comparison maps induced by the chosen kernels and cokernels.

Facts & Assumptions

Given: Composable morphisms $A \overset{f}{\to} B \overset{g}{\to} C$ .

[L1]

Under the stated endpoint hypotheses, the induced kernel and cokernel sequences are exact (Exactness of kernel and cokernel sequences under endpoint hypotheses).

[L2]

Exactness is self-dual (Exactness is self-dual).

[L3]

Kernels and cokernels are universal for the morphisms they annihilate (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers).

[L4]

The identity of an object is a kernel of its map to $0$ , and dually a cokernel of the map $0 \to A$ (The cokernel of the zero map out of the zero object is the target, and dually for kernels).

[L5]

Every kernel is monic (Every equalizer is a monomorphism, and every coequalizer is an epimorphism).

Proof

technique · direct

1.1L3construct

Choose kernels $k_{f} : K_{f} \to A, k_{g f} : K_{g f} \to A, k_{g} : K_{g} \to B$ and cokernels $q_{f} : B \to Q_{f}, q_{g f} : C \to Q_{g f}, q_{g} : C \to Q_{g} .$ Because $g f k_{f} = 0$ , [L3] gives a canonical map $u : K_{f} \to K_{g f}$ with $k_{g f} u = k_{f}$ . Likewise $g f k_{g f} = 0$ gives a canonical map $v : K_{g f} \to K_{g}$ with $k_{g} v = f k_{g f}$ . Put $δ : = q_{f} k_{g} : K_{g} \to Q_{f} .$ Since $q_{g f} g f = 0$ and $q_{g} g = 0$ , [L3] also gives canonical maps $w : Q_{f} \to Q_{g f}$ and $x : Q_{g f} \to Q_{g}$ .

2.1L5step 1.1algebra

The map $u$ is monic: if $u s = u t$ , then $k_{f} s = k_{g f} u s = k_{g f} u t = k_{f} t$ , and monicity of $k_{f}$ from [L5] forces $s = t$ . So the sequence is exact at $\ker (f)$ .

2.2L1L4step 1.1construct

Apply [L1] to the commutative diagram tikzcd \ker(f) \arrow[r, "k_f"] \arrow[d, "0"'] & A \arrow[r, "f"] \arrow[d, "g f"'] & B \arrow[d, "g"'] \\ 0 \arrow[r] & C \arrow[r, "1_C"'] & C. The top row is exact, and $0 \to C$ is monic. Hence the induced sequence $\ker (0) \to \ker (g f) \to \ker (g)$ is exact. By [L4], $\ker (0)$ is represented by $1_{\ker (f)}$ , so this is exactly the sequence $\ker (f) \overset{u}{\to} \ker (g f) \overset{v}{\to} \ker (g)$ at $\ker (g f)$ .

2.3L1L4step 1.1construct

Apply [L1] again to tikzcd A \arrow[r, "f"] \arrow[d, "g f"'] & B \arrow[r, "q_f"] \arrow[d, "g"'] & \operatorname{coker}(f) \arrow[d, "0"'] \\ C \arrow[r, "1_C"'] & C \arrow[r] & 0. The top row is exact, and $1_{C}$ is monic. Therefore the induced sequence $\ker (g f) \to \ker (g) \to \ker (0_{coker (f), 0})$ is exact. By [L4], the last kernel is represented by $1_{coker (f)}$ , and the induced map is $q_{f} k_{g} = δ$ . Hence $\ker (g f) \overset{v}{\to} \ker (g) \overset{δ}{\to} coker (f)$ is exact at $\ker (g)$ .

3.1L2step 1.1step 2.1step 2.2step 2.3

Apply steps 2.1 to 2.3 in the opposite category to the composable pair $C \overset{g^{o p}}{\to} B \overset{f^{o p}}{\to} A .$ Using [L2], the resulting exactness statements transport back to exactness of $\ker (g) \overset{δ}{\to} coker (f) \overset{w}{\to} coker (g f) \overset{x}{\to} coker (g) \to 0$ at $coker (f)$ , at $coker (g f)$ , and at $coker (g)$ .

4.1step 2.1step 2.2step 2.3step 3.1∎

Steps 2.1 to 2.3 and 3.1 give the full exact sequence displayed in the statement.

Depends on

Used by

Dependency tree · two levels

13 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

Saunders Mac Lane, Categories for the Working Mathematician, Exercise VIII.4.6 (standard reference, not scraped)