pentagon_inv_hom_hom_hom_hom — Mathlib

English

A reformulation of the pentagon identity using inverse associators and whiskering on both sides.

Русский

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

LaTeX

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

Lean4

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

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