We sketch enough of the theory of abelian groups to state and prove a well known result called the snake lemma. Our proof generalizes easily to modules and thence to abelian categories, via Mitchell’s embedding theorem.

The proof itself is on a separate page, to avoid excessive widening of this one. The Haskell program (tbz) that created the proof is available also.

An *abelian group* is a quadruple **A** = (*A*, +, 0, -) such that

*A*is a set, (+) ∈ (*A*×*A*→*A*) is a two-place operator, 0 ∈*A*is an element, and (-) ∈ (*A*→*A*) is a one-place operator,∀

*a*_{1}∈*A*, ∀*a*_{2}∈*A*, ∀*a*_{3}∈*A*,*a*_{1}+ (*a*_{2}+*a*_{3}) =*a*_{1}+*a*_{2}+*a*_{3}= (*a*_{1}+*a*_{2}) +*a*_{3},∀

*a*_{1}∈*A*, ∀*a*_{2}∈*A*,*a*_{1}+*a*_{2}=*a*_{2}+*a*_{1},∀

*a*∈*A*, 0 +*a*=*a*=*a*+ 0, and∀

*a*∈*A*,*a*+ (-*a*) = 0 = (-*a*) +*a*.

We write *a* ∈ **A** to mean that *a* ∈ *A*.

The *zero abelian group* is **0** = ({0}, +, 0, -) where 0 + 0 = 0 and -0 = 0.

A *subgroup* of an abelian group **A** = (*A*, +, 0, -) is an abelian group **A**′ = (*A*′, +′, 0′, -′) such that

*A*′ ⊆*A*,(+)′ = (+)|

_{A′ × A′},0′ = 0, and

(-)′ = (-)|

_{A′}.

The subgroup **A**′ is defined uniquely by **A** and the set *A*′. We write **A**′ ⊆ **A** to mean that **A**′ is a subgroup of **A**.

The *direct product* of abelian groups **A** = (*A*, +_{A}, 0_{A}, -_{A}) and **B** = (*B*, +_{B}, 0_{B}, -_{B}) is the abelian group **A** × **B** = (*A* × *B*, +, 0, -) where

∀(

*a*_{1},*b*_{1}) ∈*A*×*B*, ∀(*a*_{2},*b*_{2}) ∈*A*×*B*, (*a*_{1},*b*_{1}) + (*a*_{2},*b*_{2}) = (*a*_{1}+_{A}*a*_{2},*b*_{1}+_{B}*b*_{2})0 = (0

_{A}, 0_{B}), and∀(

*a*,*b*) ∈*A*×*B*, -(*a*,*b*) = (-_{A}*a*, -_{B}*b*).

A *linear relation* on a pair of abelian groups (**A**, **B**) is a subgroup of **A** × **B**. For all abelian groups **A**, the *identity linear relation* **1**_{A} on (**A**, **A**) is the linear relation defined by the set {(*a*, *a*) : *a* ∈ **A**}. For all abelian groups **A** and **B** = (*B*, +, 0, -), the *zero linear relation* **0**_{AB} on (**A**, **B**) is the linear relation defined by the set {(*a*, 0) : *a* ∈ **A**}. For all linear relations α on (**A**, **B**) and β on (**B**, **C**), the *composite linear relation* β α defined by the set {(*a*, *c*) : (*a*, *b*_{1}) ∈ α, (*b*_{2}, *c*) ∈ β, *b*_{1} = *b*_{2}}. For all linear relations α on (**A**, **B**), the *inverse linear relation* α^{-1} on (**B**, **A**) is defined by the set {(*b*, *a*) : (*a*, *b*) ∈ α}. For all linear relations α on (**A**, **B**) and β on (**B**, **C**) and γ on (**C**, **D**), it holds that γ (β α) = (γ β) α, so we define γ (β α) = γ β α = (γ β) α. For all linear relations α on (**A**, **B**) and β on (**B**, **C**), it holds that (β α)^{-1} = α^{-1} β^{-1}.

A linear relation α on (**A**, **B**) is *well defined* if and only if α **0**_{0A} ⊆ **0**_{0B}. The linear relation α is *total* if and only if **0**_{A0}^{-1} ⊆ α^{-1} **0**_{B0}^{-1}. A linear relation is *functional* if and only if it is well defined and total. The zero linear relation and the identity linear relation are functional. For functional linear relations α on (**A**, **B**) and β on (**B**, **C**), the pair (α, β) is *exact* if and only if α **0**_{A0}^{-1} = β^{-1} **0**_{C0}, i.e., α **0**_{A0}^{-1} ⊆ β^{-1} **0**_{C0} and β^{-1} **0**_{C0} ⊆ α **0**_{A0}^{-1}. A sequence of linear relations is exact if and only if every contiguous pair is exact.

Let there be functional linear relations according to the following diagram, where, e.g., `A →α→ B`

means that α is a linear relation on (**A**, **B**).

```
A B C
↓ ↓ ↓
γ δ ε
↓ ↓ ↓
D →ζ→ E →η→ F
↓ ↓ ↓
θ λ μ
↓ ↓ ↓
G →ν→ H →ξ→ I
↓ ↓ ↓
π ρ σ
↓ ↓ ↓
J K L
```

Assume that λ ζ = ν θ and μ η = ξ λ, i.e., that the squares commute. Assume that the column sequences (**0**_{0A}, γ, θ, π, **0**_{J0}) and (**0**_{0B}, δ, λ, ρ, **0**_{K0}) and (**0**_{0C}, ε, μ, σ, **0**_{L0}) and the row sequences (**0**_{0D}, ζ, η, **0**_{F0}) and (**0**_{0G}, ν, ξ, **0**_{I0}) all are exact.

Define α = δ^{-1} ζ γ and β = ε^{-1} η δ and τ = ρ ν π^{-1} and φ = σ ξ ρ^{-1} and ω = π ν^{-1} λ η^{-1} ε.

```
A →α→ B →β→ C
↓ ↓ ↓
γ δ ε
↓ ↓ ↓
D →ζ→ E →η→ F
↓ ↓ ↓
θ λ μ
↓ ↓ ↓
G →ν→ H →ξ→ I
↓ ↓ ↓
π ρ σ
↓ ↓ ↓
J →τ→ K →φ→ L
```

Then it holds that δ α = ζ γ and ε β = η δ and ρ ν = τ π and σ ξ = φ ρ, and the sequence (**0**_{0A}, α, β, ω, τ, φ, **0**_{L0}) is exact.

We write

```
───
P
─── ───
R Q
─────────
S
```

to mean that `P`

and `Q`

are axioms, `R`

is inferred from `P`

, and `S`

is inferred from `R`

and `Q`

.

The first rule is

```
α ⊆ β
─────────
α⁻¹ ⊆ β⁻¹ .
```

We use it a lot but always implicitly. The second rule is

```
α ⊆ β
─────────
γ α ⊆ γ β ,
```

which, by the first rule, has a variation

```
α ⊆ β
─────────
α γ ⊆ β γ .
```

The third rule is

```
α ⊆ β β ⊆ γ
─────────────
α ⊆ γ .
```

We compress repeated applications of this rule, e.g.,

```
α ⊆ β β ⊆ γ γ ⊆ δ
─────────────────────
α ⊆ δ .
```

The fourth rule is

```
α 0 ⊆ β 0
───────────
α α⁻¹ β ⊆ β .
```

The fifth rule is

```
α 0⁻¹ ⊆ β 0⁻¹
─────────────
α ⊆ β β⁻¹ α .
```

In addition to the hypotheses of the snake lemma, two axioms are

```
───────
0 ⊆ α 0
───────────
α 0⁻¹ ⊆ 0⁻¹ .
```

The proof of soundness in each case here requires at most a couple of lines.

© 2014 David Eisenstat