hexagon_reverse_iso — Mathlib

English

A complementary hexagon identity expresses the reverse arrangement of the hexagon equation in a braided category, relating the inverse associator and braiding in a symmetrical form with whisker isomorphisms.

Русский

Дополнительное гексагональное тождество выражает обратное расположение компонентов гексагонального равенства, связывая инвертированный ассоциатор и braiding в симметричной форме.

LaTeX

$$$$ (\alpha_{Z,X,Y})^{-1} \circ (\beta_{(X\otimes Y),Z})^{−1} \circ (\alpha_{X,Y,Z}) = \text{whiskerLeftIso} X (\beta_{Y,Z}) \circ (\alpha_{X,Z,Y})^{−1} \circ \text{whiskerRightIso} (\beta_{X,Z}) Y, $$$$

Lean4

theorem hexagon_reverse_iso (X Y Z : C) :
    (α_ X Y Z).symm ≪≫ β_ (X ⊗ Y) Z ≪≫ (α_ Z X Y).symm =
      whiskerLeftIso X (β_ Y Z) ≪≫ (α_ X Z Y).symm ≪≫ whiskerRightIso (β_ X Z) Y :=
  Iso.ext (hexagon_reverse X Y Z)

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