Theorems · Definition · category theory

CategoryTheory.Abelian.epiDesc

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [CategoryTheory.Epi f] →
            {T : C} →
              (g : X ⟶ T) → CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0 → (Y ⟶ T)

In an abelian category, any morphism that turns to zero when precomposed with the kernel of an epimorphism factors through that epimorphism.

Defined in

Mathlib.CategoryTheory.Abelian.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.Epi