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

Equations

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

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.

Equations

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

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

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)

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] (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

Equations

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

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.

Equations

• CategoryTheory.monoidalOfHasFiniteProducts.instMonoidal F = CategoryTheory.Functor.Monoidal.ofOplaxMonoidal F