Theorems · Definition · category theory
CategoryTheory.Abelian.coim
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[CategoryTheory.Abelian C] → CategoryTheory.Functor (CategoryTheory.Arrow C) CAbelian.coimage as a functor from the arrow category.
- Defined in
- Mathlib.CategoryTheory.Abelian.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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.Homproof · cited by 32,603
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.Abelianstatement and proof · cited by 1,753
- CategoryTheory.Arrowstatement and proof · cited by 713
- CategoryTheory.Arrow.homproof · cited by 335
- CategoryTheory.Limits.kernel.ιproof · cited by 214
- CategoryTheory.Arrow.Hom.leftproof · cited by 160
- CategoryTheory.Limits.cokernel.descproof · cited by 53
- CategoryTheory.Abelian.coimageproof · cited by 44
- CategoryTheory.Abelian.coimage.πproof · cited by 19
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.Abelian.coimIsoImstatement · cited by 2
- CategoryTheory.Abelian.coimIsoIm_hom_appstatement · cited by 0
- CategoryTheory.Abelian.coimIsoIm_inv_appstatement · cited by 0
- CategoryTheory.Abelian.coim_mapstatement and proof · cited by 0
- CategoryTheory.Abelian.coim_objstatement and proof · cited by 0