hexagon_reverse — Mathlib

English

The opposite hexagon identity holds with inverse associator and braiding; the reverse hexagon commutes.

Русский

Обратная диаграмма гексагона выполняется: обратимый ассоциатор и braiding удовлетворяют равенству.

LaTeX

$$$(\\alpha_{X,Y,Z})^{-1} \\; ; \\; braiding_{-,Z}.hom \\; ; \\alpha_{Z,X,Y} ^{-1} = X ◁ braiding_{Y,Z}.hom \\; ; \\alpha_{X,Z,Y}^{-1} \\; ; \\; (X braiding Z).hom ▷ Y$$$

Lean4

@[simp]
theorem hexagon_reverse (X Y Z : ModuleCat.{u} R) :
    (α_ X Y Z).inv ≫ (braiding _ Z).hom ≫ (α_ Z X Y).inv =
      X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y :=
  by
  apply (cancel_epi (α_ X Y Z).hom).1
  ext : 1
  apply TensorProduct.ext_threefold
  intro x y z
  rfl

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