hexagon_forward — Mathlib

English

In a symmetric monoidal category, the forward hexagon diagram commutes: α_hom edges with braiding compose to the symmetric form.

Русский

В симметричной моноидальной категории диаграмма гексагона сходится по направлению вперёд.

LaTeX

$$$(\\alpha_{X,Y,Z}).\\mathrm{hom} \\; ; \\; braiding_{X} \\; ; \\alpha_{Y,Z,X}.\\mathrm{hom} = braiding_{X,Y}.hom \\; ▷ \\; Z \\; ; \\alpha_{Y,X,Z}.hom \\; ; \\; Y ◁ braiding_{X,Z}.hom$$$

Lean4

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

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