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.

@[deprecated CategoryTheory.CartesianMonoidalCategory.ofHasFiniteProducts (since := "2025-10-19")]

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

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

@[deprecated CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique (since := "2025-10-19")]

theorem CategoryTheory.monoidalOfHasFiniteProducts.unit_ext (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] {X : C} (f g : X ⟶ MonoidalCategoryStruct.tensorUnit C) : f = g

@[deprecated CategoryTheory.CartesianMonoidalCategory.hom_ext (since := "2025-10-19")]

theorem CategoryTheory.monoidalOfHasFiniteProducts.tensor_ext (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] {X Y Z : C} (f g : X ⟶ MonoidalCategoryStruct.tensorObj Y Z) (w₁ : CategoryStruct.comp f Limits.prod.fst = CategoryStruct.comp g Limits.prod.fst) (w₂ : CategoryStruct.comp f Limits.prod.snd = CategoryStruct.comp g Limits.prod.snd) : f = g

@[simp, deprecated "This is an implementation detail." (since := "2025-10-19")]

theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorUnit (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] : MonoidalCategoryStruct.tensorUnit C = ⊤_ C

@[simp, deprecated "This is an implementation detail." (since := "2025-10-19")]

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

@[simp, deprecated CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom (since := "2025-10-19")]

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

@[simp, deprecated CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom (since := "2025-10-19")]

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

@[simp, deprecated "Use the `CartesianMonoidalCategory.associator_hom_...` lemmas" (since := "2025-10-19")]

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

@[deprecated "Use the `CartesianMonoidalCategory.associator_inv_...` lemmas" (since := "2025-10-19")]

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

@[deprecated CategoryTheory.CartesianMonoidalCategory.associator_hom_fst (since := "2025-10-19")]

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

@[deprecated CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst (since := "2025-10-19")]

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

@[deprecated CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd (since := "2025-10-19")]

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

@[deprecated CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst (since := "2025-10-19")]

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

@[deprecated CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd (since := "2025-10-19")]

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

@[deprecated CategoryTheory.CartesianMonoidalCategory.associator_inv_snd (since := "2025-10-19")]

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

@[deprecated CategoryTheory.CartesianMonoidalCategory.toSymmetricCategory (since := "2025-10-19")]

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

The monoidal structure coming from finite products is symmetric.

@[simp]

theorem CategoryTheory.symmetricOfHasFiniteProducts_braiding_inv (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] (X Y : C) : (β_ X Y).inv = CartesianMonoidalCategory.lift (SemiCartesianMonoidalCategory.snd Y X) (SemiCartesianMonoidalCategory.fst Y X)

@[simp]

theorem CategoryTheory.symmetricOfHasFiniteProducts_braiding_hom (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] (X Y : C) : (β_ X Y).hom = CartesianMonoidalCategory.lift (SemiCartesianMonoidalCategory.snd X Y) (SemiCartesianMonoidalCategory.fst X Y)

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.

@[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)

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.

@[simp]

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

@[deprecated CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts (since := "2025-10-19")]

instance CategoryTheory.monoidalOfHasFiniteProducts.instOplaxMonoidal {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) [Limits.HasTerminal C] [Limits.HasBinaryProducts C] [Limits.HasTerminal D] [Limits.HasBinaryProducts D] : have this := ⋯; have this_1 := ⋯; have this := CartesianMonoidalCategory.ofHasFiniteProducts; have this_2 := CartesianMonoidalCategory.ofHasFiniteProducts; F.OplaxMonoidal

@[deprecated "No replacement" (since := "2025-10-19")]

theorem CategoryTheory.monoidalOfHasFiniteProducts.η_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) [Limits.HasTerminal C] [Limits.HasBinaryProducts C] [Limits.HasTerminal D] [Limits.HasBinaryProducts D] : have this := ⋯; have this_1 := ⋯; have this := CartesianMonoidalCategory.ofHasFiniteProducts; have this := CartesianMonoidalCategory.ofHasFiniteProducts; Functor.OplaxMonoidal.η F = Limits.terminalComparison F

@[deprecated "No replacement" (since := "2025-10-19")]

theorem CategoryTheory.monoidalOfHasFiniteProducts.δ_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) [Limits.HasTerminal C] [Limits.HasBinaryProducts C] [Limits.HasTerminal D] [Limits.HasBinaryProducts D] (X Y : C) : have this := ⋯; have this_1 := ⋯; have this := CartesianMonoidalCategory.ofHasFiniteProducts; have this := CartesianMonoidalCategory.ofHasFiniteProducts; Functor.OplaxMonoidal.δ F X Y = Limits.prodComparison F X Y

@[deprecated inferInstance (since := "2025-10-19")]

instance CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoη {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) [Limits.HasTerminal C] [Limits.HasBinaryProducts C] [Limits.HasTerminal D] [Limits.HasBinaryProducts D] [Limits.PreservesLimit (Functor.empty C) F] : have this := ⋯; have this_1 := ⋯; have this := CartesianMonoidalCategory.ofHasFiniteProducts; have this := CartesianMonoidalCategory.ofHasFiniteProducts; IsIso (Functor.OplaxMonoidal.η F)

@[deprecated inferInstance (since := "2025-10-19")]

instance CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoδ {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) [Limits.HasTerminal C] [Limits.HasBinaryProducts C] [Limits.HasTerminal D] [Limits.HasBinaryProducts D] [Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F] (X Y : C) : have this := ⋯; have this_1 := ⋯; have this := CartesianMonoidalCategory.ofHasFiniteProducts; have this := CartesianMonoidalCategory.ofHasFiniteProducts; IsIso (Functor.OplaxMonoidal.δ F X Y)

@[deprecated CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts (since := "2025-10-19")]

instance CategoryTheory.monoidalOfHasFiniteProducts.instMonoidal {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) [Limits.HasTerminal C] [Limits.HasBinaryProducts C] [Limits.HasTerminal D] [Limits.HasBinaryProducts D] [Limits.PreservesLimit (Functor.empty C) F] [Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F] : have this := ⋯; have this_1 := ⋯; have this := CartesianMonoidalCategory.ofHasFiniteProducts; have this_2 := CartesianMonoidalCategory.ofHasFiniteProducts; F.Monoidal

Promote a functor that preserves finite products to a monoidal functor between categories equipped with the monoidal category structure given by finite products.