Theorems · Theorem · category theory

CategoryTheory.IsPushout.hom_eq_add_up_to_refinements

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X₁ X₂ X₃ X₄ : C}
  {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPushout t l r b →
    ∀ {T : C} (x₄ : T ⟶ X₄),
      ∃ T' π,
        ∃ (_ : CategoryTheory.Epi π),
          ∃ x₂ x₃,
            CategoryTheory.CategoryStruct.comp π x₄ =
              CategoryTheory.CategoryStruct.comp x₂ r + CategoryTheory.CategoryStruct.comp x₃ b

Given a pushout square in an abelian category `` X₁ ⟶ X₂ | | v v X₃ ⟶ X₄ ` the morphism X₂ ⊞ X₃ ⟶ X₄ is an epimorphism. This lemma translates this as the existence of liftings up to refinements: a morphism z : T ⟶ X₄ can be written as a sum of a morphism to X₂ and a morphism to X₃, at least if we allow a precomposition with an epimorphism π : T' ⟶ T`.

Defined in

Mathlib.CategoryTheory.Abelian.CommSq

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian