English
For any objects X, W, Y, Z and morphisms f: W → Y, g: X → Z, the braiding maps interact with the biproduct map via the standard braiding equation: the diagram obtained by braiding X with W, then applying biprod.map f g, then braiding Y with Z, equals the biprod.map g f.
Русский
Для любых объектов X, W, Y, Z и морфизмов f: W → Y, g: X → Z, отражение биобразного произведения совместно с картой biprod.map удовлетворяет стандартному равенству перегибов: сопоставление через braiding X с W, затем biprod.map f g, затем braiding Y с Z эквивалентно biprod.map g f.
LaTeX
$$$(\mathrm{biprod.braiding}\,X\,W)^{\mathrm{hom}} \;\circ\; \mathrm{biprod.map}\; f\; g \; \circ\; (\mathrm{biprod.braiding}\,Y\,Z)^{\mathrm{hom}} = \mathrm{biprod.map}\; g\; f.$$$
Lean4
@[reassoc]
theorem braiding_map_braiding {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) :
(biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom = biprod.map g f := by cat_disch
