English
Let C be a monoidal category with associator α. Then the two natural ways of re-associating four objects W, X, Y, Z through a four-step pentagon commute; equivalently, a certain composite of associators is equal to another.
Русский
Пусть C — моноидальная категория с ассоциатором α. Тогда две естественные цепочки переразложения четырех объектов W, X, Y, Z через четверку образцов приводят к одинаковому морфизму; эквивалентно равенству двух композиций ассоциаторов.
LaTeX
$$$$ (\alpha_{W,X\otimes Y,Z})^{-1} \circ \big( (\alpha_{W,X,Y})^{-1} \triangleright Z \circ (\alpha_{(W\otimes X)Y Z}).hom \big) = W \triangleleft (\alpha_{X Y Z}).hom \circ (\alpha_{W X (Y\otimes Z)})^{-1} $$$$
Lean4
@[reassoc (attr := simp)]
theorem pentagon_inv_inv_hom_hom_inv :
(α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom = W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv :=
by
rw [← cancel_epi (W ◁ (α_ X Y Z).inv), ← cancel_mono (α_ (W ⊗ X) Y Z).inv]
simp
