Theorems · Definition · category theory
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.Preadditive C] →
[CategoryTheory.Limits.HasKernels C] →
[CategoryTheory.Limits.HasCokernels C] → {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Limits.MonoFactorisation fThe factorisation of a morphism through its abelian image.
- Defined in
- Mathlib.CategoryTheory.Abelian.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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.Preadditivestatement and proof · cited by 3,309
- CategoryTheory.Limits.kernel.ιproof · cited by 214
- CategoryTheory.Limits.cokernel.πproof · cited by 194
- CategoryTheory.Limits.MonoFactorisationstatement · cited by 69
- CategoryTheory.Limits.HasKernelsstatement and proof · cited by 67
- CategoryTheory.Limits.kernel.liftproof · cited by 64
- CategoryTheory.Abelian.imageproof · cited by 57
- CategoryTheory.Limits.HasCokernelsstatement and proof · cited by 47
Cited by7
Results whose statement or proof uses this declaration.
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e'statement · cited by 1
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageFactorisationproof · cited by 1
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_Istatement and proof · cited by 0
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_estatement and proof · cited by 0
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_mstatement and proof · cited by 0
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.isNormalEpiCategoryproof · cited by 0