Theorems · Theorem · category theory

CategoryTheory.SymmetricCategory.rightDistrib_of_leftDistrib

∀ {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]
  [inst_4 : CategoryTheory.IsMonoidalDistrib C] {X Y Z : C},
  ∂R X Y Z = CategoryTheory.Limits.coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ CategoryTheory.leftDistrib X Y Z ≪≫ β_ X (Y ⨿ Z)

The right distributivity isomorphism of the a left distributive symmetric monoidal category is given by (β_ (Y ⨿ Z) X).hom ≫ (∂L X Y Z).inv ≫ (coprod.map (β_ X Y).hom (β_ X Z).hom).

Defined in

Mathlib.CategoryTheory.Distributive.Monoidal

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Limits.HasBinaryCoproductsCategoryTheory.SymmetricCategoryCategoryTheory.IsMonoidalDistrib