English
In a braided category with left distributivity, the left distributivity isomorphism interacts with braiding to relate left and right distributivity via braiding braiding between Y and X; the two distributivity structures are compatible up to braiding.
Русский
В braid-категории с левым распределением левый распределительный изоморфизм сочетается с braiding, чтобы связать левое и правое распределение через braiding между Y и X.
LaTeX
$$$(coprodComparison (tensorLeft X) Y Z) \\circ (\\beta_X (Y \\sqcup Z))^{\\mathrm{hom}} = (coprod.map (\\beta_X Y)^{\\mathrm{hom}} (\\beta_X Z)^{\\mathrm{hom}}) \\circ (coprodComparison (tensorRight X) Y Z)$$$
Lean4
/-- In a symmetric monoidal category, the left distributivity is equal to
the right distributivity up to braiding isomorphisms. -/
@[simp]
theorem coprodComparison_tensorLeft_braiding_hom [BraidedCategory C] {X Y Z : C} :
(coprodComparison (tensorLeft X) Y Z) ≫ (β_ X (Y ⨿ Z)).hom =
(coprod.map (β_ X Y).hom (β_ X Z).hom) ≫ (coprodComparison (tensorRight X) Y Z) :=
by simp [coprodComparison]
