Theorems · Theorem · category theory

CategoryTheory.coprodComparison_tensorRight_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.SymmetricCategory C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorRight X) Y Z) (β_ (Y ⨿ Z) X).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (β_ Y X).hom (β_ Z X).hom)
      (CategoryTheory.Limits.coprodComparison (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z)

In a symmetric monoidal category, the right distributivity is equal to the left 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.SymmetricCategory