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.

Implementation

We had previously chosen to rely on HasTerminal and HasBinaryProducts instead of HasBinaryProducts, because we were later relying on the definitional form of the tensor product. Now that has_limit has been refactored to be a Prop, this issue is irrelevant and we could simplify the construction here.

See CategoryTheory.monoidalOfChosenFiniteProducts for a variant of this construction which allows specifying a particular choice of terminal object and binary products.

def CategoryTheory.monoidalOfHasFiniteProducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.MonoidalCategory C

A category with a terminal object and binary products has a natural monoidal structure.

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorObj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) : CategoryTheory.MonoidalCategory.tensorObj X Y = (X ⨯ Y)

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorHom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.Limits.prod.map f g

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteProducts.leftUnitor_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) : (CategoryTheory.MonoidalCategory.leftUnitor X).hom = CategoryTheory.Limits.prod.snd

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteProducts.leftUnitor_inv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) : (CategoryTheory.MonoidalCategory.leftUnitor X).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.terminal.from X) (CategoryTheory.CategoryStruct.id X)

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteProducts.rightUnitor_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) : (CategoryTheory.MonoidalCategory.rightUnitor X).hom = CategoryTheory.Limits.prod.fst

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteProducts.rightUnitor_inv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) : (CategoryTheory.MonoidalCategory.rightUnitor X).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.terminal.from X)

theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.associator X Y Z).hom = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)

theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.associator X Y Z).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)

@[simp]

theorem CategoryTheory.symmetricOfHasFiniteProducts_braiding (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) : β_ X Y = CategoryTheory.Limits.prod.braiding X Y

def CategoryTheory.symmetricOfHasFiniteProducts (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.SymmetricCategory C

The monoidal structure coming from finite products is symmetric.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

The monoidal structure coming from finite coproducts is symmetric.