homMk_comp_homMk — Mathlib

English

In the LeftFraction.Localization setup, composition of Hom objects is compatible: homMk z1 ≫ homMk z2 equals homMk (z1.comp0 z2 z3) when h3 holds.

Русский

В конструкции LeftFraction.Localization композиция Hom-объектов совместима: homMk z1 ≫ homMk z2 = homMk (z1.comp0 z2 z3) при выполнении h3.

LaTeX

$$homMk z_1 \circ HomMk z_2 = HomMk (z_1.comp_0 z_2 z_3)$$

Lean4

theorem homMk_comp_homMk {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
    (z₃ : W.LeftFraction z₁.Y' z₂.Y') (h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f) : homMk z₁ ≫ homMk z₂ = homMk (z₁.comp₀ z₂ z₃) :=
  by
  change Hom.comp _ _ = _
  rw [Hom.comp_eq, comp_eq z₁ z₂ z₃ h₃]

Похожие утверждения