hexagon_reverse_inv — Mathlib

English

The inverse hexagon identity relates the inverse of the associator with the braiding via whisker isomorphisms, establishing a dual form of the hexagon relation.

Русский

Инвариант обратного гексагонального тождества связывает обратный ассоциатор с braiding через whisker-изоморфизмы, устанавливая двойственную форму гексагонального тождества.

LaTeX

$$$$ (\alpha_{Z,X,Y})\,^{−1} \circ (\beta_{(X\otimes Y),Z})^{−1} \circ (\alpha_{X,Y,Z})^{−1} = (\beta_{X,Z})^{−1} \triangleright Y \circ (\alpha_{X,Z,Y}) \circ X \triangleleft (\beta_{Y,Z})^{−1}, $$$$

Lean4

@[reassoc]
theorem hexagon_reverse_inv (X Y Z : C) :
    (α_ Z X Y).hom ≫ (β_ (X ⊗ Y) Z).inv ≫ (α_ X Y Z).hom = (β_ X Z).inv ▷ Y ≫ (α_ X Z Y).hom ≫ X ◁ (β_ Y Z).inv := by
  simp

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