TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30‡ rests on unproved material (inherited)

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.

‡ Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Cohen's first model: an infinite Dedekind-finite set of reals, ‡ Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and ‡ The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

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]

The subtraction surrogate produces a member mapping to zero from two members with the same image (The subtraction surrogate).

[L4]

Exactness at a node is equivalent to the member-lifting condition (Exactness is detected by members).

[L5]

The opposite of an abelian category is abelian (The opposite of an abelian category is abelian).

Proof

technique · direct

1.1

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

L2given

2.1

Let $k_{h} : K \to C$ be a kernel of $h$ , let $q_{f} : A^{'} \to Q$ be a cokernel of $f$ , and use [L1] to form the pullback object $P$ , the map $π : P \to K$ , the map $π^{'} : P \to B$ , and the connecting morphism $δ : K \to Q$ with $ι δ π = ι^{'} g π^{'} .$ The proof of [L1] gives that $π$ is epic.

L1step 1.1construct

3.1

First, $δ$ kills the image of $\ker (g) \to \ker (h)$ . Indeed, a member of $\ker (g)$ factors through the pullback $P$ , and the defining identity of step 2.1 then gives $ι δ g^{'} = 0$ . Since $ι$ is monic in the pushout square used to define $δ$ , this implies $δ g^{'} = 0$ .

L1step 2.1constructalgebra

3.2

Conversely, let $t$ be a member of $\ker (h)$ with $δ t \equiv 0$ . Because $π$ is epic, lift $t$ to a member $n$ of $P$ with $π n \equiv t$ . Writing $a : P \to A^{'}$ for the map from the proof of [L1], we have $q_{f} a n = δ π n \equiv δ t \equiv 0.$ Exactness of $A \overset{f}{\to} A^{'} \overset{q_{f}}{\to} Q$ at $A^{'}$ gives a member $x$ of $A$ with $f x \equiv a n$ by [L4]. The equality $i^{'} a = g π^{'}$ from the construction of $a$ therefore gives $g π^{'} n \equiv i^{'} f x = g i x .$ Applying the subtraction surrogate [L3] to $π^{'} n$ and $i x$ , we obtain a member $z$ of $B$ with $g z \equiv 0$ and $p z \equiv p π^{'} n - p i x = k_{h} π n \equiv k_{h} t .$ Exactness of the top row at $B$ gives a member $y$ of $\ker (g)$ mapping to $z$ , and then exactness at $\ker (h)$ follows because $k_{h}$ is monic. Hence every member in $\ker (δ)$ lies in the image of $\ker (g) \to \ker (h)$ .

L1L3L4step 2.1constructalgebra

4.1

By [L5], the opposite of an abelian category is abelian. Applying step 3.2 there to the opposite snake diagram proves exactness at $coker (f)$ in the original category.

L5step 3.2

5.1

Therefore the full six-term sequence displayed in the statement is exact.

step 1.1step 3.1step 3.2step 4.1∎

Depends on

Used by

The kernel-cokernel sequence of a composite is a snake Corollary
A snake configuration whose kernel row is not short exact Counterexample
The connecting morphism computed for a short exact sequence of abelian groups Example
The published module snake lemma as an instance Example
The snake lemma applied to multiplication by an integer Example
FALSE: the snake lemma is just a pair of short exact kernel and cokernel rows False statement
An exact functor transports every diagram lemma Theorem
The diagram lemmas hold in the opposite category Theorem
The nine lemma follows from the snake lemma Theorem

Dependency tree · two levels

29 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, Lemma VIII.4.5 (standard reference, not scraped)
The Stacks Project, Section 12.5, Lemma 12.5.17(2) (standard reference, not scraped)