English
In the localized monoidal setting, the inverse associator μ is natural with respect to left whiskering. More precisely, for any morphism f: X1 → X2 and any object Y in the base category, the inverse associator at X1,Y composed with the left whiskering of f equals the left whiskering of f with Y composed with the inverse associator at X2,Y.
Русский
В локализованной моноидальной структуре обратная ассоциирующая изомория μ является естественной по отношению к левому придвижению. Говоря точнее, для любого морфизма f: X1 → X2 и любого объекта Y в базе, композиция μ^{-1}_{X1,Y} с левым отнесением f равна композиции левому отнесению f по Y с правой стороны μ^{-1}_{X2,Y}.
LaTeX
$$$(\\mu L W ε X_1 Y)^{-1} \\circ ((L')\\mathrm{map}(f) \\ ▷ (L').\\mathrm{obj} Y) \;=\\; ((L').\\mathrm{map}(f \\ ▷ Y)) \\circ (\\mu L W ε X_2 Y)^{-1}$$$
Lean4
@[reassoc (attr := simp)]
theorem μ_inv_natural_left {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
(μ L W ε X₁ Y).inv ≫ (L').map f ▷ (L').obj Y = (L').map (f ▷ Y) ≫ (μ L W ε X₂ Y).inv := by simp [Iso.eq_comp_inv]
