homMk_comp — Mathlib

English

The morphism homMk respects composition: homMk(f ≫ g) = homMk f w_f ≫ homMk g w_g.

Русский

Гом Mk сохраняет композицию: homMk(f ≫ g) = homMk f w_f ≫ homMk g w_g.

LaTeX

$$homMk (f ≫ g) (by simp) = homMk f w_f ≫ homMk g w_g$$

Lean4

/-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence. -/
theorem homMk_comp {U V W : Under X} (f : U.right ⟶ V.right) (g : V.right ⟶ W.right) (w_f w_g) :
    homMk (f ≫ g) (by simp only [reassoc_of% w_f, w_g]) = homMk f w_f ≫ homMk g w_g :=
  by
  ext
  simp

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