Distributive monoidal categories

Main definitions

A monoidal category C with binary coproducts is left distributive if the left tensor product preserves binary coproducts. This means that, for all objects X, Y, and Z in C, the cogap map (X ⊗ Y) ⨿ (X ⊗ Z) ⟶ X ⊗ (Y ⨿ Z) can be promoted to an isomorphism. We refer to this isomorphism as the left distributivity isomorphism.

A monoidal category C with binary coproducts is right distributive if the right tensor product preserves binary coproducts. This means that, for all objects X, Y, and Z in C, the cogap map (Y ⊗ X) ⨿ (Z ⊗ X) ⟶ (Y ⨿ Z) ⊗ X can be promoted to an isomorphism. We refer to this isomorphism as the right distributivity isomorphism.

A distributive monoidal category is a monoidal category that is both left and right distributive.

Main results

• A symmetric monoidal category is left distributive if and only if it is right distributive.

• A closed monoidal category is left distributive.

• For a category C the category of endofunctors C ⥤ C is left distributive (but almost never right distributive). The left distributivity is tantamount to the fact that the coproduct in the functor categories is computed pointwise.

• We show that any preadditive monoidal category with coproducts is distributive. This includes the examples of abelian groups, R-modules, and vector bundles.

TODO

Show that a distributive monoidal category whose unit is weakly terminal is finitary distributive.

Show that the category of pointed types with the monoidal structure given by the smash product of pointed types and the coproduct given by the wedge sum is distributive.

References

• Hans-Joachim Baues, Mamuka Jibladze, Andy Tonks, Cohomology of monoids in monoidal categories, in: Operads: Proceedings of Renaissance Conferences, Contemporary Mathematics 202, AMS (1997) 137-166

class CategoryTheory.IsMonoidalLeftDistrib (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] : Prop

A monoidal category with binary coproducts is left distributive if the left tensor product functor preserves binary coproducts.

• preservesBinaryCoproducts_tensorLeft (X : C) : Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) (MonoidalCategory.tensorLeft X)

class CategoryTheory.IsMonoidalRightDistrib (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] : Prop

A monoidal category with binary coproducts is right distributive if the right tensor product functor preserves binary coproducts.

• preservesBinaryCoproducts_tensorRight (X : C) : Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) (MonoidalCategory.tensorRight X)

class CategoryTheory.IsMonoidalDistrib (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] extends CategoryTheory.IsMonoidalLeftDistrib C, CategoryTheory.IsMonoidalRightDistrib C : Prop

A monoidal category with binary coproducts is distributive if it is both left and right distributive.

• preservesBinaryCoproducts_tensorLeft (X : C) : Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) (MonoidalCategory.tensorLeft X)
• preservesBinaryCoproducts_tensorRight (X : C) : Limits.PreservesColimitsOfShape (Discrete Limits.WalkingPair) (MonoidalCategory.tensorRight X)

def CategoryTheory.leftDistrib {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] (X Y Z : C) : MonoidalCategoryStruct.tensorObj X Y ⨿ MonoidalCategoryStruct.tensorObj X Z ≅ MonoidalCategoryStruct.tensorObj X (Y ⨿ Z)

The canonical left distributivity isomorphism

Equations

• CategoryTheory.leftDistrib X Y Z = CategoryTheory.Limits.PreservesColimitPair.iso (CategoryTheory.MonoidalCategory.tensorLeft X) Y Z

def CategoryTheory.Distributive.«term∂L» : Lean.ParserDescr

Notation for the forward direction morphism of the canonical left distributivity isomorphism

Equations

• CategoryTheory.Distributive.«term∂L» = Lean.ParserDescr.node `CategoryTheory.Distributive.«term∂L» 1024 (Lean.ParserDescr.symbol "∂L")

theorem CategoryTheory.IsMonoidalLeftDistrib.of_isIso_coprodComparisonTensorLeft {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [i : ∀ {X Y Z : C}, IsIso (Limits.coprodComparison (MonoidalCategory.tensorLeft X) Y Z)] : IsMonoidalLeftDistrib C

theorem CategoryTheory.leftDistrib_hom {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] {X Y Z : C} : (leftDistrib X Y Z).hom = Limits.coprod.desc (MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inl) (MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inr)

The forward direction of the left distributivity isomorphism is the cogap morphism coprod.desc (_ ◁ coprod.inl) (_ ◁ coprod.inr) : (X ⊗ Y) ⨿ (X ⊗ Z) ⟶ X ⊗ (Y ⨿ Z).

@[simp]

theorem CategoryTheory.coprod_inl_leftDistrib_hom {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] {X Y Z : C} : CategoryStruct.comp Limits.coprod.inl (leftDistrib X Y Z).hom = MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inl

@[simp]

theorem CategoryTheory.coprod_inl_leftDistrib_hom_assoc {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] {X Y Z Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X (Y ⨿ Z) ⟶ Z✝) : CategoryStruct.comp Limits.coprod.inl (CategoryStruct.comp (leftDistrib X Y Z).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inl) h

@[simp]

theorem CategoryTheory.coprod_inr_leftDistrib_hom {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] {X Y Z : C} : CategoryStruct.comp Limits.coprod.inr (leftDistrib X Y Z).hom = MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inr

@[simp]

theorem CategoryTheory.coprod_inr_leftDistrib_hom_assoc {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] {X Y Z Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X (Y ⨿ Z) ⟶ Z✝) : CategoryStruct.comp Limits.coprod.inr (CategoryStruct.comp (leftDistrib X Y Z).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inr) h

@[simp]

theorem CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] {X Y Z : C} : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inl) (leftDistrib X Y Z).inv = Limits.coprod.inl

The composite of (X ◁ coprod.inl) : X ⊗ Y ⟶ X ⊗ (Y ⨿ Z) and (∂L X Y Z).inv : X ⊗ (Y ⨿ Z) ⟶ (X ⊗ Y) ⨿ (X ⊗ Z) is equal to the left coprojection coprod.inl : X ⊗ Y ⟶ (X ⊗ Y) ⨿ (X ⊗ Z).

@[simp]

theorem CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv_assoc {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] {X Y Z Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X Y ⨿ MonoidalCategoryStruct.tensorObj X Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inl) (CategoryStruct.comp (leftDistrib X Y Z).inv h) = CategoryStruct.comp Limits.coprod.inl h

@[simp]

theorem CategoryTheory.whiskerLeft_coprod_inr_leftDistrib_inv {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] {X Y Z : C} : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inr) (leftDistrib X Y Z).inv = Limits.coprod.inr

The composite of (X ◁ coprod.inr) : X ⊗ Z ⟶ X ⊗ (Y ⨿ Z) and (∂L X Y Z).inv : X ⊗ (Y ⨿ Z) ⟶ (X ⊗ Y) ⨿ (X ⊗ Z) is equal to the right coprojection coprod.inr : X ⊗ Z ⟶ (X ⊗ Y) ⨿ (X ⊗ Z).

@[simp]

theorem CategoryTheory.whiskerLeft_coprod_inr_leftDistrib_inv_assoc {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] {X Y Z Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X Y ⨿ MonoidalCategoryStruct.tensorObj X Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X Limits.coprod.inr) (CategoryStruct.comp (leftDistrib X Y Z).inv h) = CategoryStruct.comp Limits.coprod.inr h

def CategoryTheory.rightDistrib {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] (X Y Z : C) : MonoidalCategoryStruct.tensorObj Y X ⨿ MonoidalCategoryStruct.tensorObj Z X ≅ MonoidalCategoryStruct.tensorObj (Y ⨿ Z) X

The canonical right distributivity isomorphism

Equations

• ∂R X Y Z = CategoryTheory.Limits.PreservesColimitPair.iso (CategoryTheory.MonoidalCategory.tensorRight X) Y Z

def CategoryTheory.Distributive.«term∂R» : Lean.ParserDescr

Notation for the forward direction morphism of the canonical right distributivity isomorphism

Equations

• CategoryTheory.Distributive.«term∂R» = Lean.ParserDescr.node `CategoryTheory.Distributive.«term∂R» 1024 (Lean.ParserDescr.symbol "∂R")

theorem CategoryTheory.IsMonoidalRightDistrib.of_isIso_coprodComparisonTensorRight {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [i : ∀ {X Y Z : C}, IsIso (Limits.coprodComparison (MonoidalCategory.tensorRight X) Y Z)] : IsMonoidalRightDistrib C

theorem CategoryTheory.rightDistrib_hom {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] {X Y Z : C} : (∂R X Y Z).hom = Limits.coprod.desc (MonoidalCategoryStruct.whiskerRight Limits.coprod.inl X) (MonoidalCategoryStruct.whiskerRight Limits.coprod.inr X)

The forward direction of the right distributivity isomorphism is equal to the cogap morphism coprod.desc (coprod.inl ▷ _) (coprod.inr ▷ _) : (Y ⊗ X) ⨿ (Z ⊗ X) ⟶ (Y ⨿ Z) ⊗ X.

@[simp]

theorem CategoryTheory.coprod_inl_rightDistrib_hom {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] {X Y Z : C} : CategoryStruct.comp Limits.coprod.inl (∂R X Y Z).hom = MonoidalCategoryStruct.whiskerRight Limits.coprod.inl X

@[simp]

theorem CategoryTheory.coprod_inl_rightDistrib_hom_assoc {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] {X Y Z Z✝ : C} (h : MonoidalCategoryStruct.tensorObj (Y ⨿ Z) X ⟶ Z✝) : CategoryStruct.comp Limits.coprod.inl (CategoryStruct.comp (∂R X Y Z).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight Limits.coprod.inl X) h

@[simp]

theorem CategoryTheory.coprod_inr_rightDistrib_hom {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] {X Y Z : C} : CategoryStruct.comp Limits.coprod.inr (∂R X Y Z).hom = MonoidalCategoryStruct.whiskerRight Limits.coprod.inr X

@[simp]

theorem CategoryTheory.coprod_inr_rightDistrib_hom_assoc {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] {X Y Z Z✝ : C} (h : MonoidalCategoryStruct.tensorObj (Y ⨿ Z) X ⟶ Z✝) : CategoryStruct.comp Limits.coprod.inr (CategoryStruct.comp (∂R X Y Z).hom h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight Limits.coprod.inr X) h

@[simp]

theorem CategoryTheory.whiskerRight_coprod_inl_rightDistrib_inv {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] {X Y Z : C} : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight Limits.coprod.inl X) (∂R X Y Z).inv = Limits.coprod.inl

The composite of (coprod.inl ▷ X) : Y ⊗ X ⟶ (Y ⨿ Z) ⊗ X and (∂R X Y Z).inv : (Y ⨿ Z) ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X) is equal to the left coprojection coprod.inl : Y ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X).

@[simp]

theorem CategoryTheory.whiskerRight_coprod_inl_rightDistrib_inv_assoc {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] {X Y Z Z✝ : C} (h : MonoidalCategoryStruct.tensorObj Y X ⨿ MonoidalCategoryStruct.tensorObj Z X ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight Limits.coprod.inl X) (CategoryStruct.comp (∂R X Y Z).inv h) = CategoryStruct.comp Limits.coprod.inl h

@[simp]

theorem CategoryTheory.whiskerRight_coprod_inr_rightDistrib_inv {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] {X Y Z : C} : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight Limits.coprod.inr X) (∂R X Y Z).inv = Limits.coprod.inr

The composite of (coprod.inr ▷ X) : Z ⊗ X ⟶ (Y ⨿ Z) ⊗ X and (∂R X Y Z).inv : (Y ⨿ Z) ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X) is equal to the right coprojection coprod.inr : Z ⊗ X ⟶ (Y ⊗ X) ⨿ (Z ⊗ X).

@[simp]

theorem CategoryTheory.whiskerRight_coprod_inr_rightDistrib_inv_assoc {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [IsMonoidalRightDistrib C] {X Y Z Z✝ : C} (h : MonoidalCategoryStruct.tensorObj Y X ⨿ MonoidalCategoryStruct.tensorObj Z X ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight Limits.coprod.inr X) (CategoryStruct.comp (∂R X Y Z).inv h) = CategoryStruct.comp Limits.coprod.inr h

@[simp]

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

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

@[simp]

theorem CategoryTheory.coprodComparison_tensorRight_braiding_hom {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [SymmetricCategory C] {X Y Z : C} : CategoryStruct.comp (Limits.coprodComparison (MonoidalCategory.tensorRight X) Y Z) (β_ (Y ⨿ Z) X).hom = CategoryStruct.comp (Limits.coprod.map (β_ Y X).hom (β_ Z X).hom) (Limits.coprodComparison (MonoidalCategory.tensorLeft X) Y Z)

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

theorem CategoryTheory.SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [SymmetricCategory C] [IsMonoidalLeftDistrib C] : IsMonoidalDistrib C

A left distributive symmetric monoidal category is distributive.

@[simp]

theorem CategoryTheory.SymmetricCategory.rightDistrib_of_leftDistrib {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [SymmetricCategory C] [IsMonoidalDistrib C] {X Y Z : C} : ∂R X Y Z = Limits.coprod.mapIso (β_ Y X) (β_ Z X) ≪≫ 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).

instance CategoryTheory.MonoidalClosed.isMonoidalLeftDistrib {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [MonoidalClosed C] : IsMonoidalLeftDistrib C

A closed monoidal category is left distributive.

instance CategoryTheory.isMonoidalDistrib.of_symmetric_monoidal_closed {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [SymmetricCategory C] [MonoidalClosed C] : IsMonoidalDistrib C

theorem CategoryTheory.MonoidalClosed.leftDistrib_inv {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [MonoidalClosed C] {X Y Z : C} : (leftDistrib X Y Z).inv = uncurry (Limits.coprod.desc (curry Limits.coprod.inl) (curry Limits.coprod.inr))

The inverse of distributivity isomorphism from the closed monoidal strurcture

instance CategoryTheory.isMonoidalLeftDistrib.of_endofunctors {C : Type u_1} [Category.{v, u_1} C] [Limits.HasBinaryCoproducts C] : IsMonoidalLeftDistrib (Functor C C)

The monoidal structure on the category of endofunctors is left distributive.

instance CategoryTheory.IsMonoidalDistrib.of_MonoidalPreadditive_with_binary_coproducts {C : Type u_1} [Category.{v, u_1} C] [MonoidalCategory C] [Limits.HasBinaryCoproducts C] [Preadditive C] [MonoidalPreadditive C] : IsMonoidalDistrib C

A preadditive monoidal category with binary biproducts is distributive.