English
In a braided monoidal category, one can rewrite the three-fold braiding identity in a tensorized form, where the two sides become expressions that are equivalent after projecting onto tensor components. This is a variant of the Yang–Baxter relation.
Русский
В браидированной моноидальной категории существует версия уравнения Янга–Баштера в тензорной форме, показывающая эквивалентность двух составов после проекции на тензорные компоненты.
LaTeX
$$$$ (\beta_{X,Y}) \triangleright Z \otimes (Y \triangleleft (\beta_{X,Z}) ) \otimes (\beta_{Y,Z}) \triangleright X \;=\; \mathrm{Id}_{\;X \otimes Y \otimes Z} $$$$
Lean4
theorem yang_baxter' (X Y Z : C) :
(β_ X Y).hom ▷ Z ⊗≫ Y ◁ (β_ X Z).hom ⊗≫ (β_ Y Z).hom ▷ X =
𝟙 _ ⊗≫ (X ◁ (β_ Y Z).hom ⊗≫ (β_ X Z).hom ▷ Y ⊗≫ Z ◁ (β_ X Y).hom) ⊗≫ 𝟙 _ :=
by
rw [← cancel_epi (α_ X Y Z).inv, ← cancel_mono (α_ Z Y X).hom]
convert yang_baxter X Y Z using 1
all_goals monoidal
