Theorems · Theorem · category theory

CategoryTheory.ShortComplex.mono_homologyMap_iff_up_to_refinements

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  CategoryTheory.Mono (CategoryTheory.ShortComplex.homologyMap φ) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
      CategoryTheory.CategoryStruct.comp x₂ S₁.g = 0 →
        ∀ (y₁ : A ⟶ S₂.X₁),
          CategoryTheory.CategoryStruct.comp x₂ φ.τ₂ = CategoryTheory.CategoryStruct.comp y₁ S₂.f →
            ∃ A' π,
              ∃ (_ : CategoryTheory.Epi π),
                ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ S₁.f

Defined in

Mathlib.CategoryTheory.Abelian.Refinements

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian