English
Let C be a braided monoidal category. For any objects X, Y, Z in C, a fundamental compatibility (the Yang–Baxter relation) holds between the associator and the braiding, expressing that braiding and tensoring commute coherently in threefold products.
Русский
Пусть C — браидированная моноидальная категория. Для любых объектов X, Y, Z в C выполняется основная совместимость (уравнение Янга–Баштера) между ассоциатором и braiding, выражающая когерентность braiding и тензоризации в произведении из трёх объектов.
LaTeX
$$$$(\alpha_{X,Y,Z})^{-1} \;\circ\; (\beta_{X,Y}) \triangleright Z \;\circ\; (\alpha_{Y,X,Z}) \;\circ\; Y \triangleleft (\beta_{X,Z}) \circ (\alpha_{Y,Z,X})^{-1} \circ (\beta_{Y,Z}) \triangleright X \circ (\alpha_{Z,Y,X}) = X \triangleleft (\beta_{Y,Z}) \triangleright Y \;\circ\; (\alpha_{X,Z,Y})^{-1} \circ (\beta_{X,Z}) \triangleright Y \circ (\alpha_{Z,X,Y}) \circ Z \triangleleft (\beta_{X,Y}).$$$$
Lean4
@[reassoc]
theorem yang_baxter (X Y Z : C) :
(α_ X Y Z).inv ≫
(β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv ≫ (β_ Y Z).hom ▷ X ≫ (α_ Z Y X).hom =
X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y ≫ (α_ Z X Y).hom ≫ Z ◁ (β_ X Y).hom :=
by
rw [← braiding_tensor_right_hom_assoc X Y Z, ← cancel_mono (α_ Z Y X).inv]
repeat rw [assoc]
rw [Iso.hom_inv_id, comp_id, ← braiding_naturality_right, braiding_tensor_right_hom]
