hexagon_forward_iso — Mathlib

English

The forward hexagon identity in a braided category gives an equality between two ways of rebracketing and braiding a triple tensor X ⊗ Y ⊗ Z, expressed via associators and braidings in a concrete equality of isomorphisms.

Русский

Прямой гексагональный тождество в браидированной категории даёт равенство двух способов перестройки скобок и Braiding для тройного тензора X ⊗ Y ⊗ Z, выраженное через ассоциаторы и braiding.

LaTeX

$$$$ \\alpha_{X,Y,Z} \\;\\circ\\; \\beta_{X, Y} \\otimes Z \\circ \\alpha_{Y,Z,X} \;=\\; \\text{whiskerRightIso}(\\beta_{X,Y}) Z \\circ \\alpha_{Y,X,Z} \\circ \\text{whiskerLeftIso} Y(\\beta_{X,Z}), $$$$

Lean4

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

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