isIso_of_epi_of_isIso_of_isIso_of_mono

English

In a diagram with two composable exact sequences and monomorphisms at the end, the middle epimorphism is established under certain conditions.

Русский

В диаграмме с двумя последовательностями точности и мономорфизмами в конце, при определенных условиях середняя стрелка является эпиморфизмом.

LaTeX

$$$\\\\forall φ: R_1 \\to R_2, \\\\text{R1.Exact}, \\\\text{R2.Exact} \\\\Rightarrow \\\\mathrm{Epi}(app' φ 1).$$$

Lean4

/-- The five lemma. -/
theorem isIso_of_epi_of_isIso_of_isIso_of_mono (h₀ : Epi (app' φ 0)) (h₁ : IsIso (app' φ 1)) (h₂ : IsIso (app' φ 3))
    (h₃ : Mono (app' φ 4)) : IsIso (app' φ 2) := by
  dsimp at h₀ h₁ h₂ h₃
  have : Mono (app' φ 2) := by
    apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1 (R₂.exact_iff_δlast.1 hR₂).1 <;>
        dsimp <;>
      infer_instance
  have : Epi (app' φ 2) := by
    apply epi_of_epi_of_epi_of_mono (δ₀Functor.map φ) (R₁.exact_iff_δ₀.1 hR₁).2 (R₂.exact_iff_δ₀.1 hR₂).2 <;> dsimp <;>
      infer_instance
  apply isIso_of_mono_of_epi

Похожие утверждения