pentagon_inv_hom_hom_hom_inv — Mathlib

English

In a monoidal category, an equivalent rearrangement of the pentagon identity holds when you replace certain associator morphisms by their inverses in a symmetric fashion.

Русский

В моноидальной категории эквивалентная перестановка пентагонной идентичности сохраняется при замене некоторых морфизмов ассоциатора их обратными в симметричном виде.

LaTeX

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

Lean4

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

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