pentagon_inv_inv_hom_inv_inv — Mathlib

English

A variant form of the pentagon identity exploiting the inverses of associators and their whiskered images.

Русский

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

LaTeX

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

Lean4

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

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