English
In a commutative diagram of abelian categories with four arrows at the ends and exact rows, if the outer arrows are isomorphisms and the leftmost morphisms satisfy epi/mono hypotheses, then the middle arrow is an isomorphism.
Русский
В коммутативной диаграмме абелиевых категорий с четырьмя стрелками в концах и точными рядами, если внешние стрелки изоморфизмы, а слева условия эпиморфизма/моно соблюдаются, тогда средняя стрелка — изоморфизм.
LaTeX
$$$\\\\forall φ: R_1 \\to R_2, \\\\text{Exact}(R_1), \\\\text{Exact}(R_2), \\\\mathrm{IsIso}(app' φ 1), \\\\mathrm{IsIso}(app' φ 3) \\\\Rightarrow \\\\mathrm{IsIso}(app' φ 2).$$$
Lean4
theorem epi_of_epi_of_epi_of_mono' (hR₁ : (mk₂ (R₁.map' 1 2) (R₁.map' 2 3)).Exact)
(hR₂ : (mk₂ (R₂.map' 0 1) (R₂.map' 1 2)).Exact) (hR₂' : R₂.map' 1 3 = 0) (h₀ : Epi (app' φ 0)) (h₂ : Epi (app' φ 2))
(h₃ : Mono (app' φ 3)) : Epi (app' φ 1) :=
by
rw [epi_iff_surjective_up_to_refinements]
intro A g₁
obtain ⟨A₁, π₁, _, f₂, h₁⟩ := surjective_up_to_refinements_of_epi (app' φ 2 _) (g₁ ≫ R₂.map' 1 2)
have h₂ : f₂ ≫ R₁.map' 2 3 = 0 := by
rw [← cancel_mono (app' φ 3 _), assoc, zero_comp, NatTrans.naturality, ← reassoc_of% h₁, ← R₂.map'_comp 1 2 3, hR₂',
comp_zero, comp_zero]
obtain ⟨A₂, π₂, _, f₁, h₃⟩ := (hR₁.exact 0).exact_up_to_refinements _ h₂
dsimp at f₁ h₃
have h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 _) ≫ R₂.map' 1 2 = 0 := by
rw [sub_comp, assoc, assoc, assoc, ← NatTrans.naturality, ← reassoc_of% h₃, h₁, sub_self]
obtain ⟨A₃, π₃, _, g₀, h₅⟩ := (hR₂.exact 0).exact_up_to_refinements _ h₄
dsimp at g₀ h₅
rw [comp_sub] at h₅
obtain ⟨A₄, π₄, _, f₀, h₆⟩ := surjective_up_to_refinements_of_epi (app' φ 0 _) g₀
refine ⟨A₄, π₄ ≫ π₃ ≫ π₂ ≫ π₁, inferInstance, π₄ ≫ π₃ ≫ f₁ + f₀ ≫ (by exact R₁.map' 0 1), ?_⟩
rw [assoc, assoc, assoc, add_comp, assoc, assoc, assoc, NatTrans.naturality, ← reassoc_of% h₆, ← h₅, comp_sub]
dsimp
rw [add_sub_cancel]
