Theorems · Definition · category theory
CategoryTheory.MorphismProperty.LeftFraction.ofHom
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
(W : CategoryTheory.MorphismProperty C) → {X Y : C} → (X ⟶ Y) → [W.ContainsIdentities] → W.LeftFraction X YThe left fraction from X to Y given by a morphism f : X ⟶ Y.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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.CategoryStruct.idproof · cited by 6,235
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.MorphismProperty.ContainsIdentitiesstatement and proof · cited by 94
- CategoryTheory.MorphismProperty.LeftFractionstatement · cited by 67
- CategoryTheory.MorphismProperty.id_memproof · cited by 23
Cited by9
Results whose statement or proof uses this declaration.
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Qproof · cited by 21
- CategoryTheory.MorphismProperty.LeftFraction.map_ofHomstatement and proof · cited by 3
- CategoryTheory.MorphismProperty.map_eq_iff_postcompproof · cited by 2
- CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_mapstatement · cited by 1
- CategoryTheory.MorphismProperty.LeftFraction.ofHom_Y'statement and proof · cited by 0
- CategoryTheory.MorphismProperty.LeftFraction.ofHom_fstatement and proof · cited by 0
- CategoryTheory.MorphismProperty.LeftFraction.ofHom_sstatement and proof · cited by 0