Theorems · Theorem · category theory

CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 4},
  R₁.Exact →
    R₂.Exact →
      ∀ (φ : R₁ ⟶ R₂),
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 0
              CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2) →
          CategoryTheory.IsIso
              (CategoryTheory.ComposableArrows.app' φ 1
                CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4) →
            CategoryTheory.IsIso
                (CategoryTheory.ComposableArrows.app' φ 3
                  CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6) →
              CategoryTheory.Mono
                  (CategoryTheory.ComposableArrows.app' φ 4
                    CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7) →
                CategoryTheory.IsIso
                  (CategoryTheory.ComposableArrows.app' φ 2
                    CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)

The five lemma.

Defined in

Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Cited by

4 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian