TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-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.

Snake lemma in an abelian category

Statement

For snake data

there is an exact sequence $0 \to \ker (f) \to \ker (g) \to \ker (h) \overset{δ}{\to} coker (f) \to coker (g) \to coker (h) \to 0,$ where $δ$ is the connecting morphism of The connecting morphism exists and is unique.

Facts & Assumptions

Given: The snake-data diagram in the statement.

[L1]

The connecting morphism exists and is unique (The connecting morphism exists and is unique).

[L2]

The kernel row is exact at its first two nodes, and the cokernel row is exact at its last two nodes (The kernel row and cokernel row of a morphism of short exact sequences are exact at two nodes each).

[L3]

Exactness identifies the image of one arrow with the kernel of the next (Exactness at a node).

[L4]

Every morphism factors as an epimorphism followed by its image inclusion, and epimorphisms remain epic after pullback (Every morphism factors as an epimorphism followed by a monomorphism, uniquely up to unique isomorphism, The pullback of an epimorphism is an epimorphism).

[L5]

Every image inclusion is a kernel of the corresponding cokernel, and 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.1L2given

By [L2], the induced kernel row is exact at $\ker (f)$ and $\ker (g)$ , and the induced cokernel row is exact at $coker (g)$ and $coker (h)$ . It remains to prove exactness at $\ker (h)$ and $coker (f)$ .

1.2L1construct

Let $k_{h} : K \to C$ be a kernel of $h$ , $q_{f} : A^{'} \to Q$ a cokernel of $f$ , and $q_{g} : B^{'} \to Q_{g}$ a cokernel of $g$ . Use the pullback $P = B \times_{C} K$ from [L1], with projections $π^{'} : P \to B$ and $π : P \to K$ . That construction gives an epimorphism $π$ , a map $a : P \to A^{'}$ satisfying $i^{'} a = g π^{'}$ , and $δ : K \to Q$ satisfying $δ π = q_{f} a$ . Let $u : K_{g} \to K$ be the induced arrow from a kernel $k_{g} : K_{g} \to B$ of $g$ , and let $c : Q \to Q_{g}$ be induced by $i^{'}$ . Thus $k_{h} u = p k_{g}$ and $c q_{f} = q_{g} i^{'}$ .

2.1step 1.2constructalgebra

The pair $(k_{g}, u)$ induces $s : K_{g} \to P$ with $π^{'} s = k_{g}$ and $π s = u$ . Since $i^{'} a s = g k_{g} = 0$ and $i^{'}$ is monic, $a s = 0$ . Consequently $δ u = δ π s = q_{f} a s = 0$ .

2.2L3L4step 1.2construct

Let $t : T \to K$ be a kernel of $δ$ . Pull back $π$ along $t$ , obtaining $e_{0} : E_{0} \to T$ epic and $v : E_{0} \to P$ with $π v = t e_{0}$ . Then $q_{f} a v = δ t e_{0} = 0$ . By [L3], $im (f) = \ker (q_{f})$ , so $a v$ factors through the image inclusion $m_{f} : I_{f} \to A^{'}$ . Factor $f = m_{f} e_{f}$ with $e_{f} : A \to I_{f}$ epic, and pull back $e_{f}$ along this factorization. The resulting $e_{1} : E \to E_{0}$ is epic and has a map $x : E \to A$ with $f x = a v e_{1}$ .

2.3L3L4step 1.2constructalgebra

From $c q_{f} = q_{g} i^{'}$ and $i^{'} a = g π^{'}$ one obtains $c δ π = q_{g} i^{'} a = q_{g} g π^{'} = 0$ . Since $π$ is epic, $c δ = 0$ . Now let $r : R \to Q$ be a kernel of $c$ . Pull back the epimorphism $q_{f} : A^{'} \to Q$ along $r$ , obtaining an epimorphism $d_{0} : D_{0} \to R$ and $v : D_{0} \to A^{'}$ with $q_{f} v = r d_{0}$ . Then $q_{g} i^{'} v = c r d_{0} = 0$ , so $i^{'} v$ factors through $im (g) = \ker (q_{g})$ . Pull back the epic image projection $B \to im (g)$ along this factorization. This gives an epimorphism $d_{1} : D \to D_{0}$ and $y : D \to B$ with $g y = i^{'} v d_{1}$ .

3.1L3L5step 1.2step 2.1step 2.2constructalgebra

Put $z = π^{'} v e_{1} - i x : E \to B$ . Then $g z = i^{'} a v e_{1} - i^{'} f x = 0$ , so $z = k_{g} w$ for a unique $w : E \to K_{g}$ . Also $p z = p π^{'} v e_{1} = k_{h} t e_{0} e_{1} = k_{h} u w$ . Since $k_{h}$ is monic, $u w = t e_{0} e_{1}$ . The composite $e_{0} e_{1}$ is epic; hence $coker (u) t = 0$ . By [L5], $t$ factors through $im (u)$ . Together with $δ u = 0$ from step 2.1, this gives $im (u) = \ker (δ)$ .

3.2L3L5step 1.2step 2.3constructalgebra

The bottom-row relation gives $h p y = p^{'} g y = p^{'} i^{'} v d_{1} = 0$ , so $p y = k_{h} x$ for a unique $x : D \to K$ . The pair $(y, x)$ induces $s : D \to P$ , and $i^{'} a s = g y = i^{'} v d_{1}$ implies $a s = v d_{1}$ by monicity of $i^{'}$ . Thus $δ x = q_{f} a s = q_{f} v d_{1} = r d_{0} d_{1}$ . Because $d_{0} d_{1}$ is epic, $coker (δ) r = 0$ , so [L5] makes $r$ factor through $im (δ)$ . Along with $c δ = 0$ , this proves $im (δ) = \ker (c)$ .

4.1step 1.1step 3.1step 3.2∎

The two remaining nodes are exact by steps 3.1 and 3.2; the other nodes are exact by step 1.1. Therefore the snake sequence is exact.

Snake lemma in an abelian category

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources