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.

Equations

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

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

theorem CategoryTheory.monoidalOfHasFiniteProducts.tensor_ext (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] {X Y Z : C} (f g : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) (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]

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

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteProducts.tensorObj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y : C) : CategoryTheory.MonoidalCategoryStruct.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 X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.Limits.prod.map f g

@[simp]

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

@[simp]

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

@[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.MonoidalCategoryStruct.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.MonoidalCategoryStruct.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.MonoidalCategoryStruct.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.MonoidalCategoryStruct.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 Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.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 Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.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)

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

theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_fst_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) {Z✝ : C} (h : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).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_snd_fst (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).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_fst_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).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_snd (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) = CategoryTheory.Limits.prod.snd

theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_hom_snd_snd_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).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_inv_fst_fst (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst

theorem CategoryTheory.monoidalOfHasFiniteProducts.associator_inv_fst_fst_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) {Z✝ : C} (h : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).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_snd (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).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_fst_snd_assoc (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).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_snd (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd

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

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.

Equations

• CategoryTheory.symmetricOfHasFiniteProducts C = CategoryTheory.SymmetricCategory.mk ⋯

@[simp]

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

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.

Equations

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

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.tensorObj (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X Y : C) : CategoryTheory.MonoidalCategoryStruct.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 X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.Limits.coprod.map f g

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerLeft (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) f

@[simp]

theorem CategoryTheory.monoidalOfHasFiniteCoproducts.whiskerRight (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] [CategoryTheory.Limits.HasBinaryCoproducts C] {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z = CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id Z)

@[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.MonoidalCategoryStruct.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.MonoidalCategoryStruct.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.MonoidalCategoryStruct.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.MonoidalCategoryStruct.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 Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.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 Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.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)

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.

Equations

• CategoryTheory.symmetricOfHasFiniteCoproducts C = CategoryTheory.SymmetricCategory.mk ⋯

@[simp]

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

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

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

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

instance CategoryTheory.monoidalOfHasFiniteProducts.instIsIsoδ {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasTerminal D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] (X Y : C) : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)

instance CategoryTheory.monoidalOfHasFiniteProducts.instMonoidal {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasTerminal D] [CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.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