English
In the same exact commutative diagram as above, the pair of maps δ: K3 → C1 and G: C1 → C2 form an exact sequence at C1, i.e. im δ = ker G. This is the left part of the snake lemma’s exactness statement.
Русский
В той же точной и коммутативной диаграмме, как выше, отображения δ: K3 → C1 и G: C1 → C2 образуют точную последовательность в C1, т.е. Im δ = Ker G. Это левая часть утверждения о точности змейки.
LaTeX
$$$\operatorname{Im}(\delta) = \ker(G).$$$
Lean4
/-- 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.
-/
theorem exact_δ_left (G : C₁ →ₗ[R] C₂) (hF : G.comp π₁ = π₂.comp g₁) (h : Surjective π₁) :
Exact (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) G :=
by
haveI H₂ := δ_aux i₂ i₃ f₂ g₁ g₂ hg h₂ σ hσ ρ hρ ι₃ hι₃
intro x
constructor
· intro H
obtain ⟨x, rfl⟩ := h x
obtain ⟨y, hy⟩ := (hπ₂ (g₁ x)).mp (by simpa only [← LinearMap.comp_apply, hF] using H)
obtain ⟨z, hz⟩ : f₂ y ∈ range ι₃ :=
(hι₃ (f₂ y)).mp (by rw [← i₃.comp_apply, ← h₂, g₂.comp_apply, hy, hg.apply_apply_eq_zero])
exact ⟨z, δ_eq i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ _ _ hz.symm _ hy.symm⟩
· rintro ⟨x, rfl⟩
simp only [δ, coe_mk, AddHom.coe_mk]
rw [← G.comp_apply, hF, π₂.comp_apply, H₂, hπ₂.apply_apply_eq_zero]
