English
In the localized monoidal setting, the action of the left unitor on an object Y is expressed as a composite involving the inverse of the local version of ε', whiskering, and μ’s hom component; this gives an explicit realization of the left unitor in the localized category.
Русский
В локализованной моноидальной структуре левый единичный отображатель для объекта Y выражается через композицию обратного ε' в локализованной категории, придвижения и гомоморфизм μ; это явное представление левого единичного отображения в локализованной категории.
LaTeX
$$$(\\lambda^{{L'}}_Y)^{-1} \\triangleright (L')\\mathrm{obj} Y \\;\\circ\\; (\\mu L W ε \\_\\_\\_ X Y).hom = (L')\\mathrm{obj} Y \\triangleleft (\\mathrm{map} \\lambda_Y) \\circ (\\mu L W ε X Y).hom$$$
Lean4
theorem leftUnitor_hom_app (Y : C) :
(λ_ ((L').obj Y)).hom = (ε' L W ε).inv ▷ (L').obj Y ≫ (μ _ _ _ _ _).hom ≫ (L').map (λ_ Y).hom :=
by
dsimp [monoidalCategoryStruct, leftUnitor]
rw [liftNatTrans_app]
dsimp
rw [assoc]
change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _
simp only [comp_id]
