English
Let W, X, Y, Z be objects in a monoidal category. The two natural ways to reparent the associators in the fourfold tensor product W ⊗ X ⊗ Y ⊗ Z yield equal morphisms. Concretely, the coherence morphisms built from the associator satisfy the pentagon equation when composed appropriately with the inv of the associator on Y ⊗ Z.
Русский
Пусть W, X, Y, Z — объекты в моноидальной категории. Существуют два естественных способа перестроить скобки в тензорном произведении W ⊗ X ⊗ Y ⊗ Z, которые приводят к одинаковым морфизмам. Конкретно, композиции ассоциатора удовлетворяют pentagon-неравенству при надлежащем объединении с обратным ассоциатором на Y ⊗ Z.
LaTeX
$$$(\\alpha_{W,X,(Y\\otimes Z)}).hom \\;\\gg\\; (\\mathrm{id}_W \\otimes (\\alpha_{X,Y,Z}.inv)) = (\\alpha_{(W\\otimes X),Y,Z}).inv \\gg ((\\alpha_{W,X,Y}.hom \\otimes \\mathrm{id}_Z) \\gg (\\alpha_{W,(X\\otimes Y),Z}).hom$$$
Lean4
@[reassoc]
theorem pentagon_hom_inv {W X Y Z : C} :
(α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ₘ (α_ X Y Z).inv) =
(α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ₘ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom :=
by simp
