rightUnitor_naturality — Mathlib

English

Natural transformation given by the right unitor is natural with respect to morphisms in the localized monoidal category.

Русский

Натуральность естественного преобразования правой единицы в локализованной монойдальной категории.

LaTeX

$$$f \;\triangleright\; \mathrm{id} \circ (\rho_Y)^{\mathrm{hom}} = (\rho_X)^{\mathrm{hom}} \circ f$$$

Lean4

theorem rightUnitor_naturality {X Y : LocalizedMonoidal L W ε} (f : X ⟶ Y) :
    f ▷ 𝟙_ (LocalizedMonoidal L W ε) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f :=
  (rightUnitor L W ε).hom.naturality f

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