Theorems · Definition · category theory
CategoryTheory.Limits.Image.monoFactorisation
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
{X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasImage f] → CategoryTheory.Limits.MonoFactorisation fSome factorisation of f through a monomorphism (selected with choice).
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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.HasImagestatement and proof · cited by 107
- CategoryTheory.Limits.MonoFactorisationstatement · cited by 69
- CategoryTheory.Limits.ImageFactorisation.Fproof · cited by 9
- CategoryTheory.Limits.Image.imageFactorisationproof · cited by 0
Cited by22
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.imageproof · cited by 124
- CategoryTheory.Limits.image.ιproof · cited by 104
- CategoryTheory.Limits.factorThruImageproof · cited by 55
- CategoryTheory.Limits.image.facproof · cited by 27
- CategoryTheory.Limits.Image.isImagestatement · cited by 11
- CategoryTheory.Limits.image.compIsoproof · cited by 7
- CategoryTheory.Limits.IsImage.lift_ιstatement and proof · cited by 4
- CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ιproof · cited by 3
- CategoryTheory.Limits.imageMonoIsoSource_inv_ιproof · cited by 2
- CategoryTheory.Limits.image.compIso_hom_comp_image_ιproof · cited by 2
- CategoryTheory.Limits.image.compIso_inv_comp_image_ιproof · cited by 2
- CategoryTheory.PreservesImage.iso_homstatement · cited by 2