Categories with chosen finite products

We introduce a class, CartesianMonoidalCategory, which bundles explicit choices for a terminal object and binary products in a category C. This is primarily useful for categories which have finite products with good definitional properties, such as the category of types.

For better defeqs, we also extend MonoidalCategory.

Implementation notes

For Cartesian monoidal categories, the oplax-monoidal/monoidal/braided structure of a functor F preserving finite products is uniquely determined. See the ofChosenFiniteProducts declarations.

We however develop the theory for any F.OplaxMonoidal/F.Monoidal/F.Braided instance instead of requiring it to be the ofChosenFiniteProducts one. This is to avoid diamonds: Consider e.g. 𝟭 C and F ⋙ G.

In applications requiring a finite-product-preserving functor to be oplax-monoidal/monoidal/braided, avoid attribute [local instance] ofChosenFiniteProducts but instead turn on the corresponding ofChosenFiniteProducts declaration for that functor only.

Projects

• Construct an instance of chosen finite products in the category of affine scheme, using the tensor product.
• Construct chosen finite products in other categories appearing "in nature".

class CategoryTheory.SemiCartesianMonoidalCategory (C : Type u) [Category.{v, u} C] extends CategoryTheory.MonoidalCategory C : Type (max u v)

A monoidal category is semicartesian if the unit for the tensor product is a terminal object.

• tensorObj : C → C → C
• whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂
• whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y
• tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂
• tensorUnit : C
• associator (X Y Z : C) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
• leftUnitor (X : C) : tensorObj (tensorUnit C) X ≅ X
• rightUnitor (X : C) : tensorObj X (tensorUnit C) ≅ X
• tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorHom f g = CategoryStruct.comp (whiskerRight f X₂) (whiskerLeft Y₁ g)
• id_tensorHom_id (X₁ X₂ : C) : tensorHom (CategoryStruct.id X₁) (CategoryStruct.id X₂) = CategoryStruct.id (tensorObj X₁ X₂)
• tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂)
• whiskerLeft_id (X Y : C) : whiskerLeft X (CategoryStruct.id Y) = CategoryStruct.id (tensorObj X Y)
• id_whiskerRight (X Y : C) : whiskerRight (CategoryStruct.id X) Y = CategoryStruct.id (tensorObj X Y)
• associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))
• leftUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerLeft (tensorUnit C) f) (leftUnitor Y).hom = CategoryStruct.comp (leftUnitor X).hom f
• rightUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerRight f (tensorUnit C)) (rightUnitor Y).hom = CategoryStruct.comp (rightUnitor X).hom f
• pentagon (W X Y Z : C) : CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (whiskerLeft W (associator X Y Z).hom)) = CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom
• triangle (X Y : C) : CategoryStruct.comp (associator X (tensorUnit C) Y).hom (whiskerLeft X (leftUnitor Y).hom) = whiskerRight (rightUnitor X).hom Y
• isTerminalTensorUnit : Limits.IsTerminal (MonoidalCategoryStruct.tensorUnit C)

  The tensor unit is a terminal object.

• fst (X Y : C) : MonoidalCategoryStruct.tensorObj X Y ⟶ X

  The first projection from the product.

• snd (X Y : C) : MonoidalCategoryStruct.tensorObj X Y ⟶ Y

  The second projection from the product.

• fst_def (X Y : C) : fst X Y = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (isTerminalTensorUnit.from Y)) (MonoidalCategoryStruct.rightUnitor X).hom
• snd_def (X Y : C) : snd X Y = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (isTerminalTensorUnit.from X) Y) (MonoidalCategoryStruct.leftUnitor Y).hom

def CategoryTheory.SemiCartesianMonoidalCategory.toUnit {C : Type u} [Category.{v, u} C] [SemiCartesianMonoidalCategory C] (X : C) : X ⟶ MonoidalCategoryStruct.tensorUnit C

The unique map to the terminal object.

Equations

• CategoryTheory.SemiCartesianMonoidalCategory.toUnit X = CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from X

instance CategoryTheory.SemiCartesianMonoidalCategory.instUniqueHomTensorUnit {C : Type u} [Category.{v, u} C] [SemiCartesianMonoidalCategory C] (X : C) : Unique (X ⟶ MonoidalCategoryStruct.tensorUnit C)

Equations

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

theorem CategoryTheory.SemiCartesianMonoidalCategory.default_eq_toUnit {C : Type u} [Category.{v, u} C] [SemiCartesianMonoidalCategory C] (X : C) : default = toUnit X

theorem CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique {C : Type u} [Category.{v, u} C] [SemiCartesianMonoidalCategory C] {X : C} (f g : X ⟶ MonoidalCategoryStruct.tensorUnit C) : f = g

This lemma follows from the preexisting Unique instance, but it is often convenient to use it directly as apply toUnit_unique forcing lean to do the necessary elaboration.

theorem CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique_iff {C : Type u} [Category.{v, u} C] [SemiCartesianMonoidalCategory C] {X : C} {f g : X ⟶ MonoidalCategoryStruct.tensorUnit C} : f = g ↔ True

@[simp]

theorem CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unit {C : Type u} [Category.{v, u} C] [SemiCartesianMonoidalCategory C] : toUnit (MonoidalCategoryStruct.tensorUnit C) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit {C : Type u} [Category.{v, u} C] [SemiCartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f (toUnit Y) = toUnit X

@[simp]

theorem CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit_assoc {C : Type u} [Category.{v, u} C] [SemiCartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (toUnit Y) h) = CategoryStruct.comp (toUnit X) h

class CategoryTheory.CartesianMonoidalCategory (C : Type u) [Category.{v, u} C] extends CategoryTheory.SemiCartesianMonoidalCategory C : Type (max u v)

An instance of CartesianMonoidalCategory C bundles an explicit choice of a binary product of two objects of C, and a terminal object in C.

Users should use the monoidal notation: X ⊗ Y for the product and 𝟙_ C for the terminal object.

• tensorObj : C → C → C
• whiskerLeft (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂) : tensorObj X Y₁ ⟶ tensorObj X Y₂
• whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y
• tensorHom {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂
• tensorUnit : C
• associator (X Y Z : C) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)
• leftUnitor (X : C) : tensorObj (tensorUnit C) X ≅ X
• rightUnitor (X : C) : tensorObj X (tensorUnit C) ≅ X
• tensorHom_def {X₁ Y₁ X₂ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorHom f g = CategoryStruct.comp (whiskerRight f X₂) (whiskerLeft Y₁ g)
• id_tensorHom_id (X₁ X₂ : C) : tensorHom (CategoryStruct.id X₁) (CategoryStruct.id X₂) = CategoryStruct.id (tensorObj X₁ X₂)
• tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryStruct.comp (tensorHom f₁ f₂) (tensorHom g₁ g₂) = tensorHom (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂)
• whiskerLeft_id (X Y : C) : whiskerLeft X (CategoryStruct.id Y) = CategoryStruct.id (tensorObj X Y)
• id_whiskerRight (X Y : C) : whiskerRight (CategoryStruct.id X) Y = CategoryStruct.id (tensorObj X Y)
• associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (tensorHom (tensorHom f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom f₁ (tensorHom f₂ f₃))
• leftUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerLeft (tensorUnit C) f) (leftUnitor Y).hom = CategoryStruct.comp (leftUnitor X).hom f
• rightUnitor_naturality {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (whiskerRight f (tensorUnit C)) (rightUnitor Y).hom = CategoryStruct.comp (rightUnitor X).hom f
• pentagon (W X Y Z : C) : CategoryStruct.comp (whiskerRight (associator W X Y).hom Z) (CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (whiskerLeft W (associator X Y Z).hom)) = CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom
• triangle (X Y : C) : CategoryStruct.comp (associator X (tensorUnit C) Y).hom (whiskerLeft X (leftUnitor Y).hom) = whiskerRight (rightUnitor X).hom Y
• isTerminalTensorUnit : Limits.IsTerminal (MonoidalCategoryStruct.tensorUnit C)
• fst (X Y : C) : MonoidalCategoryStruct.tensorObj X Y ⟶ X
• snd (X Y : C) : MonoidalCategoryStruct.tensorObj X Y ⟶ Y
• fst_def (X Y : C) : fst X Y = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (isTerminalTensorUnit.from Y)) (MonoidalCategoryStruct.rightUnitor X).hom
• snd_def (X Y : C) : snd X Y = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (isTerminalTensorUnit.from X) Y) (MonoidalCategoryStruct.leftUnitor Y).hom
• tensorProductIsBinaryProduct (X Y : C) : Limits.IsLimit (Limits.BinaryFan.mk (fst X Y) (snd X Y))

  The monoidal product is the categorical product.

@[deprecated CategoryTheory.CartesianMonoidalCategory (since := "2025-05-15")]

def CategoryTheory.ChosenFiniteProducts (C : Type u) [Category.{v, u} C] : Type (max u v)

Alias of CategoryTheory.CartesianMonoidalCategory.

---

An instance of CartesianMonoidalCategory C bundles an explicit choice of a binary product of two objects of C, and a terminal object in C.

Users should use the monoidal notation: X ⊗ Y for the product and 𝟙_ C for the terminal object.

Equations

• CategoryTheory.ChosenFiniteProducts = CategoryTheory.CartesianMonoidalCategory

@[reducible, inline]

abbrev CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) (X Y : C) : C

Implementation of the tensor product for CartesianMonoidalCategory.ofChosenFiniteProducts.

Equations

• CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorObj ℬ X Y = (ℬ X Y).cone.pt

@[reducible, inline]

abbrev CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : tensorObj ℬ X₁ X₂ ⟶ tensorObj ℬ Y₁ Y₂

Implementation of the tensor product of morphisms for CartesianMonoidalCategory.ofChosenFiniteProducts.

Equations

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

theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.id_tensorHom_id {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) (X Y : C) : tensorHom ℬ (CategoryStruct.id X) (CategoryStruct.id Y) = CategoryStruct.id (tensorObj ℬ X Y)

@[deprecated CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.id_tensorHom_id (since := "2025-07-14")]

theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensor_id {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) (X Y : C) : tensorHom ℬ (CategoryStruct.id X) (CategoryStruct.id Y) = CategoryStruct.id (tensorObj ℬ X Y)

Alias of CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.id_tensorHom_id.

theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom_comp_tensorHom {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryStruct.comp (tensorHom ℬ f₁ f₂) (tensorHom ℬ g₁ g₂) = tensorHom ℬ (CategoryStruct.comp f₁ g₁) (CategoryStruct.comp f₂ g₂)

theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.pentagon {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) (W X Y Z : C) : CategoryStruct.comp (tensorHom ℬ (Limits.BinaryFan.associatorOfLimitCone ℬ W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (Limits.BinaryFan.associatorOfLimitCone ℬ W (tensorObj ℬ X Y) Z).hom (tensorHom ℬ (CategoryStruct.id W) (Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).hom)) = CategoryStruct.comp (Limits.BinaryFan.associatorOfLimitCone ℬ (tensorObj ℬ W X) Y Z).hom (Limits.BinaryFan.associatorOfLimitCone ℬ W X (tensorObj ℬ Y Z)).hom

theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.triangle {C : Type u} [Category.{v, u} C] (𝒯 : Limits.LimitCone (Functor.empty C)) (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) (X Y : C) : CategoryStruct.comp (Limits.BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom (tensorHom ℬ (CategoryStruct.id X) (Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt Y).isLimit).hom) = tensorHom ℬ (Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X 𝒯.cone.pt).isLimit).hom (CategoryStruct.id Y)

theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.leftUnitor_naturality {C : Type u} [Category.{v, u} C] (𝒯 : Limits.LimitCone (Functor.empty C)) (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) {X₁ X₂ : C} (f : X₁ ⟶ X₂) : CategoryStruct.comp (tensorHom ℬ (CategoryStruct.id 𝒯.cone.pt) f) (Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₂).isLimit).hom = CategoryStruct.comp (Limits.BinaryFan.leftUnitor 𝒯.isLimit (ℬ 𝒯.cone.pt X₁).isLimit).hom f

theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.rightUnitor_naturality {C : Type u} [Category.{v, u} C] (𝒯 : Limits.LimitCone (Functor.empty C)) (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) {X₁ X₂ : C} (f : X₁ ⟶ X₂) : CategoryStruct.comp (tensorHom ℬ f (CategoryStruct.id 𝒯.cone.pt)) (Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₂ 𝒯.cone.pt).isLimit).hom = CategoryStruct.comp (Limits.BinaryFan.rightUnitor 𝒯.isLimit (ℬ X₁ 𝒯.cone.pt).isLimit).hom f

theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.associator_naturality {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (tensorHom ℬ (tensorHom ℬ f₁ f₂) f₃) (Limits.BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom = CategoryStruct.comp (Limits.BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom (tensorHom ℬ f₁ (tensorHom ℬ f₂ f₃))

@[reducible, inline]

abbrev CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts {C : Type u} [Category.{v, u} C] (𝒯 : Limits.LimitCone (Functor.empty C)) (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) : CartesianMonoidalCategory C

Construct an instance of CartesianMonoidalCategory C given a terminal object and limit cones over arbitrary pairs of objects.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.CartesianMonoidalCategory.ofHasFiniteProducts {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] : CartesianMonoidalCategory C

Constructs an instance of CartesianMonoidalCategory C given the existence of finite products in C.

Equations

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

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

def CategoryTheory.CartesianMonoidalCategory.ofFiniteProducts {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] : CartesianMonoidalCategory C

Alias of CategoryTheory.CartesianMonoidalCategory.ofHasFiniteProducts.

---

Constructs an instance of CartesianMonoidalCategory C given the existence of finite products in C.

Equations

• @CategoryTheory.CartesianMonoidalCategory.ofFiniteProducts = @CategoryTheory.CartesianMonoidalCategory.ofHasFiniteProducts

def CategoryTheory.CartesianMonoidalCategory.lift {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) : T ⟶ MonoidalCategoryStruct.tensorObj X Y

Constructs a morphism to the product given its two components.

Equations

• CategoryTheory.CartesianMonoidalCategory.lift f g = ↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' (CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct X Y) f g)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) : CategoryStruct.comp (lift f g) (fst X Y) = f

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (fst X Y) h) = CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) : CategoryStruct.comp (lift f g) (snd X Y) = g

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (snd X Y) h) = CategoryStruct.comp g h

instance CategoryTheory.CartesianMonoidalCategory.mono_lift_of_mono_left {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [Mono f] : Mono (lift f g)

instance CategoryTheory.CartesianMonoidalCategory.mono_lift_of_mono_right {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y) [Mono g] : Mono (lift f g)

theorem CategoryTheory.CartesianMonoidalCategory.hom_ext {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {T X Y : C} (f g : T ⟶ MonoidalCategoryStruct.tensorObj X Y) (h_fst : CategoryStruct.comp f (fst X Y) = CategoryStruct.comp g (fst X Y)) (h_snd : CategoryStruct.comp f (snd X Y) = CategoryStruct.comp g (snd X Y)) : f = g

theorem CategoryTheory.CartesianMonoidalCategory.hom_ext_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {T X Y : C} {f g : T ⟶ MonoidalCategoryStruct.tensorObj X Y} : f = g ↔ CategoryStruct.comp f (fst X Y) = CategoryStruct.comp g (fst X Y) ∧ CategoryStruct.comp f (snd X Y) = CategoryStruct.comp g (snd X Y)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.comp_lift {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {V W X Y : C} (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) : CategoryStruct.comp f (lift g h) = lift (CategoryStruct.comp f g) (CategoryStruct.comp f h)

theorem CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {V W X Y : C} (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) {Z : C} (h✝ : MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (lift g h) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f g) (CategoryStruct.comp f h)) h✝

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_fst_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} : lift (fst X Y) (snd X Y) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj X Y)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_comp_fst_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z : C} (f : X ⟶ MonoidalCategoryStruct.tensorObj Y Z) : lift (CategoryStruct.comp f (fst Y Z)) (CategoryStruct.comp f (snd Y Z)) = f

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X f) (fst X Z) = fst X Y

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X f) (CategoryStruct.comp (fst X Z) h) = CategoryStruct.comp (fst X Y) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X f) (snd X Z) = CategoryStruct.comp (snd X Y) f

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X f) (CategoryStruct.comp (snd X Z) h) = CategoryStruct.comp (snd X Y) (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) (fst Y Z) = CategoryStruct.comp (fst X Z) f

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.whiskerRight_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) (CategoryStruct.comp (fst Y Z) h) = CategoryStruct.comp (fst X Z) (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) (snd Y Z) = snd X Z

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Z) (CategoryStruct.comp (snd Y Z) h) = CategoryStruct.comp (snd X Z) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorHom_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (fst X₂ Y₂) = CategoryStruct.comp (fst X₁ Y₁) f

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorHom_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) {Z : C} (h : X₂ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (CategoryStruct.comp (fst X₂ Y₂) h) = CategoryStruct.comp (fst X₁ Y₁) (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorHom_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (snd X₂ Y₂) = CategoryStruct.comp (snd X₁ Y₁) g

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorHom_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) {Z : C} (h : Y₂ ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f g) (CategoryStruct.comp (snd X₂ Y₂) h) = CategoryStruct.comp (snd X₁ Y₁) (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_map {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) : CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.tensorHom h k) = lift (CategoryStruct.comp f h) (CategoryStruct.comp g k)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_map_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {V W X Y Z : C} (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj Y Z ⟶ Z✝) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom h k) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f h) (CategoryStruct.comp g k)) h✝

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_fst_comp_snd_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) : lift (CategoryStruct.comp (fst W Y) g) (CategoryStruct.comp (snd W Y) g') = MonoidalCategoryStruct.tensorHom g g'

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W) : CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.whiskerRight h Z) = lift (CategoryStruct.comp f h) g

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj W Z ⟶ Z✝) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h Z) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f h) g) h✝

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Z ⟶ W) : CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.whiskerLeft Y h) = lift f (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Z ⟶ W) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj Y W ⟶ Z✝) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft Y h) h✝) = CategoryStruct.comp (lift f (CategoryStruct.comp g h)) h✝

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.associator_hom_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (fst X (MonoidalCategoryStruct.tensorObj Y Z)) = CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (fst X Y)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).hom (CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (snd Y Z)) = snd (MonoidalCategoryStruct.tensorObj X Y) Z

@[simp]

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

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj X Y) Z) (fst X Y)) = fst X (MonoidalCategoryStruct.tensorObj Y Z)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.associator_inv_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X Y Z : C) : CategoryStruct.comp (MonoidalCategoryStruct.associator X Y Z).inv (snd (MonoidalCategoryStruct.tensorObj X Y) Z) = CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorObj Y Z)) (snd Y Z)

@[simp]

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

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) : CategoryStruct.comp (lift (lift f g) h) (MonoidalCategoryStruct.associator Y Z W).hom = lift f (lift g h)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_hom_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj Y (MonoidalCategoryStruct.tensorObj Z W) ⟶ Z✝) : CategoryStruct.comp (lift (lift f g) h) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y Z W).hom h✝) = CategoryStruct.comp (lift f (lift g h)) h✝

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) : CategoryStruct.comp (lift f (lift g h)) (MonoidalCategoryStruct.associator Y Z W).inv = lift (lift f g) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_inv_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) {Z✝ : C} (h✝ : MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorObj Y Z) W ⟶ Z✝) : CategoryStruct.comp (lift f (lift g h)) (CategoryStruct.comp (MonoidalCategoryStruct.associator Y Z W).inv h✝) = CategoryStruct.comp (lift (lift f g) h) h✝

theorem CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) : (MonoidalCategoryStruct.leftUnitor X).hom = snd (MonoidalCategoryStruct.tensorUnit C) X

theorem CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) : (MonoidalCategoryStruct.rightUnitor X).hom = fst X (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (fst (MonoidalCategoryStruct.tensorUnit C) X) = toUnit X

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorUnit C) X) h) = CategoryStruct.comp (toUnit X) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (snd (MonoidalCategoryStruct.tensorUnit C) X) = CategoryStruct.id X

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.leftUnitor_inv_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).inv (CategoryStruct.comp (snd (MonoidalCategoryStruct.tensorUnit C) X) h) = h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (fst X (MonoidalCategoryStruct.tensorUnit C)) = CategoryStruct.id X

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (CategoryStruct.comp (fst X (MonoidalCategoryStruct.tensorUnit C)) h) = h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (snd X (MonoidalCategoryStruct.tensorUnit C)) = toUnit X

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).inv (CategoryStruct.comp (snd X (MonoidalCategoryStruct.tensorUnit C)) h) = CategoryStruct.comp (toUnit X) h

theorem CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (toUnit Y)) (MonoidalCategoryStruct.rightUnitor X).hom = fst X Y

theorem CategoryTheory.CartesianMonoidalCategory.whiskerLeft_toUnit_comp_rightUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X Y : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (toUnit Y)) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom h) = CategoryStruct.comp (fst X Y) h

theorem CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X Y : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (toUnit X) Y) (MonoidalCategoryStruct.leftUnitor Y).hom = snd X Y

theorem CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X Y : C) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (toUnit X) Y) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).hom h) = CategoryStruct.comp (snd X Y) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_leftUnitor_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) (g : X ⟶ Y) : CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.leftUnitor Y).hom = g

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_leftUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} (f : X ⟶ MonoidalCategoryStruct.tensorUnit C) (g : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor Y).hom h) = CategoryStruct.comp g h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_rightUnitor_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (g : X ⟶ MonoidalCategoryStruct.tensorUnit C) : CategoryStruct.comp (lift f g) (MonoidalCategoryStruct.rightUnitor Y).hom = f

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_rightUnitor_hom_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y : C} (f : X ⟶ Y) (g : X ⟶ MonoidalCategoryStruct.tensorUnit C) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor Y).hom h) = CategoryStruct.comp f h

def CategoryTheory.CartesianMonoidalCategory.homEquivToProd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z : C} : (Z ⟶ MonoidalCategoryStruct.tensorObj X Y) ≃ (Z ⟶ X) × (Z ⟶ Y)

Universal property of the Cartesian product: Maps to X ⊗ Y correspond to pairs of maps to X and to Y.

Equations

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

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.homEquivToProd_symm_apply {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z : C} (f : (Z ⟶ X) × (Z ⟶ Y)) : homEquivToProd.symm f = lift f.1 f.2

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.homEquivToProd_apply {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X Y Z : C} (f : Z ⟶ MonoidalCategoryStruct.tensorObj X Y) : homEquivToProd f = (CategoryStruct.comp f (fst X Y), CategoryStruct.comp f (snd X Y))

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X Y : C) : CategoryStruct.comp (β_ X Y).hom (fst Y X) = snd X Y

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X Y : C) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (β_ X Y).hom (CategoryStruct.comp (fst Y X) h) = CategoryStruct.comp (snd X Y) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X Y : C) : CategoryStruct.comp (β_ X Y).hom (snd Y X) = fst X Y

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X Y : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (β_ X Y).hom (CategoryStruct.comp (snd Y X) h) = CategoryStruct.comp (fst X Y) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X Y : C) : CategoryStruct.comp (β_ X Y).inv (fst X Y) = snd Y X

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.braiding_inv_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X Y : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (β_ X Y).inv (CategoryStruct.comp (fst X Y) h) = CategoryStruct.comp (snd Y X) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X Y : C) : CategoryStruct.comp (β_ X Y).inv (snd X Y) = fst Y X

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.braiding_inv_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X Y : C) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (β_ X Y).inv (CategoryStruct.comp (snd X Y) h) = CategoryStruct.comp (fst Y X) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorμ_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (W X Y Z : C) : CategoryStruct.comp (MonoidalCategory.tensorμ W X Y Z) (fst (MonoidalCategoryStruct.tensorObj W Y) (MonoidalCategoryStruct.tensorObj X Z)) = MonoidalCategoryStruct.tensorHom (fst W X) (fst Y Z)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorμ_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (W X Y Z : C) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj W Y ⟶ Z✝) : CategoryStruct.comp (MonoidalCategory.tensorμ W X Y Z) (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj W Y) (MonoidalCategoryStruct.tensorObj X Z)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (fst W X) (fst Y Z)) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorμ_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (W X Y Z : C) : CategoryStruct.comp (MonoidalCategory.tensorμ W X Y Z) (snd (MonoidalCategoryStruct.tensorObj W Y) (MonoidalCategoryStruct.tensorObj X Z)) = MonoidalCategoryStruct.tensorHom (snd W X) (snd Y Z)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorμ_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (W X Y Z : C) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategory.tensorμ W X Y Z) (CategoryStruct.comp (snd (MonoidalCategoryStruct.tensorObj W Y) (MonoidalCategoryStruct.tensorObj X Z)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (snd W X) (snd Y Z)) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorδ_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (W X Y Z : C) : CategoryStruct.comp (MonoidalCategory.tensorδ W X Y Z) (fst (MonoidalCategoryStruct.tensorObj W X) (MonoidalCategoryStruct.tensorObj Y Z)) = MonoidalCategoryStruct.tensorHom (fst W Y) (fst X Z)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorδ_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (W X Y Z : C) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj W X ⟶ Z✝) : CategoryStruct.comp (MonoidalCategory.tensorδ W X Y Z) (CategoryStruct.comp (fst (MonoidalCategoryStruct.tensorObj W X) (MonoidalCategoryStruct.tensorObj Y Z)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (fst W Y) (fst X Z)) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorδ_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (W X Y Z : C) : CategoryStruct.comp (MonoidalCategory.tensorδ W X Y Z) (snd (MonoidalCategoryStruct.tensorObj W X) (MonoidalCategoryStruct.tensorObj Y Z)) = MonoidalCategoryStruct.tensorHom (snd W Y) (snd X Z)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.tensorδ_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (W X Y Z : C) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj Y Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategory.tensorδ W X Y Z) (CategoryStruct.comp (snd (MonoidalCategoryStruct.tensorObj W X) (MonoidalCategoryStruct.tensorObj Y Z)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (snd W Y) (snd X Z)) h

theorem CategoryTheory.CartesianMonoidalCategory.lift_snd_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X Y : C} : lift (snd X Y) (fst X Y) = (β_ X Y).hom

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) : lift (CategoryStruct.comp (snd W Y) g') (CategoryStruct.comp (fst W Y) g) = CategoryStruct.comp (β_ W Y).hom (MonoidalCategoryStruct.tensorHom g' g)

theorem CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj Z X ⟶ Z✝) : CategoryStruct.comp (lift (CategoryStruct.comp (snd W Y) g') (CategoryStruct.comp (fst W Y) g)) h = CategoryStruct.comp (β_ W Y).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom g' g) h)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_braiding_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) : CategoryStruct.comp (lift f g) (β_ X Y).hom = lift g f

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_braiding_hom_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorObj Y X ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (β_ X Y).hom h) = CategoryStruct.comp (lift g f) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_braiding_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) : CategoryStruct.comp (lift f g) (β_ Y X).inv = lift g f

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.lift_braiding_inv_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C} (h : MonoidalCategoryStruct.tensorObj Y X ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (β_ Y X).inv h) = CategoryStruct.comp (lift g f) h

@[instance 100]

instance CategoryTheory.CartesianMonoidalCategory.toSymmetricCategory {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : SymmetricCategory C

Equations

• CategoryTheory.CartesianMonoidalCategory.toSymmetricCategory = { toBraidedCategory := inst✝, symmetry := ⋯ }

def CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : BraidedCategory C

CartesianMonoidalCategory implies BraidedCategory. This is not an instance to prevent diamonds.

Equations

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

@[deprecated CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory (since := "2025-05-15")]

def CategoryTheory.BraidedCategory.ofChosenFiniteProducts {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : BraidedCategory C

Alias of CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory.

---

CartesianMonoidalCategory implies BraidedCategory. This is not an instance to prevent diamonds.

Equations

• @CategoryTheory.BraidedCategory.ofChosenFiniteProducts = @CategoryTheory.BraidedCategory.ofCartesianMonoidalCategory

instance CategoryTheory.CartesianMonoidalCategory.instNonemptyBraidedCategory {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : Nonempty (BraidedCategory C)

instance CategoryTheory.CartesianMonoidalCategory.instSubsingletonBraidedCategory {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : Subsingleton (BraidedCategory C)

instance CategoryTheory.CartesianMonoidalCategory.instSubsingletonSymmetricCategory {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : Subsingleton (SymmetricCategory C)

@[instance 100]

instance CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : Limits.HasFiniteProducts C

@[reducible, inline]

abbrev CategoryTheory.CartesianMonoidalCategory.terminalComparison {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ MonoidalCategoryStruct.tensorUnit D

When C and D have chosen finite products and F : C ⥤ D is any functor, terminalComparison F is the unique map F (𝟙_ C) ⟶ 𝟙_ D.

Equations

• CategoryTheory.CartesianMonoidalCategory.terminalComparison F = CategoryTheory.SemiCartesianMonoidalCategory.toUnit (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

theorem CategoryTheory.CartesianMonoidalCategory.map_toUnit_comp_terminalComparison {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A : C) : CategoryStruct.comp (F.map (toUnit A)) (terminalComparison F) = toUnit (F.obj A)

theorem CategoryTheory.CartesianMonoidalCategory.map_toUnit_comp_terminalComparison_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A : C) {Z : D} (h : MonoidalCategoryStruct.tensorUnit D ⟶ Z) : CategoryStruct.comp (F.map (toUnit A)) (CategoryStruct.comp (terminalComparison F) h) = CategoryStruct.comp (toUnit (F.obj A)) h

theorem CategoryTheory.CartesianMonoidalCategory.preservesLimit_empty_of_isIso_terminalComparison {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) [IsIso (terminalComparison F)] : Limits.PreservesLimit (Functor.empty C) F

If terminalComparison F is an Iso, then F preserves terminal objects.

noncomputable def CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) [h : Limits.PreservesLimit (Functor.empty C) F] : F.obj (MonoidalCategoryStruct.tensorUnit C) ≅ MonoidalCategoryStruct.tensorUnit D

If F preserves terminal objects, then terminalComparison F is an isomorphism.

Equations

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

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) [Limits.PreservesLimit (Functor.empty C) F] : (preservesTerminalIso F).hom = terminalComparison F

instance CategoryTheory.CartesianMonoidalCategory.terminalComparison_isIso_of_preservesLimits {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) [Limits.PreservesLimit (Functor.empty C) F] : IsIso (terminalComparison F)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_id {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : preservesTerminalIso (Functor.id C) = Iso.refl ((Functor.id C).obj (MonoidalCategoryStruct.tensorUnit C))

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {E : Type u₂} [Category.{v₂, u₂} E] [CartesianMonoidalCategory E] (G : Functor D E) [Limits.PreservesLimit (Functor.empty C) F] [Limits.PreservesLimit (Functor.empty D) G] [Limits.PreservesLimit (Functor.empty C) (F.comp G)] : preservesTerminalIso (F.comp G) = G.mapIso (preservesTerminalIso F) ≪≫ preservesTerminalIso G

def CategoryTheory.CartesianMonoidalCategory.prodComparison {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) : F.obj (MonoidalCategoryStruct.tensorObj A B) ⟶ MonoidalCategoryStruct.tensorObj (F.obj A) (F.obj B)

When C and D have chosen finite products and F : C ⥤ D is any functor, prodComparison F A B is the canonical comparison morphism from F (A ⊗ B) to F(A) ⊗ F(B).

Equations

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

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) : CategoryStruct.comp (prodComparison F A B) (fst (F.obj A) (F.obj B)) = F.map (fst A B)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) {Z : D} (h : F.obj A ⟶ Z) : CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (fst (F.obj A) (F.obj B)) h) = CategoryStruct.comp (F.map (fst A B)) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) : CategoryStruct.comp (prodComparison F A B) (snd (F.obj A) (F.obj B)) = F.map (snd A B)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) {Z : D} (h : F.obj B ⟶ Z) : CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (snd (F.obj A) (F.obj B)) h) = CategoryStruct.comp (F.map (snd A B)) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] : CategoryStruct.comp (inv (prodComparison F A B)) (F.map (fst A B)) = fst (F.obj A) (F.obj B)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] {Z : D} (h : F.obj A ⟶ Z) : CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (fst A B)) h) = CategoryStruct.comp (fst (F.obj A) (F.obj B)) h

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] : CategoryStruct.comp (inv (prodComparison F A B)) (F.map (snd A B)) = snd (F.obj A) (F.obj B)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.inv_prodComparison_map_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] {Z : D} (h : F.obj B ⟶ Z) : CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (snd A B)) h) = CategoryStruct.comp (snd (F.obj A) (F.obj B)) h

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_natural {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B A' B' : C} (f : A ⟶ A') (g : B ⟶ B') : CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (prodComparison F A' B') = CategoryStruct.comp (prodComparison F A B) (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g))

Naturality of the prodComparison morphism in both arguments.

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B A' B' : C} (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj A') (F.obj B') ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) (CategoryStruct.comp (prodComparison F A' B') h) = CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) h)

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B B' : C} (g : B ⟶ B') : CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft A g)) (prodComparison F A B') = CategoryStruct.comp (prodComparison F A B) (MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g))

Naturality of the prodComparison morphism in the right argument.

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B B' : C} (g : B ⟶ B') {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj A) (F.obj B') ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft A g)) (CategoryStruct.comp (prodComparison F A B') h) = CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g)) h)

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerRight {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B A' : C} (f : A ⟶ A') : CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f B)) (prodComparison F A' B) = CategoryStruct.comp (prodComparison F A B) (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B))

Naturality of the prodComparison morphism in the left argument.

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B A' : C} (f : A ⟶ A') {Z : D} (h : MonoidalCategoryStruct.tensorObj (F.obj A') (F.obj B) ⟶ Z) : CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f B)) (CategoryStruct.comp (prodComparison F A' B) h) = CategoryStruct.comp (prodComparison F A B) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B)) h)

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B A' B' : C} [IsIso (prodComparison F A B)] (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A' B')] : CategoryStruct.comp (inv (prodComparison F A B)) (F.map (MonoidalCategoryStruct.tensorHom f g)) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (inv (prodComparison F A' B'))

If the product comparison morphism is an iso, its inverse is natural in both argument.

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B A' B' : C} [IsIso (prodComparison F A B)] (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A' B')] {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj A' B') ⟶ Z) : CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.tensorHom f g)) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) (CategoryStruct.comp (inv (prodComparison F A' B')) h)

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerLeft {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B B' : C} [IsIso (prodComparison F A B)] (g : B ⟶ B') [IsIso (prodComparison F A B')] : CategoryStruct.comp (inv (prodComparison F A B)) (F.map (MonoidalCategoryStruct.whiskerLeft A g)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g)) (inv (prodComparison F A B'))

If the product comparison morphism is an iso, its inverse is natural in the right argument.

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerLeft_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B B' : C} [IsIso (prodComparison F A B)] (g : B ⟶ B') [IsIso (prodComparison F A B')] {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj A B') ⟶ Z) : CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerLeft A g)) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g)) (CategoryStruct.comp (inv (prodComparison F A B')) h)

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerRight {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B A' : C} [IsIso (prodComparison F A B)] (f : A ⟶ A') [IsIso (prodComparison F A' B)] : CategoryStruct.comp (inv (prodComparison F A B)) (F.map (MonoidalCategoryStruct.whiskerRight f B)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B)) (inv (prodComparison F A' B))

If the product comparison morphism is an iso, its inverse is natural in the left argument.

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_inv_natural_whiskerRight_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {A B A' : C} [IsIso (prodComparison F A B)] (f : A ⟶ A') [IsIso (prodComparison F A' B)] {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorObj A' B) ⟶ Z) : CategoryStruct.comp (inv (prodComparison F A B)) (CategoryStruct.comp (F.map (MonoidalCategoryStruct.whiskerRight f B)) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B)) (CategoryStruct.comp (inv (prodComparison F A' B)) h)

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {E : Type u₂} [Category.{v₂, u₂} E] [CartesianMonoidalCategory E] (G : Functor D E) {A B : C} : prodComparison (F.comp G) A B = CategoryStruct.comp (G.map (prodComparison F A B)) (prodComparison G (F.obj A) (F.obj B))

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparison_id {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A B : C} : prodComparison (Functor.id C) A B = CategoryStruct.id (MonoidalCategoryStruct.tensorObj A B)

def CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A : C) : ((MonoidalCategory.curriedTensor C).obj A).comp F ⟶ F.comp ((MonoidalCategory.curriedTensor D).obj (F.obj A))

The product comparison morphism from F(A ⊗ -) to FA ⊗ F-, whose components are given by prodComparison.

Equations

• CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A = { app := fun (B : C) => CategoryTheory.CartesianMonoidalCategory.prodComparison F A B, naturality := ⋯ }

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_app {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) : (prodComparisonNatTrans F A).app B = prodComparison F A B

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {E : Type u₂} [Category.{v₂, u₂} E] [CartesianMonoidalCategory E] (G : Functor D E) {A : C} : prodComparisonNatTrans (F.comp G) A = CategoryStruct.comp (Functor.whiskerRight (prodComparisonNatTrans F A) G) (F.whiskerLeft (prodComparisonNatTrans G (F.obj A)))

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans_id {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {A : C} : prodComparisonNatTrans (Functor.id C) A = CategoryStruct.id (((MonoidalCategory.curriedTensor C).obj A).comp (Functor.id C))

def CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) : (MonoidalCategory.curriedTensor C).comp ((Functor.whiskeringRight C C D).obj F) ⟶ F.comp ((MonoidalCategory.curriedTensor D).comp ((Functor.whiskeringLeft C D D).obj F))

The product comparison morphism from F(- ⊗ -) to F- ⊗ F-, whose components are given by prodComparison.

Equations

• CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F = { app := fun (A : C) => CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A, naturality := ⋯ }

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_app {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A : C) : (prodComparisonBifunctorNatTrans F).app A = prodComparisonNatTrans F A

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) {E : Type u₂} [Category.{v₂, u₂} E] [CartesianMonoidalCategory E] (G : Functor D E) : prodComparisonBifunctorNatTrans (F.comp G) = CategoryStruct.comp (Functor.whiskerRight (prodComparisonBifunctorNatTrans F) ((Functor.whiskeringRight C D E).obj G)) (F.whiskerLeft (Functor.whiskerRight (prodComparisonBifunctorNatTrans G) ((Functor.whiskeringLeft C D E).obj F)))

instance CategoryTheory.CartesianMonoidalCategory.instIsIsoFunctorProdComparisonNatTransOfProdComparison {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A : C) [∀ (B : C), IsIso (prodComparison F A B)] : IsIso (prodComparisonNatTrans F A)

instance CategoryTheory.CartesianMonoidalCategory.instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) [∀ (A B : C), IsIso (prodComparison F A B)] : IsIso (prodComparisonBifunctorNatTrans F)

noncomputable def CategoryTheory.CartesianMonoidalCategory.isLimitCartesianMonoidalCategoryOfPreservesLimits {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) (A B : C) [Limits.PreservesLimit (Limits.pair A B) F] : Limits.IsLimit (Limits.BinaryFan.mk (F.map (fst A B)) (F.map (snd A B)))

If F preserves the limit of the pair (A, B), then the binary fan given by (F.map fst A B, F.map (snd A B)) is a limit cone.

Equations

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

@[deprecated CategoryTheory.CartesianMonoidalCategory.isLimitCartesianMonoidalCategoryOfPreservesLimits (since := "2025-05-15")]

def CategoryTheory.CartesianMonoidalCategory.isLimitChosenFiniteProductsOfPreservesLimits {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] (F : Functor C D) (A B : C) [Limits.PreservesLimit (Limits.pair A B) F] : Limits.IsLimit (Limits.BinaryFan.mk (F.map (fst A B)) (F.map (snd A B)))

Alias of CategoryTheory.CartesianMonoidalCategory.isLimitCartesianMonoidalCategoryOfPreservesLimits.

---

If F preserves the limit of the pair (A, B), then the binary fan given by (F.map fst A B, F.map (snd A B)) is a limit cone.

Equations

• @CategoryTheory.CartesianMonoidalCategory.isLimitChosenFiniteProductsOfPreservesLimits = @CategoryTheory.CartesianMonoidalCategory.isLimitCartesianMonoidalCategoryOfPreservesLimits

noncomputable def CategoryTheory.CartesianMonoidalCategory.prodComparisonIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) [Limits.PreservesLimit (Limits.pair A B) F] : F.obj (MonoidalCategoryStruct.tensorObj A B) ≅ MonoidalCategoryStruct.tensorObj (F.obj A) (F.obj B)

If F preserves the limit of the pair (A, B), then prodComparison F A B is an isomorphism.

Equations

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

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) [Limits.PreservesLimit (Limits.pair A B) F] : (prodComparisonIso F A B).hom = prodComparison F A B

instance CategoryTheory.CartesianMonoidalCategory.isIso_prodComparison_of_preservesLimit_pair {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) [Limits.PreservesLimit (Limits.pair A B) F] : IsIso (prodComparison F A B)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_id {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A B : C) : prodComparisonIso (Functor.id C) A B = Iso.refl ((Functor.id C).obj (MonoidalCategoryStruct.tensorObj A B))

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) {E : Type u₂} [Category.{v₂, u₂} E] [CartesianMonoidalCategory E] (G : Functor D E) [Limits.PreservesLimit (Limits.pair A B) F] [Limits.PreservesLimit (Limits.pair A B) (F.comp G)] [Limits.PreservesLimit (Limits.pair (F.obj A) (F.obj B)) G] : prodComparisonIso (F.comp G) A B = G.mapIso (prodComparisonIso F A B) ≪≫ prodComparisonIso G (F.obj A) (F.obj B)

noncomputable def CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A : C) [∀ (B : C), Limits.PreservesLimit (Limits.pair A B) F] : ((MonoidalCategory.curriedTensor C).obj A).comp F ≅ F.comp ((MonoidalCategory.curriedTensor D).obj (F.obj A))

The natural isomorphism F(A ⊗ -) ≅ FA ⊗ F-, provided each prodComparison F A B is an isomorphism (as B changes).

Equations

• CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso F A = CategoryTheory.asIso (CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A : C) [∀ (B : C), Limits.PreservesLimit (Limits.pair A B) F] : (prodComparisonNatIso F A).inv = inv (prodComparisonNatTrans F A)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonNatIso_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A : C) [∀ (B : C), Limits.PreservesLimit (Limits.pair A B) F] : (prodComparisonNatIso F A).hom = prodComparisonNatTrans F A

noncomputable def CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) [∀ (A B : C), Limits.PreservesLimit (Limits.pair A B) F] : (MonoidalCategory.curriedTensor C).comp ((Functor.whiskeringRight C C D).obj F) ≅ F.comp ((MonoidalCategory.curriedTensor D).comp ((Functor.whiskeringLeft C D D).obj F))

The natural isomorphism of bifunctors F(- ⊗ -) ≅ F- ⊗ F-, provided each prodComparison F A B is an isomorphism.

Equations

• CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso F = CategoryTheory.asIso (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) [∀ (A B : C), Limits.PreservesLimit (Limits.pair A B) F] : (prodComparisonBifunctorNatIso F).hom = prodComparisonBifunctorNatTrans F

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) [∀ (A B : C), Limits.PreservesLimit (Limits.pair A B) F] : (prodComparisonBifunctorNatIso F).inv = inv (prodComparisonBifunctorNatTrans F)

theorem CategoryTheory.CartesianMonoidalCategory.preservesLimit_pair_of_isIso_prodComparison {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) (A B : C) [IsIso (prodComparison F A B)] : Limits.PreservesLimit (Limits.pair A B) F

If prodComparison F A B is an isomorphism, then F preserves the limit of pair A B.

theorem CategoryTheory.CartesianMonoidalCategory.preservesLimitsOfShape_discrete_walkingPair_of_isIso_prodComparison {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u₁} [Category.{v₁, u₁} D] [CartesianMonoidalCategory D] (F : Functor C D) [∀ (A B : C), IsIso (prodComparison F A B)] : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F

If prodComparison F A B is an isomorphism for all A B then F preserves limits of shape Discrete (WalkingPair).

noncomputable def CategoryTheory.CartesianMonoidalCategory.tensorLeftIsoProd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [Limits.HasBinaryProducts C] (X : C) : MonoidalCategory.tensorLeft X ≅ Limits.prod.functor.obj X

In a cartesian monoidal category, tensorLeft X is naturally isomorphic prod.functor.obj X.

Equations

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

instance CategoryTheory.CartesianMonoidalCategory.fullSubcategory {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] : CartesianMonoidalCategory P.FullSubcategory

The restriction of a Cartesian-monoidal category along an object property that's closed under finite products is Cartesian-monoidal.

Equations

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

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X : P.FullSubcategory) : (MonoidalCategoryStruct.leftUnitor X).inv = P.fullyFaithfulι.preimage (MonoidalCategoryStruct.leftUnitor X.obj).inv

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorProductIsBinaryProduct_lift {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X Y : P.FullSubcategory) (t : Limits.Cone (Limits.pair X Y)) : (tensorProductIsBinaryProduct X Y).lift t = lift (Limits.BinaryFan.fst t) (Limits.BinaryFan.snd t)

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] {X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : MonoidalCategoryStruct.tensorHom f g = MonoidalCategoryStruct.tensorHom f g

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X Y : P.FullSubcategory) : snd X Y = snd X.obj Y.obj

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X : P.FullSubcategory) : (MonoidalCategoryStruct.rightUnitor X).inv = P.fullyFaithfulι.preimage (MonoidalCategoryStruct.rightUnitor X.obj).inv

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_isTerminalTensorUnit_lift {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (s : Limits.Cone (Functor.empty P.FullSubcategory)) : isTerminalTensorUnit.lift s = toUnit s.pt.obj

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X Y : P.FullSubcategory) : fst X Y = fst X.obj Y.obj

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorObj_obj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X Y : P.FullSubcategory) : (MonoidalCategoryStruct.tensorObj X Y).obj = MonoidalCategoryStruct.tensorObj X.obj Y.obj

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_leftUnitor_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X : P.FullSubcategory) : (MonoidalCategoryStruct.leftUnitor X).hom = P.fullyFaithfulι.preimage (MonoidalCategoryStruct.leftUnitor X.obj).hom

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerLeft {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X x✝ x✝¹ : P.FullSubcategory) (f : x✝ ⟶ x✝¹) : MonoidalCategoryStruct.whiskerLeft X f = MonoidalCategoryStruct.whiskerLeft X.obj f

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_rightUnitor_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X : P.FullSubcategory) : (MonoidalCategoryStruct.rightUnitor X).hom = P.fullyFaithfulι.preimage (MonoidalCategoryStruct.rightUnitor X.obj).hom

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerRight {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] {X₁✝ X₂✝ : P.FullSubcategory} (f : X₁✝ ⟶ X₂✝) (X : P.FullSubcategory) : MonoidalCategoryStruct.whiskerRight f X = MonoidalCategoryStruct.whiskerRight f X.obj

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_tensorUnit_obj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] : (MonoidalCategoryStruct.tensorUnit P.FullSubcategory).obj = MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X Y Z : P.FullSubcategory) : (MonoidalCategoryStruct.associator X Y Z).inv = P.fullyFaithfulι.preimage (MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).inv

@[simp]

theorem CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {P : ObjectProperty C} [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderLimitsOfShape (Discrete Limits.WalkingPair)] (X Y Z : P.FullSubcategory) : (MonoidalCategoryStruct.associator X Y Z).hom = P.fullyFaithfulι.preimage (MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).hom

theorem CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] : η F = CartesianMonoidalCategory.terminalComparison F

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_fst {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y : C) : CategoryStruct.comp (δ F X Y) (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj Y)) = F.map (SemiCartesianMonoidalCategory.fst X Y)

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (δ F X Y) (CategoryStruct.comp (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj Y)) h) = CategoryStruct.comp (F.map (SemiCartesianMonoidalCategory.fst X Y)) h

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_snd {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y : C) : CategoryStruct.comp (δ F X Y) (SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj Y)) = F.map (SemiCartesianMonoidalCategory.snd X Y)

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.δ_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y : C) {Z : D} (h : F.obj Y ⟶ Z) : CategoryStruct.comp (δ F X Y) (CategoryStruct.comp (SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj Y)) h) = CategoryStruct.comp (F.map (SemiCartesianMonoidalCategory.snd X Y)) h

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.lift_δ {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) {X Y Z : C} [F.OplaxMonoidal] (f : X ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (F.map (CartesianMonoidalCategory.lift f g)) (δ F Y Z) = CartesianMonoidalCategory.lift (F.map f) (F.map g)

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.lift_δ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) {X Y Z : C} [F.OplaxMonoidal] (f : X ⟶ Y) (g : X ⟶ Z) {Z✝ : D} (h : MonoidalCategoryStruct.tensorObj (F.obj Y) (F.obj Z) ⟶ Z✝) : CategoryStruct.comp (F.map (CartesianMonoidalCategory.lift f g)) (CategoryStruct.comp (δ F Y Z) h) = CategoryStruct.comp (CartesianMonoidalCategory.lift (F.map f) (F.map g)) h

theorem CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] (X Y : C) : δ F X Y = CartesianMonoidalCategory.prodComparison F X Y

instance CategoryTheory.Functor.OplaxMonoidal.instIsIsoη {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] [Limits.PreservesFiniteProducts F] : IsIso (η F)

instance CategoryTheory.Functor.OplaxMonoidal.instIsIsoδ {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.OplaxMonoidal] [Limits.PreservesFiniteProducts F] (X Y : C) : IsIso (δ F X Y)

def CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) : F.OplaxMonoidal

Any functor between Cartesian-monoidal categories is oplax monoidal.

This is not made an instance because it would create a diamond for the oplax monoidal structure on the identity and composition of functors.

Equations

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

instance CategoryTheory.Functor.OplaxMonoidal.instSubsingleton {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) : Subsingleton F.OplaxMonoidal

Any functor between Cartesian-monoidal categories is oplax monoidal in a unique way.

@[simp]

theorem CategoryTheory.Functor.Monoidal.toUnit_ε {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) : CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (F.obj X)) (LaxMonoidal.ε F) = F.map (SemiCartesianMonoidalCategory.toUnit X)

@[simp]

theorem CategoryTheory.Functor.Monoidal.toUnit_ε_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (X : C) {Z : D} (h : F.obj (MonoidalCategoryStruct.tensorUnit C) ⟶ Z) : CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (F.obj X)) (CategoryStruct.comp (LaxMonoidal.ε F) h) = CategoryStruct.comp (F.map (SemiCartesianMonoidalCategory.toUnit X)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.lift_μ {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) {X Y Z : C} [F.Monoidal] (f : X ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift (F.map f) (F.map g)) (LaxMonoidal.μ F Y Z) = F.map (CartesianMonoidalCategory.lift f g)

@[simp]

theorem CategoryTheory.Functor.Monoidal.lift_μ_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) {X Y Z : C} [F.Monoidal] (f : X ⟶ Y) (g : X ⟶ Z) {Z✝ : D} (h : F.obj (MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z✝) : CategoryStruct.comp (CartesianMonoidalCategory.lift (F.map f) (F.map g)) (CategoryStruct.comp (LaxMonoidal.μ F Y Z) h) = CategoryStruct.comp (F.map (CartesianMonoidalCategory.lift f g)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.μ_fst {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : CategoryStruct.comp (LaxMonoidal.μ F X Y) (F.map (SemiCartesianMonoidalCategory.fst X Y)) = SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj Y)

@[simp]

theorem CategoryTheory.Functor.Monoidal.μ_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) {Z : D} (h : F.obj X ⟶ Z) : CategoryStruct.comp (LaxMonoidal.μ F X Y) (CategoryStruct.comp (F.map (SemiCartesianMonoidalCategory.fst X Y)) h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj Y)) h

@[simp]

theorem CategoryTheory.Functor.Monoidal.μ_snd {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) : CategoryStruct.comp (LaxMonoidal.μ F X Y) (F.map (SemiCartesianMonoidalCategory.snd X Y)) = SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj Y)

@[simp]

theorem CategoryTheory.Functor.Monoidal.μ_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (X Y : C) {Z : D} (h : F.obj Y ⟶ Z) : CategoryStruct.comp (LaxMonoidal.μ F X Y) (CategoryStruct.comp (F.map (SemiCartesianMonoidalCategory.snd X Y)) h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj Y)) h

theorem CategoryTheory.Functor.Monoidal.μ_comp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.Monoidal] [G.Monoidal] [(F.comp G).Monoidal] (X Y : C) : LaxMonoidal.μ (F.comp G) X Y = CategoryStruct.comp (LaxMonoidal.μ G (F.obj X) (F.obj Y)) (G.map (LaxMonoidal.μ F X Y))

theorem CategoryTheory.Functor.Monoidal.μ_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] (F : Functor C D) (G : Functor D E) [F.Monoidal] [G.Monoidal] [(F.comp G).Monoidal] (X Y : C) {Z : E} (h : G.obj (F.obj (MonoidalCategoryStruct.tensorObj X Y)) ⟶ Z) : CategoryStruct.comp (LaxMonoidal.μ (F.comp G) X Y) h = CategoryStruct.comp (LaxMonoidal.μ G (F.obj X) (F.obj Y)) (CategoryStruct.comp (G.map (LaxMonoidal.μ F X Y)) h)

theorem CategoryTheory.Functor.Monoidal.ε_of_cartesianMonoidalCategory {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] [Limits.PreservesFiniteProducts F] : LaxMonoidal.ε F = (CartesianMonoidalCategory.preservesTerminalIso F).inv

theorem CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] [Limits.PreservesFiniteProducts F] (X Y : C) : LaxMonoidal.μ F X Y = (CartesianMonoidalCategory.prodComparisonIso F X Y).inv

noncomputable def CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [Limits.PreservesFiniteProducts F] : F.Monoidal

A finite-product-preserving functor between Cartesian monoidal categories is monoidal.

This is not made an instance because it would create a diamond for the monoidal structure on the identity and composition of functors.

Equations

• CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts F = CategoryTheory.Functor.Monoidal.ofOplaxMonoidal F

instance CategoryTheory.Functor.Monoidal.instSubsingleton {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) : Subsingleton F.Monoidal

instance CategoryTheory.Functor.Monoidal.instPreservesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] : Limits.PreservesFiniteProducts F

theorem CategoryTheory.Functor.Monoidal.nonempty_monoidal_iff_preservesFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) : Nonempty F.Monoidal ↔ Limits.PreservesFiniteProducts F

A functor between Cartesian monoidal categories is monoidal iff it preserves finite products.

noncomputable def CategoryTheory.Functor.Braided.ofChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory C] [BraidedCategory D] (F : Functor C D) [Limits.PreservesFiniteProducts F] : F.Braided

A finite-product-preserving functor between Cartesian monoidal categories is braided.

This is not made an instance because it would create a diamond for the monoidal structure on the identity and composition of functors.

Equations

• CategoryTheory.Functor.Braided.ofChosenFiniteProducts F = { toMonoidal := CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts F, braided := ⋯ }

instance CategoryTheory.Functor.Braided.instSubsingleton {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [BraidedCategory C] [BraidedCategory D] : Subsingleton F.Braided

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

def CategoryTheory.Functor.oplaxMonoidalOfChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) : F.OplaxMonoidal

Alias of CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts.

---

Any functor between Cartesian-monoidal categories is oplax monoidal.

This is not made an instance because it would create a diamond for the oplax monoidal structure on the identity and composition of functors.

Equations

• @CategoryTheory.Functor.oplaxMonoidalOfChosenFiniteProducts = @CategoryTheory.Functor.OplaxMonoidal.ofChosenFiniteProducts

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

def CategoryTheory.Functor.monoidalOfChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [Limits.PreservesFiniteProducts F] : F.Monoidal

Alias of CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts.

---

A finite-product-preserving functor between Cartesian monoidal categories is monoidal.

This is not made an instance because it would create a diamond for the monoidal structure on the identity and composition of functors.

Equations

• @CategoryTheory.Functor.monoidalOfChosenFiniteProducts = @CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts

@[deprecated CategoryTheory.Functor.Braided.ofChosenFiniteProducts (since := "2025-04-24")]

def CategoryTheory.Functor.braidedOfChosenFiniteProducts {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory C] [BraidedCategory D] (F : Functor C D) [Limits.PreservesFiniteProducts F] : F.Braided

Alias of CategoryTheory.Functor.Braided.ofChosenFiniteProducts.

---

A finite-product-preserving functor between Cartesian monoidal categories is braided.

This is not made an instance because it would create a diamond for the monoidal structure on the identity and composition of functors.

Equations

• @CategoryTheory.Functor.braidedOfChosenFiniteProducts = @CategoryTheory.Functor.Braided.ofChosenFiniteProducts

theorem CategoryTheory.Functor.EssImageSubcategory.tensor_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y : F.EssImageSubcategory) : (MonoidalCategoryStruct.tensorObj X Y).obj = MonoidalCategoryStruct.tensorObj X.obj Y.obj

theorem CategoryTheory.Functor.EssImageSubcategory.lift_def {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] {T X Y : F.EssImageSubcategory} (f : T ⟶ X) (g : T ⟶ Y) : CartesianMonoidalCategory.lift f g = CartesianMonoidalCategory.lift f g

theorem CategoryTheory.Functor.EssImageSubcategory.associator_hom_def {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y Z : F.EssImageSubcategory) : (MonoidalCategoryStruct.associator X Y Z).hom = (MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).hom

theorem CategoryTheory.Functor.EssImageSubcategory.associator_inv_def {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X Y Z : F.EssImageSubcategory) : (MonoidalCategoryStruct.associator X Y Z).inv = (MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).inv

theorem CategoryTheory.Functor.EssImageSubcategory.toUnit_def {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Full] [F.Faithful] [Limits.PreservesFiniteProducts F] (X : F.EssImageSubcategory) : SemiCartesianMonoidalCategory.toUnit X = SemiCartesianMonoidalCategory.toUnit X.obj

instance CategoryTheory.NatTrans.IsMonoidal.of_cartesianMonoidalCategory {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F G : Functor C D) [F.Monoidal] [G.Monoidal] (α : F ⟶ G) : IsMonoidal α