homMk_comp — Mathlib

English

Mapping by the composite morphism preserves composition on the level of homs: homMk(f ≫ g) = homMk(f) ≫ homMk(g).

Русский

Преобразование по композиции сохраняет композицию на уровне гомоморфизмов: homMk(f ≫ g) = homMk(f) ≫ homMk(g).

LaTeX

$$$\\mathrm{homMk}(f \\circ g) = \\mathrm{homMk}(f) \\circ \\mathrm{homMk}(g)$$$

Lean4

/-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence. -/
theorem homMk_comp {U V W : Over X} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) (w_f w_g) :
    homMk (f ≫ g) (by simp_all) = homMk f w_f ≫ homMk g w_g :=
  by
  ext
  simp

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