Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp_eq

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z),
  (CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z₁).comp
      (CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z₂) =
    z₁.comp z₂

Defined in: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Cited by: 1 results in Mathlib
Foundations: Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

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
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
CategoryTheory.MorphismProperty.HasLeftCalculusOfFractionsstatement and proof · cited by 71
CategoryTheory.MorphismProperty.LeftFractionstatement and proof · cited by 67
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mkstatement · cited by 10
CategoryTheory.MorphismProperty.LeftFraction.Localization.Homstatement · cited by 8
CategoryTheory.MorphismProperty.LeftFraction.compstatement · cited by 2
CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.compstatement · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMkproof · cited by 1