# 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 .)

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.

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

Equations
Instances For
theorem CategoryTheory.monoidalOfHasFiniteProducts.unit_ext (C : Type u) {X : C} (f : X 𝟙_ C) (g : X 𝟙_ C) :
f = g
theorem CategoryTheory.monoidalOfHasFiniteProducts.tensor_ext (C : Type u) {X : C} {Y : C} {Z : C} (f : ) (g : ) (w₁ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst) (w₂ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd) :
f = g
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorHom (C : Type u) {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) :
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerLeft (C : Type u) (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteProducts.whiskerRight (C : Type u) {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteProducts.leftUnitor_hom (C : Type u) (X : C) :
= CategoryTheory.Limits.prod.snd
@[simp]
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteProducts.rightUnitor_hom (C : Type u) (X : C) :
= CategoryTheory.Limits.prod.fst
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom (C : Type u) (X : C) (Y : C) (Z : C) :
.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) (X : C) (Y : C) (Z : C) :
.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)
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_fst_assoc (C : Type u) (X : C) (Y : C) (Z : C) {Z : C} (h : X Z) :
CategoryTheory.CategoryStruct.comp .hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_fst (C : Type u) (X : C) (Y : C) (Z : C) :
CategoryTheory.CategoryStruct.comp .hom CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_fst_assoc (C : Type u) (X : C) (Y : C) (Z : C) {Z : C} (h : Y Z) :
CategoryTheory.CategoryStruct.comp .hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h)
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_fst (C : Type u) (X : C) (Y : C) (Z : C) :
CategoryTheory.CategoryStruct.comp .hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_snd_assoc (C : Type u) (X : C) (Y : C) (Z : C) {Z : C} (h : Z✝ Z) :
CategoryTheory.CategoryStruct.comp .hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_snd (C : Type u) (X : C) (Y : C) (Z : C) :
CategoryTheory.CategoryStruct.comp .hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) = CategoryTheory.Limits.prod.snd
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_fst_assoc (C : Type u) (X : C) (Y : C) (Z : C) {Z : C} (h : X Z) :
CategoryTheory.CategoryStruct.comp .inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_fst (C : Type u) (X : C) (Y : C) (Z : C) :
CategoryTheory.CategoryStruct.comp .inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_snd_assoc (C : Type u) (X : C) (Y : C) (Z : C) {Z : C} (h : Y Z) :
CategoryTheory.CategoryStruct.comp .inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h)
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_snd (C : Type u) (X : C) (Y : C) (Z : C) :
CategoryTheory.CategoryStruct.comp .inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_snd_assoc (C : Type u) (X : C) (Y : C) (Z : C) {Z : C} (h : Z✝ Z) :
CategoryTheory.CategoryStruct.comp .inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h)
theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_snd (C : Type u) (X : C) (Y : C) (Z : C) :
CategoryTheory.CategoryStruct.comp .inv CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd
@[simp]

The monoidal structure coming from finite products is symmetric.

Equations
Instances For

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

Equations
Instances For
@[simp]
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteCoproducts.tensorHom (C : Type u) {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) :
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerLeft (C : Type u) (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerRight (C : Type u) {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteCoproducts.leftUnitor_inv (C : Type u) (X : C) :
= CategoryTheory.Limits.coprod.inr
@[simp]
theorem CategoryTheory.monoidalOfHasFiniteCoproducts.rightUnitor_inv (C : Type u) (X : C) :
= CategoryTheory.Limits.coprod.inl
theorem CategoryTheory.monoidalOfHasFiniteCoproducts.associator_hom (C : Type u) (X : C) (Y : C) (Z : C) :
.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) (X : C) (Y : C) (Z : C) :
.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]

The monoidal structure coming from finite coproducts is symmetric.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.toMonoidalFunctorOfHasFiniteProducts_toLaxMonoidalFunctor_μ {C : Type u} {D : Type u_1} [] (F : ) (X : C) (Y : C) :
F.toMonoidalFunctorOfHasFiniteProducts X Y = .inv
@[simp]
theorem CategoryTheory.Functor.toMonoidalFunctorOfHasFiniteProducts_toLaxMonoidalFunctor_toFunctor {C : Type u} {D : Type u_1} [] (F : ) :
F.toMonoidalFunctorOfHasFiniteProducts.toFunctor = F
@[simp]
theorem CategoryTheory.Functor.toMonoidalFunctorOfHasFiniteProducts_toLaxMonoidalFunctor_ε {C : Type u} {D : Type u_1} [] (F : ) :
F.toMonoidalFunctorOfHasFiniteProducts =

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.instIsEquivalenceToMonoidalFunctorOfHasFiniteProducts {C : Type u} {D : Type u_1} [] (F : ) [F.IsEquivalence] :
F.toMonoidalFunctorOfHasFiniteProducts.IsEquivalence
Equations
• = inst