English
The forward hexagon identity can be encapsulated as an iso equality expressing that a certain composite of associator and braiding is equal to a composite involving whiskerIsos, highlighting the hexagonal coherence.
Русский
Прямое гексагональное тождество в виде равенства изоморфизмов выражает, что некоторая композиция ассоциатора и braiding равна композиции с whiskerIsos, подчёркивая когерентность.
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
@[simp, reassoc]
theorem map_braiding (F : C ⥤ D) (X Y : C) [F.Braided] :
F.map (β_ X Y).hom = δ F X Y ≫ (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X := by
rw [← Functor.Braided.braided, δ_μ_assoc]
