pentagon_hom_inv_inv_inv_inv — Mathlib

English

Another symmetric form of the pentagon identity expresses equivalence between two different but natural routes of reassociation in a monoidal category using inverses and homs of associators.

Русский

Ещё одна симметричная форма пентагонной идентичности выражает эквивалентность между двумя различными, но естественными маршрутами переразложения в моноидальной категории, используя инверсии и гомоморфизмы ассоциаторов.

LaTeX

$$$$ (\alpha_{W,X,Y})^{-1} \triangleright Z \circ (\alpha_{W, X, (Y Z)}).hom = (\alpha_{W(X Y) Z}).hom \circ W \triangleleft (\alpha_{X Y Z})^{-1} $$$$

Lean4

@[reassoc (attr := simp)]
theorem pentagon_hom_inv_inv_inv_inv :
    W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv = (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z := by
  simp [← cancel_epi (W ◁ (α_ X Y Z).inv)]

Похожие утверждения