isIso_homologyMap_τ₃ — Mathlib

English

Under hypotheses, φ.τ3 i is an isomorphism.

Русский

При гипотезах φ.τ3 i является изоморфизмом.

LaTeX

$$isIso (homologyMap φ.τ₃ i)$$

Lean4

theorem isIso_homologyMap_τ₃ (i : ι) (h₁ : Epi (homologyMap φ.τ₁ i)) (h₂ : IsIso (homologyMap φ.τ₂ i))
    (h₃ : ∀ j, c.Rel i j → IsIso (homologyMap φ.τ₁ j)) (h₄ : ∀ j, c.Rel i j → Mono (homologyMap φ.τ₂ j)) :
    IsIso (homologyMap φ.τ₃ i) :=
  by
  have :=
    mono_homologyMap_τ₃ φ hS₁ hS₂ i h₁ (IsIso.mono_of_iso _)
      (fun j hij => by
        have := h₃ j hij
        infer_instance)
  have :=
    epi_homologyMap_τ₃ φ hS₁ hS₂ i inferInstance
      (fun j hij => by
        have := h₃ j hij
        infer_instance)
      h₄
  apply isIso_of_mono_of_epi

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