Theorems · Definition · category theory

CategoryTheory.NonPreadditiveAbelian.monoIsKernelOfCokernel

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.NonPreadditiveAbelian C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [CategoryTheory.Mono f] →
            (s : CategoryTheory.Limits.Cofork f 0) →
              CategoryTheory.Limits.IsColimit s →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f ⋯)

In a NonPreadditiveAbelian category, a mono is the kernel of its cokernel. More precisely: If f is a monomorphism and s is some colimit cokernel cocone on f, then f is a kernel of Cofork.π s.

Defined in

Mathlib.CategoryTheory.Abelian.NonPreadditive

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.NonPreadditiveAbelianCategoryTheory.Mono