Theorems · Definition · category theory

CategoryTheory.ObjectProperty.createsCokernels

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P : CategoryTheory.ObjectProperty C) →
        [P.IsClosedUnderCokernels] →
          {X Y : P.FullSubcategory} →
            (f : X ⟶ Y) →
              [CategoryTheory.Limits.HasCokernel f.hom] →
                CategoryTheory.CreatesColimit (CategoryTheory.Limits.parallelPair f 0) P.ι

If an object property P is closed under cokernels, then P.ι creates cokernels. In particular, this implies P.ι preserves cokernels.

Defined in

Mathlib.CategoryTheory.ObjectProperty.Kernels

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.ObjectProperty.IsClosedUnderCokernelsCategoryTheory.Limits.HasCokernel