English
The right unitor hom component in the localized monoidal category can be written as a composite starting from the tensor of X with the unit, followed by μ, then whiskering with the map for the unit, yielding the right unitor in the localized setting.
Русский
Гомоморфизм правого единичного отображения в локализованной моноидальной категории записывается как композит, начинающийся с тензора X с единицей, затем μ и придвижение через отображение единицы, приводя к правому единичному отображению в локализованной структуре.
LaTeX
$$$(\\rho_ (L').obj X).hom = (L').obj X \\triangleleft (\\epsilon' L W ε)^{-1} \\circ (\\mu L W ε _ _ _).hom \\circ (L').map (\\rho_X).hom$$$
Lean4
theorem rightUnitor_hom_app (X : C) :
(ρ_ ((L').obj X)).hom = (L').obj X ◁ (ε' L W ε).inv ≫ (μ _ _ _ _ _).hom ≫ (L').map (ρ_ X).hom :=
by
dsimp [monoidalCategoryStruct, rightUnitor]
rw [liftNatTrans_app]
dsimp
rw [assoc]
change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _
simp only [comp_id]
