The monoidal structure on a category with chosen finite products.

This is a variant of the development in CategoryTheory.Monoidal.OfHasFiniteProducts, which uses specified choices of the terminal object and binary product, enabling the construction of a cartesian category with specific definitions of the tensor unit and tensor product.

(Because the construction in CategoryTheory.Monoidal.OfHasFiniteProducts uses HasLimit classes, the actual definitions there are opaque behind Classical.choice.)

We use this in CategoryTheory.Monoidal.TypeCat to construct the monoidal category of types so that the tensor product is the usual cartesian product of types.

For now we only do the construction from products, and not from coproducts, which seems less often useful.

def CategoryTheory.Limits.BinaryFan.swap {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (t : CategoryTheory.Limits.BinaryFan P Q) : CategoryTheory.Limits.BinaryFan Q P

Swap the two sides of a BinaryFan.

Equations

• CategoryTheory.Limits.BinaryFan.swap t = CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Limits.BinaryFan.snd t) (CategoryTheory.Limits.BinaryFan.fst t)

@[simp]

theorem CategoryTheory.Limits.BinaryFan.swap_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (t : CategoryTheory.Limits.BinaryFan P Q) : CategoryTheory.Limits.BinaryFan.fst (CategoryTheory.Limits.BinaryFan.swap t) = CategoryTheory.Limits.BinaryFan.snd t

@[simp]

theorem CategoryTheory.Limits.BinaryFan.swap_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} (t : CategoryTheory.Limits.BinaryFan P Q) : CategoryTheory.Limits.BinaryFan.snd (CategoryTheory.Limits.BinaryFan.swap t) = CategoryTheory.Limits.BinaryFan.fst t

@[simp]

theorem CategoryTheory.Limits.IsLimit.swapBinaryFan_lift {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {t : CategoryTheory.Limits.BinaryFan P Q} (I : CategoryTheory.Limits.IsLimit t) (s : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair Q P)) : (CategoryTheory.Limits.IsLimit.swapBinaryFan I).lift s = I.lift (CategoryTheory.Limits.BinaryFan.swap s)

def CategoryTheory.Limits.IsLimit.swapBinaryFan {C : Type u} [CategoryTheory.Category.{v, u} C] {P : C} {Q : C} {t : CategoryTheory.Limits.BinaryFan P Q} (I : CategoryTheory.Limits.IsLimit t) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.swap t)

If a binary fan t over P Q is a limit cone, then t.swap is a limit cone over Q P.

Equations

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

theorem CategoryTheory.Limits.HasBinaryProduct.swap {C : Type u} [CategoryTheory.Category.{v, u} C] (P : C) (Q : C) [CategoryTheory.Limits.HasBinaryProduct P Q] : CategoryTheory.Limits.HasBinaryProduct Q P

Construct HasBinaryProduct Q P from HasBinaryProduct P Q. This can't be an instance, as it would cause a loop in typeclass search.

def CategoryTheory.Limits.BinaryFan.braiding {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t) : s.pt ≅ t.pt

Given a limit cone over X and Y, and another limit cone over Y and X, we can construct an isomorphism between the cone points. Relative to some fixed choice of limits cones for every pair, these isomorphisms constitute a braiding.

Equations

• CategoryTheory.Limits.BinaryFan.braiding P Q = CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso P (CategoryTheory.Limits.IsLimit.swapBinaryFan Q)

def CategoryTheory.Limits.BinaryFan.assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) (s : CategoryTheory.Limits.BinaryFan sXY.pt Z) : CategoryTheory.Limits.BinaryFan X sYZ.pt

Given binary fans sXY over X Y, and sYZ over Y Z, and s over sXY.X Z, if sYZ is a limit cone we can construct a binary fan over X sYZ.X.

This is an ingredient of building the associator for a cartesian category.

Equations

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

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assoc_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) (s : CategoryTheory.Limits.BinaryFan sXY.pt Z) : CategoryTheory.Limits.BinaryFan.fst (CategoryTheory.Limits.BinaryFan.assoc Q s) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.fst s) (CategoryTheory.Limits.BinaryFan.fst sXY)

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assoc_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) (s : CategoryTheory.Limits.BinaryFan sXY.pt Z) : CategoryTheory.Limits.BinaryFan.snd (CategoryTheory.Limits.BinaryFan.assoc Q s) = Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.fst s) (CategoryTheory.Limits.BinaryFan.snd sXY)) (CategoryTheory.Limits.BinaryFan.snd s))

def CategoryTheory.Limits.BinaryFan.assocInv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit sXY) {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (s : CategoryTheory.Limits.BinaryFan X sYZ.pt) : CategoryTheory.Limits.BinaryFan sXY.pt Z

Given binary fans sXY over X Y, and sYZ over Y Z, and s over X sYZ.X, if sYZ is a limit cone we can construct a binary fan over sXY.X Z.

This is an ingredient of building the associator for a cartesian category.

Equations

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

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assocInv_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit sXY) {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (s : CategoryTheory.Limits.BinaryFan X sYZ.pt) : CategoryTheory.Limits.BinaryFan.fst (CategoryTheory.Limits.BinaryFan.assocInv P s) = P.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Limits.BinaryFan.fst s) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.snd s) (CategoryTheory.Limits.BinaryFan.fst sYZ)))

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assocInv_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit sXY) {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (s : CategoryTheory.Limits.BinaryFan X sYZ.pt) : CategoryTheory.Limits.BinaryFan.snd (CategoryTheory.Limits.BinaryFan.assocInv P s) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.snd s) (CategoryTheory.Limits.BinaryFan.snd sYZ)

@[simp]

theorem CategoryTheory.Limits.IsLimit.assoc_lift {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit sXY) {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) {s : CategoryTheory.Limits.BinaryFan sXY.pt Z} (R : CategoryTheory.Limits.IsLimit s) (t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X sYZ.pt)) : (CategoryTheory.Limits.IsLimit.assoc P Q R).lift t = R.lift (CategoryTheory.Limits.BinaryFan.assocInv P t)

def CategoryTheory.Limits.IsLimit.assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit sXY) {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) {s : CategoryTheory.Limits.BinaryFan sXY.pt Z} (R : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.assoc Q s)

If all the binary fans involved a limit cones, BinaryFan.assoc produces another limit cone.

Equations

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

@[reducible]

def CategoryTheory.Limits.BinaryFan.associator {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {sXY : CategoryTheory.Limits.BinaryFan X Y} (P : CategoryTheory.Limits.IsLimit sXY) {sYZ : CategoryTheory.Limits.BinaryFan Y Z} (Q : CategoryTheory.Limits.IsLimit sYZ) {s : CategoryTheory.Limits.BinaryFan sXY.pt Z} (R : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X sYZ.pt} (S : CategoryTheory.Limits.IsLimit t) : s.pt ≅ t.pt

Given two pairs of limit cones corresponding to the parenthesisations of X × Y × Z, we obtain an isomorphism between the cone points.

Equations

• CategoryTheory.Limits.BinaryFan.associator P Q R S = CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso (CategoryTheory.Limits.IsLimit.assoc P Q R) S

@[reducible]

def CategoryTheory.Limits.BinaryFan.associatorOfLimitCone {C : Type u} [CategoryTheory.Category.{v, u} C] (L : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X : C) (Y : C) (Z : C) : (L (L X Y).cone.pt Z).cone.pt ≅ (L X (L Y Z).cone.pt).cone.pt

Given a fixed family of limit data for every pair X Y, we obtain an associator.

Equations

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

@[simp]

theorem CategoryTheory.Limits.BinaryFan.leftUnitor_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan s.pt X} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.leftUnitor P Q).hom = CategoryTheory.Limits.BinaryFan.snd t

@[simp]

theorem CategoryTheory.Limits.BinaryFan.leftUnitor_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan s.pt X} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.leftUnitor P Q).inv = Q.lift (CategoryTheory.Limits.BinaryFan.mk (P.lift { pt := X, π := CategoryTheory.NatTrans.mk fun (x : CategoryTheory.Discrete PEmpty.{v + 1} ) => PEmpty.elim x.as }) (CategoryTheory.CategoryStruct.id { pt := X, π := CategoryTheory.NatTrans.mk fun (x : CategoryTheory.Discrete PEmpty.{v + 1} ) => PEmpty.elim x.as }.pt))

def CategoryTheory.Limits.BinaryFan.leftUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan s.pt X} (Q : CategoryTheory.Limits.IsLimit t) : t.pt ≅ X

Construct a left unitor from specified limit cones.

Equations

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

@[simp]

theorem CategoryTheory.Limits.BinaryFan.rightUnitor_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.rightUnitor P Q).inv = Q.lift (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.id X) (P.lift { pt := X, π := CategoryTheory.NatTrans.mk fun (x : CategoryTheory.Discrete PEmpty.{v + 1} ) => PEmpty.elim x.as }))

@[simp]

theorem CategoryTheory.Limits.BinaryFan.rightUnitor_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t) : (CategoryTheory.Limits.BinaryFan.rightUnitor P Q).hom = CategoryTheory.Limits.BinaryFan.fst t

def CategoryTheory.Limits.BinaryFan.rightUnitor {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan X s.pt} (Q : CategoryTheory.Limits.IsLimit t) : t.pt ≅ X

Construct a right unitor from specified limit cones.

Equations

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

@[reducible]

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

Implementation of the tensor product for MonoidalOfChosenFiniteProducts.

Equations

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

@[reducible]

def CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {W : C} {X : C} {Y : C} {Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ W Y ⟶ CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Z

Implementation of the tensor product of morphisms for MonoidalOfChosenFiniteProducts.

Equations

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

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

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

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

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

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

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

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

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

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

Equations

• CategoryTheory.monoidalOfChosenFiniteProducts 𝒯 ℬ = CategoryTheory.MonoidalCategory.ofTensorHom

def CategoryTheory.MonoidalOfChosenFiniteProducts.MonoidalOfChosenFiniteProductsSynonym {C : Type u} [CategoryTheory.Category.{v, u} C] (_𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)) (_ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) : Type u

A type synonym for C carrying a monoidal category structure corresponding to a fixed choice of limit data for the empty functor, and for pair X Y for every X Y : C.

This is an implementation detail for SymmetricOfChosenFiniteProducts.

Equations

• CategoryTheory.MonoidalOfChosenFiniteProducts.MonoidalOfChosenFiniteProductsSynonym _𝒯 _ℬ = C

instance CategoryTheory.MonoidalOfChosenFiniteProducts.instCategoryMonoidalOfChosenFiniteProductsSynonym {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)) (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) : CategoryTheory.Category.{v, u} (CategoryTheory.MonoidalOfChosenFiniteProducts.MonoidalOfChosenFiniteProductsSynonym 𝒯 ℬ)

Equations

• CategoryTheory.MonoidalOfChosenFiniteProducts.instCategoryMonoidalOfChosenFiniteProductsSynonym 𝒯 ℬ = id inferInstance

instance CategoryTheory.MonoidalOfChosenFiniteProducts.instMonoidalCategoryMonoidalOfChosenFiniteProductsSynonymInstCategoryMonoidalOfChosenFiniteProductsSynonym {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)) (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) : CategoryTheory.MonoidalCategory (CategoryTheory.MonoidalOfChosenFiniteProducts.MonoidalOfChosenFiniteProductsSynonym 𝒯 ℬ)

Equations

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