# A computer proof of the snake lemma

May 2014

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.

## Standard definitions

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

• A is a set, (+) ∈ (A × AA) is a two-place operator, 0 ∈ A is an element, and (-) ∈ (AA) is a one-place operator,

• a1A, ∀a2A, ∀a3A, a1 + (a2 + a3) = a1 + a2 + a3 = (a1 + a2) + a3,

• a1A, ∀a2A, a1 + a2 = a2 + a1,

• aA, 0 + a = a = a + 0, and

• aA, a + (-a) = 0 = (-a) + a.

We write aA to mean that aA.

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, 0A, -A) and B = (B, +B, 0B, -B) is the abelian group A × B = (A × B, +, 0, -) where

• ∀(a1, b1) ∈ A × B, ∀(a2, b2) ∈ A × B, (a1, b1) + (a2, b2) = (a1 +A a2, b1 +B b2)

• 0 = (0A, 0B), and

• ∀(a, b) ∈ A × B, -(a, b) = (-Aa, -Bb).

## Nonstandard definitions

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 1A on (A, A) is the linear relation defined by the set {(a, a) : aA}. For all abelian groups A and B = (B, +, 0, -), the zero linear relation 0AB on (A, B) is the linear relation defined by the set {(a, 0) : aA}. For all linear relations α on (A, B) and β on (B, C), the composite linear relation β α is defined by the set {(a, c) : (a, b1) ∈ α, (b2, c) ∈ β, b1 = b2}. 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 α 00A00B. The linear relation α is total if and only if 0A0-1 ⊆ α-1 0B0-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 α 0A0-1 = β-1 0C0, i.e., α 0A0-1 ⊆ β-1 0C0 and β-1 0C0 ⊆ α 0A0-1. A sequence of linear relations is exact if and only if every contiguous pair is exact.

## The snake lemma

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 (00A, γ, θ, π, 0J0) and (00B, δ, λ, ρ, 0K0) and (00C, ε, μ, σ, 0L0) and the row sequences (00D, ζ, η, 0F0) and (00G, ν, ξ, 0I0) 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 (00A, α, β, ω, τ, φ, 0L0) is exact.

## Rules of inference

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.