mk_comp_mk — Mathlib

English

Let f: X → Y and g: Y → Z be morphisms admitting a SmallHom structure with respect to W. Then the localization of the composite f ≫ g equals the composite of the localizations of f and g.

Русский

Пусть f: X → Y и g: Y → Z — морфизмы, допускающие структуру SmallHom относительно W. Тогда локализация композиции f ≫ g равна композиции локализаций f и g.

LaTeX

$$$\big(\mathrm{mk}\,W\,f\big) \circ \big(\mathrm{mk}\,W\,g\big) = \mathrm{mk}\,W\,(f \gg g)$$$

Lean4

theorem mk_comp_mk [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w} W Y Z] [HasSmallLocalizedHom.{w} W X Z]
    (f : X ⟶ Y) (g : Y ⟶ Z) : (mk W f).comp (mk W g) = mk W (f ≫ g) :=
  (equiv W W.Q).injective (by simp [equiv_comp])

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