coprodComparison_tensorRight_braiding_hom

English

Analogous compatibility statement for the right distributivity under braiding; braiding relates right and left distributivity in a symmetric setting.

Русский

Аналогично для правого распределения и braiding; braiding связывает правое и левое распределение в симметричной обстановке.

LaTeX

$$$(coprodComparison (tensorRight X) Y Z) \\circ (β_{(Y ⨿ Z) X})^{\\mathrm{hom}} = (coprod.map (β_Y X)^{\\mathrm{hom}} (β_Z X)^{\\mathrm{hom}}) \\circ coprodComparison (tensorLeft X) Y Z$$$

Lean4

/-- In a symmetric monoidal category, the right distributivity is equal to
the left distributivity up to braiding isomorphisms. -/
@[simp]
theorem coprodComparison_tensorRight_braiding_hom [SymmetricCategory C] {X Y Z : C} :
    (coprodComparison (tensorRight X) Y Z) ≫ (β_ (Y ⨿ Z) X).hom =
      (coprod.map (β_ Y X).hom (β_ Z X).hom) ≫ (coprodComparison (tensorLeft X) Y Z) :=
  by simp [coprodComparison]

Похожие утверждения