Theorems · Definition · category theory
CategoryTheory.Limits.HasCokernel
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → (X ⟶ Y) → PropA morphism f has a cokernel if the functor ParallelPair f 0 has a colimit.
- Cited by
- 131 results in Mathlib
- Foundations
- Depth 19 from the axioms, rests on 86 definitions · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
- CategoryTheory.Limits.parallelPairproof · cited by 766
- CategoryTheory.Limits.HasColimitproof · cited by 307
Cited by178
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.cokernelstatement and proof · cited by 229
- CategoryTheory.Limits.cokernel.πstatement and proof · cited by 194
- CategoryTheory.Abelian.imagestatement and proof · cited by 57
- CategoryTheory.Limits.cokernel.descstatement and proof · cited by 53
- CategoryTheory.Limits.cokernel.conditionstatement and proof · cited by 50
- CategoryTheory.Abelian.coimagestatement and proof · cited by 44
- CategoryTheory.Limits.cokernel.π_descstatement and proof · cited by 37
- CategoryTheory.Abelian.image.ιstatement and proof · cited by 25
- CategoryTheory.Limits.cokernel.mapstatement and proof · cited by 23
- CategoryTheory.Limits.cokernelIsCokernelstatement and proof · cited by 23
- CategoryTheory.Abelian.factorThruImagestatement and proof · cited by 20
- CategoryTheory.Abelian.coimage.πstatement and proof · cited by 19