The snake lemma in terms of modules #
The snake lemma is proven in Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean for all abelian
categories, but for definitional equality and universe issues we reprove them here for modules.
Main results #
SnakeLemma.δ: The connecting homomorphism guaranteed by the snake lemma.SnakeLemma.exact_δ_left: The connecting homomorphism is exact on the right.SnakeLemma.exact_δ_right: The connecting homomorphism is exact on the left.
Suppose we have an exact commutative diagram
K₂ -F-→ K₃
| |
ι₂ ι₃
↓ ↓
M₁ -f₁→ M₂ -f₂→ M₃
| | |
i₁ i₂ i₃
↓ ↓ ↓
N₁ -g₁→ N₂ -g₂→ N₃
| |
π₁ π₂
↓ ↓
C₁ -G-→ C₂
such that f₂ is surjective with a (set-theoretic) section σ, g₁ is injective with a
(set-theoretic) retraction ρ, and that ι₃ is injective and π₁ is surjective.
theorem
SnakeLemma.δ_aux
{R : Type u_3}
[CommRing R]
{M₂ : Type u_4}
{M₃ : Type u_5}
{N₁ : Type u_2}
{N₂ : Type u_1}
{N₃ : Type u_7}
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
(i₂ : M₂ →ₗ[R] N₂)
(i₃ : M₃ →ₗ[R] N₃)
(f₂ : M₂ →ₗ[R] M₃)
(g₁ : N₁ →ₗ[R] N₂)
(g₂ : N₂ →ₗ[R] N₃)
(hg : Function.Exact ⇑g₁ ⇑g₂)
(h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂)
(σ : M₃ → M₂)
(hσ : ⇑f₂ ∘ σ = id)
(ρ : N₂ → N₁)
(hρ : ρ ∘ ⇑g₁ = id)
{K₃ : Type u_6}
[AddCommGroup K₃]
[Module R K₃]
(ι₃ : K₃ →ₗ[R] M₃)
(hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
(x : K₃)
:
theorem
SnakeLemma.eq_of_eq
{R : Type u_3}
[CommRing R]
{M₁ : Type u_8}
{M₂ : Type u_2}
{M₃ : Type u_1}
{N₁ : Type u_6}
{N₂ : Type u_5}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(f₁ : M₁ →ₗ[R] M₂)
(f₂ : M₂ →ₗ[R] M₃)
(hf : Function.Exact ⇑f₁ ⇑f₂)
(g₁ : N₁ →ₗ[R] N₂)
(h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁)
(ρ : N₂ → N₁)
(hρ : ρ ∘ ⇑g₁ = id)
{K₃ : Type u_4}
{C₁ : Type u_7}
[AddCommGroup K₃]
[Module R K₃]
[AddCommGroup C₁]
[Module R C₁]
(ι₃ : K₃ →ₗ[R] M₃)
(π₁ : N₁ →ₗ[R] C₁)
(hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
(x : K₃)
(y₁ : M₂)
(hy₁ : f₂ y₁ = ι₃ x)
(z₁ : N₁)
(hz₁ : g₁ z₁ = i₂ y₁)
(y₂ : M₂)
(hy₂ : f₂ y₂ = ι₃ x)
(z₂ : N₁)
(hz₂ : g₁ z₂ = i₂ y₂)
:
def
SnakeLemma.δ
{R : Type u_1}
[CommRing R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
{N₁ : Type u_5}
{N₂ : Type u_6}
{N₃ : Type u_7}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(i₃ : M₃ →ₗ[R] N₃)
(f₁ : M₁ →ₗ[R] M₂)
(f₂ : M₂ →ₗ[R] M₃)
(hf : Function.Exact ⇑f₁ ⇑f₂)
(g₁ : N₁ →ₗ[R] N₂)
(g₂ : N₂ →ₗ[R] N₃)
(hg : Function.Exact ⇑g₁ ⇑g₂)
(h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁)
(h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂)
(σ : M₃ → M₂)
(hσ : ⇑f₂ ∘ σ = id)
(ρ : N₂ → N₁)
(hρ : ρ ∘ ⇑g₁ = id)
{K₃ : Type u_8}
{C₁ : Type u_9}
[AddCommGroup K₃]
[Module R K₃]
[AddCommGroup C₁]
[Module R C₁]
(ι₃ : K₃ →ₗ[R] M₃)
(hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
(π₁ : N₁ →ₗ[R] C₁)
(hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
:
Snake Lemma Suppose we have an exact commutative diagram
K₃
|
ι₃
↓
M₁ -f₁→ M₂ -f₂→ M₃
| | |
i₁ i₂ i₃
↓ ↓ ↓
N₁ -g₁→ N₂ -g₂→ N₃
|
π₁
↓
C₁
such that f₂ is surjective with a (set-theoretic) section σ, g₁ is injective with a
(set-theoretic) retraction ρ,
then the map π₁ ∘ ρ ∘ i₂ ∘ σ ∘ ι₃ is a linear map from K₃ to C₁.
Also see SnakeLemma.δ' for a noncomputable version
that does not require an explicit section and retraction.
Equations
- SnakeLemma.δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ = { toFun := fun (x : K₃) => π₁ (ρ (i₂ (σ (ι₃ x)))), map_add' := ⋯, map_smul' := ⋯ }
Instances For
theorem
SnakeLemma.δ_eq
{R : Type u_3}
[CommRing R]
{M₁ : Type u_8}
{M₂ : Type u_2}
{M₃ : Type u_1}
{N₁ : Type u_6}
{N₂ : Type u_5}
{N₃ : Type u_9}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(i₃ : M₃ →ₗ[R] N₃)
(f₁ : M₁ →ₗ[R] M₂)
(f₂ : M₂ →ₗ[R] M₃)
(hf : Function.Exact ⇑f₁ ⇑f₂)
(g₁ : N₁ →ₗ[R] N₂)
(g₂ : N₂ →ₗ[R] N₃)
(hg : Function.Exact ⇑g₁ ⇑g₂)
(h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁)
(h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂)
(σ : M₃ → M₂)
(hσ : ⇑f₂ ∘ σ = id)
(ρ : N₂ → N₁)
(hρ : ρ ∘ ⇑g₁ = id)
{K₃ : Type u_4}
{C₁ : Type u_7}
[AddCommGroup K₃]
[Module R K₃]
[AddCommGroup C₁]
[Module R C₁]
(ι₃ : K₃ →ₗ[R] M₃)
(hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
(π₁ : N₁ →ₗ[R] C₁)
(hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
(x : K₃)
(y : M₂)
(hy : f₂ y = ι₃ x)
(z : N₁)
(hz : g₁ z = i₂ y)
:
theorem
SnakeLemma.exact_δ_right
{R : Type u_1}
[CommRing R]
{M₁ : Type u_7}
{M₂ : Type u_5}
{M₃ : Type u_4}
{N₁ : Type u_8}
{N₂ : Type u_9}
{N₃ : Type u_10}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(i₃ : M₃ →ₗ[R] N₃)
(f₁ : M₁ →ₗ[R] M₂)
(f₂ : M₂ →ₗ[R] M₃)
(hf : Function.Exact ⇑f₁ ⇑f₂)
(g₁ : N₁ →ₗ[R] N₂)
(g₂ : N₂ →ₗ[R] N₃)
(hg : Function.Exact ⇑g₁ ⇑g₂)
(h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁)
(h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂)
(σ : M₃ → M₂)
(hσ : ⇑f₂ ∘ σ = id)
(ρ : N₂ → N₁)
(hρ : ρ ∘ ⇑g₁ = id)
{K₂ : Type u_2}
{K₃ : Type u_3}
{C₁ : Type u_6}
[AddCommGroup K₂]
[Module R K₂]
[AddCommGroup K₃]
[Module R K₃]
[AddCommGroup C₁]
[Module R C₁]
(ι₂ : K₂ →ₗ[R] M₂)
(hι₂ : Function.Exact ⇑ι₂ ⇑i₂)
(ι₃ : K₃ →ₗ[R] M₃)
(hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
(π₁ : N₁ →ₗ[R] C₁)
(hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
(F : K₂ →ₗ[R] K₃)
(hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F)
(h : Function.Injective ⇑ι₃)
:
Function.Exact ⇑F ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)
Suppose we have an exact commutative diagram
K₂ -F-→ K₃
| |
ι₂ ι₃
↓ ↓
M₁ -f₁→ M₂ -f₂→ M₃
| | |
i₁ i₂ i₃
↓ ↓ ↓
N₁ -g₁→ N₂ -g₂→ N₃
|
π₁
↓
C₁
such that f₂ is surjective with a (set-theoretic) section σ, g₁ is injective with a
(set-theoretic) retraction ρ, and ι₃ is injective, then K₂ -F→ K₃ -δ→ C₁ is exact.
theorem
SnakeLemma.exact_δ_left
{R : Type u_1}
[CommRing R]
{M₁ : Type u_7}
{M₂ : Type u_8}
{M₃ : Type u_9}
{N₁ : Type u_4}
{N₂ : Type u_5}
{N₃ : Type u_10}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(i₃ : M₃ →ₗ[R] N₃)
(f₁ : M₁ →ₗ[R] M₂)
(f₂ : M₂ →ₗ[R] M₃)
(hf : Function.Exact ⇑f₁ ⇑f₂)
(g₁ : N₁ →ₗ[R] N₂)
(g₂ : N₂ →ₗ[R] N₃)
(hg : Function.Exact ⇑g₁ ⇑g₂)
(h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁)
(h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂)
(σ : M₃ → M₂)
(hσ : ⇑f₂ ∘ σ = id)
(ρ : N₂ → N₁)
(hρ : ρ ∘ ⇑g₁ = id)
{K₃ : Type u_6}
{C₁ : Type u_2}
{C₂ : Type u_3}
[AddCommGroup K₃]
[Module R K₃]
[AddCommGroup C₁]
[Module R C₁]
[AddCommGroup C₂]
[Module R C₂]
(ι₃ : K₃ →ₗ[R] M₃)
(hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
(π₁ : N₁ →ₗ[R] C₁)
(hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
(π₂ : N₂ →ₗ[R] C₂)
(hπ₂ : Function.Exact ⇑i₂ ⇑π₂)
(G : C₁ →ₗ[R] C₂)
(hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁)
(h : Function.Surjective ⇑π₁)
:
Function.Exact ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) ⇑G
Suppose we have an exact commutative diagram
K₃
|
ι₃
↓
M₁ -f₁→ M₂ -f₂→ M₃
| | |
i₁ i₂ i₃
↓ ↓ ↓
N₁ -g₁→ N₂ -g₂→ N₃
| |
π₁ π₂
↓ ↓
C₁ -G-→ C₂
such that f₂ is surjective with a (set-theoretic) section σ, g₁ is injective with a
(set-theoretic) retraction ρ, and π₁ is surjective, then K₃ -δ→ C₁ -G→ C₂ is exact.
noncomputable def
SnakeLemma.δ'
{R : Type u_1}
[CommRing R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M₃ : Type u_4}
{N₁ : Type u_5}
{N₂ : Type u_6}
{N₃ : Type u_7}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(i₃ : M₃ →ₗ[R] N₃)
(f₁ : M₁ →ₗ[R] M₂)
(f₂ : M₂ →ₗ[R] M₃)
(hf : Function.Exact ⇑f₁ ⇑f₂)
(g₁ : N₁ →ₗ[R] N₂)
(g₂ : N₂ →ₗ[R] N₃)
(hg : Function.Exact ⇑g₁ ⇑g₂)
(h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁)
(h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂)
{K₃ : Type u_8}
{C₁ : Type u_9}
[AddCommGroup K₃]
[Module R K₃]
[AddCommGroup C₁]
[Module R C₁]
(ι₃ : K₃ →ₗ[R] M₃)
(hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
(π₁ : N₁ →ₗ[R] C₁)
(hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
(hf₂ : Function.Surjective ⇑f₂)
(hg₁ : Function.Injective ⇑g₁)
:
Suppose we have an exact commutative diagram
K₃
|
ι₃
↓
M₁ -f₁→ M₂ -f₂→ M₃
| | |
i₁ i₂ i₃
↓ ↓ ↓
N₁ -g₁→ N₂ -g₂→ N₃
|
π₁
↓
C₁
such that f₂ is surjective and g₁ is injective,
then this is the linear map K₃ → C₁ given by the snake lemma.
Also see SnakeLemma.δ for a computable version.
Equations
- SnakeLemma.δ' i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ ι₃ hι₃ π₁ hπ₁ hf₂ hg₁ = SnakeLemma.δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ (Function.surjInv hf₂) ⋯ (Function.invFun ⇑g₁) ⋯ ι₃ hι₃ π₁ hπ₁
Instances For
theorem
SnakeLemma.δ'_eq
{R : Type u_3}
[CommRing R]
{M₁ : Type u_8}
{M₂ : Type u_1}
{M₃ : Type u_2}
{N₁ : Type u_4}
{N₂ : Type u_5}
{N₃ : Type u_9}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(i₃ : M₃ →ₗ[R] N₃)
(f₁ : M₁ →ₗ[R] M₂)
(f₂ : M₂ →ₗ[R] M₃)
(hf : Function.Exact ⇑f₁ ⇑f₂)
(g₁ : N₁ →ₗ[R] N₂)
(g₂ : N₂ →ₗ[R] N₃)
(hg : Function.Exact ⇑g₁ ⇑g₂)
(h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁)
(h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂)
{K₃ : Type u_6}
{C₁ : Type u_7}
[AddCommGroup K₃]
[Module R K₃]
[AddCommGroup C₁]
[Module R C₁]
(ι₃ : K₃ →ₗ[R] M₃)
(hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
(π₁ : N₁ →ₗ[R] C₁)
(hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
(hf₂ : Function.Surjective ⇑f₂)
(hg₁ : Function.Injective ⇑g₁)
(x : K₃)
(y : M₂)
(hy : f₂ y = ι₃ x)
(z : N₁)
(hz : g₁ z = i₂ y)
:
theorem
SnakeLemma.exact_δ'_right
{R : Type u_3}
[CommRing R]
{M₁ : Type u_9}
{M₂ : Type u_1}
{M₃ : Type u_2}
{N₁ : Type u_4}
{N₂ : Type u_5}
{N₃ : Type u_10}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(i₃ : M₃ →ₗ[R] N₃)
(f₁ : M₁ →ₗ[R] M₂)
(f₂ : M₂ →ₗ[R] M₃)
(hf : Function.Exact ⇑f₁ ⇑f₂)
(g₁ : N₁ →ₗ[R] N₂)
(g₂ : N₂ →ₗ[R] N₃)
(hg : Function.Exact ⇑g₁ ⇑g₂)
(h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁)
(h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂)
{K₂ : Type u_6}
{K₃ : Type u_7}
{C₁ : Type u_8}
[AddCommGroup K₂]
[Module R K₂]
[AddCommGroup K₃]
[Module R K₃]
[AddCommGroup C₁]
[Module R C₁]
(ι₂ : K₂ →ₗ[R] M₂)
(hι₂ : Function.Exact ⇑ι₂ ⇑i₂)
(ι₃ : K₃ →ₗ[R] M₃)
(hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
(π₁ : N₁ →ₗ[R] C₁)
(hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
(hf₂ : Function.Surjective ⇑f₂)
(hg₁ : Function.Injective ⇑g₁)
(F : K₂ →ₗ[R] K₃)
(hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F)
(h : Function.Injective ⇑ι₃)
:
Function.Exact ⇑F ⇑(δ' i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ ι₃ hι₃ π₁ hπ₁ hf₂ hg₁)
Suppose we have an exact commutative diagram
K₂ -F-→ K₃
| |
ι₂ ι₃
↓ ↓
M₁ -f₁→ M₂ -f₂→ M₃
| | |
i₁ i₂ i₃
↓ ↓ ↓
N₁ -g₁→ N₂ -g₂→ N₃
|
π₁
↓
C₁
such that f₂ is surjective, g₁ is injective, and ι₃ is injective,
then K₂ -F→ K₃ -δ→ C₁ is exact.
theorem
SnakeLemma.exact_δ'_left
{R : Type u_3}
[CommRing R]
{M₁ : Type u_9}
{M₂ : Type u_1}
{M₃ : Type u_2}
{N₁ : Type u_4}
{N₂ : Type u_5}
{N₃ : Type u_10}
[AddCommGroup M₁]
[Module R M₁]
[AddCommGroup M₂]
[Module R M₂]
[AddCommGroup M₃]
[Module R M₃]
[AddCommGroup N₁]
[Module R N₁]
[AddCommGroup N₂]
[Module R N₂]
[AddCommGroup N₃]
[Module R N₃]
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(i₃ : M₃ →ₗ[R] N₃)
(f₁ : M₁ →ₗ[R] M₂)
(f₂ : M₂ →ₗ[R] M₃)
(hf : Function.Exact ⇑f₁ ⇑f₂)
(g₁ : N₁ →ₗ[R] N₂)
(g₂ : N₂ →ₗ[R] N₃)
(hg : Function.Exact ⇑g₁ ⇑g₂)
(h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁)
(h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂)
{K₃ : Type u_8}
{C₁ : Type u_6}
{C₂ : Type u_7}
[AddCommGroup K₃]
[Module R K₃]
[AddCommGroup C₁]
[Module R C₁]
[AddCommGroup C₂]
[Module R C₂]
(ι₃ : K₃ →ₗ[R] M₃)
(hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
(π₁ : N₁ →ₗ[R] C₁)
(hπ₁ : Function.Exact ⇑i₁ ⇑π₁)
(π₂ : N₂ →ₗ[R] C₂)
(hπ₂ : Function.Exact ⇑i₂ ⇑π₂)
(hf₂ : Function.Surjective ⇑f₂)
(hg₁ : Function.Injective ⇑g₁)
(G : C₁ →ₗ[R] C₂)
(hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁)
(h : Function.Surjective ⇑π₁)
:
Function.Exact ⇑(δ' i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ ι₃ hι₃ π₁ hπ₁ hf₂ hg₁) ⇑G
Suppose we have an exact commutative diagram
K₃
|
ι₃
↓
M₁ -f₁→ M₂ -f₂→ M₃
| | |
i₁ i₂ i₃
↓ ↓ ↓
N₁ -g₁→ N₂ -g₂→ N₃
| |
π₁ π₂
↓ ↓
C₁ -G-→ C₂
such that f₂ is surjective, g₁ is injective, and π₁ is surjective,
then K₃ -δ→ C₁ -G→ C₂ is exact.