Theorems · Definition · category theory

CategoryTheory.Abelian.Preradical.isColimitCokernelCoforkObj

{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Φ : CategoryTheory.Abelian.Preradical C) →
        (X : C) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (Φ.π.app X) ⋯)

For X : C, the cokernel cofork CokernelCofork.ofπ (Φ.π.app X) (Φ.ι_π_app X) exhibits Φ.π.app X : X ⟶ Φ.quotient.obj X as the cokernel of Φ.ι.app X : Φ.r.obj X ⟶ X.

Defined in

Mathlib.CategoryTheory.Abelian.Preradical.Colon

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian