The natural monoidal structure on any category with finite (co)products.

A category with a monoidal structure provided in this way is sometimes called a (co-)Cartesian category, although this is also sometimes used to mean a finitely complete category. (See https://ncatlab.org/nlab/show/cartesian+category.)

As this works with either products or coproducts, and sometimes we want to think of a different monoidal structure entirely, we don't set up either construct as an instance.

TODO

Once we have cocartesian-monoidal categories, replace monoidalOfHasFiniteCoproducts and symmetricOfHasFiniteCoproducts with CocartesianMonoidalCategory.ofHasFiniteCoproducts.

@[instance_reducible]

noncomputable def CategoryTheory.monoidalOfHasFiniteCoproducts (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] : MonoidalCategory C

A category with an initial object and binary coproducts has a natural monoidal structure.

Equations

• CategoryTheory.monoidalOfHasFiniteCoproducts C = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.tensorObj (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X Y : C) : MonoidalCategoryStruct.tensorObj X Y = (X ⨿ Y)

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.tensorHom (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : MonoidalCategoryStruct.tensorHom f g = Limits.coprod.map f g

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerLeft (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) {Y Z : C} (f : Y ⟶ Z) : MonoidalCategoryStruct.whiskerLeft X f = Limits.coprod.map (CategoryStruct.id X) f

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerRight (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] {X Y : C} (f : X ⟶ Y) (Z : C) : MonoidalCategoryStruct.whiskerRight f Z = Limits.coprod.map f (CategoryStruct.id Z)

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_hom (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) : (MonoidalCategoryStruct.leftUnitor X).hom = Limits.coprod.desc (Limits.initial.to X) (CategoryStruct.id X)

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_hom (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) : (MonoidalCategoryStruct.rightUnitor X).hom = Limits.coprod.desc (CategoryStruct.id X) (Limits.initial.to X)

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_inv (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) : (MonoidalCategoryStruct.leftUnitor X).inv = Limits.coprod.inr

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_inv (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X : C) : (MonoidalCategoryStruct.rightUnitor X).inv = Limits.coprod.inl

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.associator_hom (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X Y Z : C) : (MonoidalCategoryStruct.associator X Y Z).hom = Limits.coprod.desc (Limits.coprod.desc Limits.coprod.inl (CategoryStruct.comp Limits.coprod.inl Limits.coprod.inr)) (CategoryStruct.comp Limits.coprod.inr Limits.coprod.inr)

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.associator_inv (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X Y Z : C) : (MonoidalCategoryStruct.associator X Y Z).inv = Limits.coprod.desc (CategoryStruct.comp Limits.coprod.inl Limits.coprod.inl) (Limits.coprod.desc (CategoryStruct.comp Limits.coprod.inr Limits.coprod.inl) Limits.coprod.inr)

@[instance_reducible]

noncomputable def CategoryTheory.symmetricOfHasFiniteCoproducts (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] : SymmetricCategory C

The monoidal structure coming from finite coproducts is symmetric.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.symmetricOfHasFiniteCoproducts_braiding (C : Type u) [Category.{v, u} C] [Limits.HasInitial C] [Limits.HasBinaryCoproducts C] (X Y : C) : β_ X Y = Limits.coprod.braiding X Y