English
The associator μ is natural with respect to right whiskering: for any X, morphism g: Y1 → Y2, the right whiskering of g by X composed with the hom component of μ at X,Y2 equals the hom component at X,Y1 composed with the map induced by X whiskering g.
Русский
Ассоциатор μ естественно действует относительно правого подсоединения: для любого X и гомоморфизма g: Y1 → Y2 правое придвижение g по X, сочетаемое с линейным компонентом μ при X,Y2, равно гомоморфизму μ при X,Y1 далее по отображению, вызываемому X‑придвижением g.
LaTeX
$$$(L').\\mathrm{obj} X \\triangleleft g \\;\\;\\gg\\; (\\mu L W ε X Y_2).hom = (\\mu L W ε X Y_1).hom \\;\\gg\\; (L').\\mathrm{map}(X \\triangleleft g)$$$
Lean4
@[reassoc (attr := simp)]
theorem μ_natural_right (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
(L').obj X ◁ (L').map g ≫ (μ L W ε X Y₂).hom = (μ L W ε X Y₁).hom ≫ (L').map (X ◁ g) :=
((tensorBifunctorIso L W ε).hom.app X).naturality g
