Theorems · Theorem · category theory

CategoryTheory.coprodComparison_tensorLeft_braiding_hom

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.BraidedCategory C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z) (β_ X (Y ⨿ Z)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (β_ X Y).hom (β_ X Z).hom)
      (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z)

In a symmetric monoidal category, the left distributivity is equal to the right distributivity up to braiding isomorphisms.

Defined in

Mathlib.CategoryTheory.Distributive.Monoidal

Cited by

0 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Limits.HasBinaryCoproductsCategoryTheory.BraidedCategory