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

Replace monoidalOfHasFiniteProducts and symmetricOfHasFiniteProducts with CartesianMonoidalCategory.ofHasFiniteProducts.

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.

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

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

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

theorem CategoryTheory.monoidalOfHasFiniteProducts.tensor_ext_iff {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] {X Y Z : C} {f g : X ⟶ MonoidalCategoryStruct.tensorObj Y Z} : f = g ↔ CategoryStruct.comp f Limits.prod.fst = CategoryStruct.comp g Limits.prod.fst ∧ CategoryStruct.comp f Limits.prod.snd = CategoryStruct.comp g Limits.prod.snd

@[simp]

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

@[simp]

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]

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

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerLeft (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] (X : C) {Y Z : C} (f : Y ⟶ Z) : MonoidalCategoryStruct.whiskerLeft X f = Limits.prod.map (CategoryStruct.id X) f

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerRight (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] {X Y : C} (f : X ⟶ Y) (Z : C) : MonoidalCategoryStruct.whiskerRight f Z = Limits.prod.map f (CategoryStruct.id Z)

@[simp]

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]

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

@[simp]

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]

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

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)

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)

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

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

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

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

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

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

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

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

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

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

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

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

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 (C : Type u) [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasBinaryProducts C] (X Y : C) : β_ X Y = Limits.prod.braiding 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

instance CategoryTheory.monoidalOfHasFiniteProducts.instOplaxMonoidal {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [Limits.HasTerminal C] [Limits.HasBinaryProducts C] [Limits.HasTerminal D] [Limits.HasBinaryProducts D] : F.OplaxMonoidal

theorem CategoryTheory.monoidalOfHasFiniteProducts.η_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [Limits.HasTerminal C] [Limits.HasBinaryProducts C] [Limits.HasTerminal D] [Limits.HasBinaryProducts D] : Functor.OplaxMonoidal.η F = Limits.terminalComparison F

theorem CategoryTheory.monoidalOfHasFiniteProducts.δ_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [Limits.HasTerminal C] [Limits.HasBinaryProducts C] [Limits.HasTerminal D] [Limits.HasBinaryProducts D] (X Y : C) : Functor.OplaxMonoidal.δ F X Y = Limits.prodComparison F X Y

instance CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoη {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, 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] : IsIso (Functor.OplaxMonoidal.η F)

instance CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoδ {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, 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) : IsIso (Functor.OplaxMonoidal.δ F X Y)

instance CategoryTheory.monoidalOfHasFiniteProducts.instMonoidal {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, 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] : F.Monoidal

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