Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMk

∀ {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)
  (z₃ : W.LeftFraction z₁.Y' z₂.Y'),
  CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁)
        (CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂) =
      CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk (z₁.comp₀ z₂ z₃)

Defined in

Mathlib.CategoryTheory.Localization.CalculusOfFractions

Cited by

1 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.HasLeftCalculusOfFractions