pentagon_hom_inv_inv_inv_hom — Mathlib

English

A variant of the pentagon identity using inverses and whiskering in a monoidal category equating two distinct parenthesizations.

Русский

Вариант пентагонной идентичности с использованием инверсий и обрамления в моноидальной категории, приравнивающий две разные расстановки скобок.

LaTeX

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

Lean4

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

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