pentagon_hom_hom_inv_inv_hom — Mathlib

English

A pentagon form asserting equality between two stacking orders of associator homomorphisms with left and right whiskering.

Русский

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

LaTeX

$$$$ (\alpha_{W X Y})^{\} \triangleright Z \circ \cdots = \cdots $$$$

Lean4

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

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