English
In the diagram with F : K2 → K3 and hF: f2 ∘ ι2 = ι3 ∘ F, the pair F, δ' forms an exact sequence, i.e. Im F = Ker δ'.
Русский
В диаграмме с F: K2 → K3 и условием hF: f2 ∘ ι2 = ι3 ∘ F последовательность K2 → K3 → C1 (через δ') точна, то есть Im F = Ker δ'.
LaTeX
$$$\operatorname{Im}(F) = \ker\bigl(\delta' i_1 i_2 i_3 f_1 f_2 hf g_1 g_2 hg h_1 h_2 ι_3 hι_3 π_1 hπ_1\bigr).$$$
Lean4
/-- 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 exact_δ'_right (hf₂ : Surjective f₂) (hg₁ : Injective g₁) (F : K₂ →ₗ[R] K₃) (hF : f₂.comp ι₂ = ι₃.comp F)
(h : Injective ι₃) : Exact F (δ' i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ ι₃ hι₃ π₁ hπ₁ hf₂ hg₁) :=
SnakeLemma.exact_δ_right _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ‹_› _ _ _ _ _ ‹_› ‹_›
