isMonoidalDistrib_of_isMonoidalLeftDistrib

English

In a symmetric monoidal category with braiding, the left distributivity equals the right distributivity up to braiding; the braiding maps adjust the two distributivities.

Русский

В симметричной моноидальной категории braiding переводит левое распределение в правое, позволяя тождественно сопоставлять distributivity.

LaTeX

$$$(coprodComparison (tensorLeft X) Y Z) \\; ≪≫ \\; (β_X (Y ⨿ Z)).hom = (coprod.map (β_X Y).hom (β_X Z).hom) ≪≫ (coprodComparison (tensorRight X) Y Z)$$$

Lean4

/-- A left distributive symmetric monoidal category is distributive. -/
theorem isMonoidalDistrib_of_isMonoidalLeftDistrib [SymmetricCategory C] [IsMonoidalLeftDistrib C] : IsMonoidalDistrib C
    where
  preservesBinaryCoproducts_tensorRight
    X := preservesColimitsOfShape_of_natIso (BraidedCategory.tensorLeftIsoTensorRight X)

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