pentagon_hom_hom_inv_hom_hom — Mathlib

English

A form of the pentagon identity equates two composites of associator morphisms where two homs appear on one side and their inverses on the other side via whiskering.

Русский

Форма пентагонной идентичности приравнивает две композиции морфизмов ассоциатора, где с одной стороны появляются гомоморфизмы, а с другой — их обратные через обрамление.

LaTeX

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

Lean4

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

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