English
In a monoidal category, whiskering a morphism with a right unitor commutes with the braiding and associator up to coherence; the stated equality expresses compatibility of the left whisker with the tensorial structure.
Русский
В моноидальной категории окраска левые униторные множители совместимы с браидингом и ассоциатором; равенство выражает совместимость левого взятия с тензорной структурой.
LaTeX
$$$X \\;◁\\; (\\rho_Y)^{\\!\\mathrm{hom}} = α_{X,Y,I}^{-1} \\;∘\\; (X \\triangleleft (\\rho_Y)^{\\!\\mathrm{hom}})$$$
Lean4
@[reassoc, simp]
theorem whiskerLeft_rightUnitor (X Y : C) : X ◁ (ρ_ Y).hom = (α_ X Y (𝟙_ C)).inv ≫ (ρ_ (X ⊗ Y)).hom := by
rw [← whiskerRight_iff, comp_whiskerRight, ← cancel_epi (α_ _ _ _).inv, ← cancel_epi (X ◁ (α_ _ _ _).inv),
pentagon_inv_assoc, triangle_assoc_comp_right, ← associator_inv_naturality_middle, ← whiskerLeft_comp_assoc,
triangle_assoc_comp_right, associator_inv_naturality_right]
