English
In the Snake Lemma configuration, the left part of the construction using δ' yields exactness with G: C1 → C2, i.e. im δ' = ker G.
Русский
В конфигурации змейки левая часть с δ' обеспечивает точность последовательности: 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, `g₁` is injective, and `π₁` is surjective,
then `K₃ -δ→ C₁ -G→ C₂` is exact.
-/
theorem exact_δ'_left (hf₂ : Surjective f₂) (hg₁ : Injective g₁) (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π₁ hf₂ hg₁) G :=
SnakeLemma.exact_δ_left _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ‹_› _ ‹_› ‹_›
