Theorems · Definition · category theory

CategoryTheory.Abelian.epiIsCokernelOfKernel

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [CategoryTheory.Epi f] →
            (s : CategoryTheory.Limits.Fork f 0) →
              CategoryTheory.Limits.IsLimit s →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f ⋯)

In an abelian category, an epi is the cokernel of its kernel. More precisely: If f is an epimorphism and s is some limit kernel cone on f, then f is a cokernel of fork.ι s.

Defined in

Mathlib.CategoryTheory.Abelian.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.Epi