mathlibdocumentation

category_theory.monoidal.of_chosen_finite_products

The monoidal structure on a category with chosen finite products. #

This is a variant of the development in category_theory.monoidal.of_has_finite_products, 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 category_theory.monoidal.of_has_finite_products uses has_limit classes, the actual definitions there are opaque behind classical.choice.)

We use this in category_theory.monoidal.types 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 category_theory.limits.binary_fan.swap {C : Type u} {P Q : C}  :

Swap the two sides of a binary_fan.

Equations
@[simp]
theorem category_theory.limits.binary_fan.swap_fst {C : Type u} {P Q : C}  :
@[simp]
theorem category_theory.limits.binary_fan.swap_snd {C : Type u} {P Q : C}  :
def category_theory.limits.is_limit.swap_binary_fan {C : Type u} {P Q : C}  :

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

Equations
@[simp]
theorem category_theory.limits.is_limit.swap_binary_fan_lift {C : Type u} {P Q : C}  :
theorem category_theory.limits.has_binary_product.swap {C : Type u} (P Q : C)  :

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

def category_theory.limits.binary_fan.braiding {C : Type u} {X Y : C}  :
s.X t.X

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
def category_theory.limits.binary_fan.assoc {C : Type u} {X Y Z : C} {sXY : Y} {sYZ : Z} (Q : category_theory.limits.is_limit sYZ) (s : Z) :

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
@[simp]
theorem category_theory.limits.binary_fan.assoc_fst {C : Type u} {X Y Z : C} {sXY : Y} {sYZ : Z} (Q : category_theory.limits.is_limit sYZ) (s : Z) :
= s.fst sXY.fst
@[simp]
theorem category_theory.limits.binary_fan.assoc_snd {C : Type u} {X Y Z : C} {sXY : Y} {sYZ : Z} (Q : category_theory.limits.is_limit sYZ) (s : Z) :
def category_theory.limits.binary_fan.assoc_inv {C : Type u} {X Y Z : C} {sXY : Y} (P : category_theory.limits.is_limit sXY) {sYZ : Z} (s : sYZ.X) :

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
@[simp]
theorem category_theory.limits.binary_fan.assoc_inv_fst {C : Type u} {X Y Z : C} {sXY : Y} (P : category_theory.limits.is_limit sXY) {sYZ : Z} (s : sYZ.X) :
= P.lift (s.snd sYZ.fst))
@[simp]
theorem category_theory.limits.binary_fan.assoc_inv_snd {C : Type u} {X Y Z : C} {sXY : Y} (P : category_theory.limits.is_limit sXY) {sYZ : Z} (s : sYZ.X) :
= s.snd sYZ.snd
@[simp]
theorem category_theory.limits.is_limit.assoc_lift {C : Type u} {X Y Z : C} {sXY : Y} (P : category_theory.limits.is_limit sXY) {sYZ : Z} (Q : category_theory.limits.is_limit sYZ) {s : Z} (t : category_theory.limits.cone sYZ.X)) :
(P.assoc Q R).lift t =
def category_theory.limits.is_limit.assoc {C : Type u} {X Y Z : C} {sXY : Y} (P : category_theory.limits.is_limit sXY) {sYZ : Z} (Q : category_theory.limits.is_limit sYZ) {s : Z}  :

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

Equations
@[reducible]
def category_theory.limits.binary_fan.associator {C : Type u} {X Y Z : C} {sXY : Y} (P : category_theory.limits.is_limit sXY) {sYZ : Z} (Q : category_theory.limits.is_limit sYZ) {s : Z} {t : sYZ.X}  :
s.X t.X

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

Equations
@[reducible]
def category_theory.limits.binary_fan.associator_of_limit_cone {C : Type u} (L : Π (X Y : C), ) (X Y Z : C) :
(L (L X Y).cone.X Z).cone.X (L X (L Y Z).cone.X).cone.X

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

Equations
@[simp]
theorem category_theory.limits.binary_fan.left_unitor_inv {C : Type u} {X : C} {t : X}  :
= Q.lift (category_theory.limits.binary_fan.mk (P.lift {X := X, π := {app := category_theory.discrete.rec (pempty.rec (λ (n : pempty), {as := n} {as := n})), naturality' := _}}) (𝟙 X))
@[simp]
theorem category_theory.limits.binary_fan.left_unitor_hom {C : Type u} {X : C} {t : X}  :
def category_theory.limits.binary_fan.left_unitor {C : Type u} {X : C} {t : X}  :
t.X X

Construct a left unitor from specified limit cones.

Equations
def category_theory.limits.binary_fan.right_unitor {C : Type u} {X : C} {t : s.X}  :
t.X X

Construct a right unitor from specified limit cones.

Equations
@[simp]
theorem category_theory.limits.binary_fan.right_unitor_inv {C : Type u} {X : C} {t : s.X}  :
= Q.lift (P.lift {X := X, π := {app := category_theory.discrete.rec (pempty.rec (λ (n : pempty), {as := n} {as := n})), naturality' := _}}))
@[simp]
theorem category_theory.limits.binary_fan.right_unitor_hom {C : Type u} {X : C} {t : s.X}  :
@[reducible]
def category_theory.monoidal_of_chosen_finite_products.tensor_obj {C : Type u} (ℬ : Π (X Y : C), ) (X Y : C) :
C

Implementation of the tensor product for monoidal_of_chosen_finite_products.

Equations
@[reducible]
def category_theory.monoidal_of_chosen_finite_products.tensor_hom {C : Type u} (ℬ : Π (X Y : C), ) {W X Y Z : C} (f : W X) (g : Y Z) :

Implementation of the tensor product of morphisms for monoidal_of_chosen_finite_products.

Equations
theorem category_theory.monoidal_of_chosen_finite_products.tensor_id {C : Type u} (ℬ : Π (X Y : C), ) (X₁ X₂ : C) :
theorem category_theory.monoidal_of_chosen_finite_products.tensor_comp {C : Type u} (ℬ : Π (X Y : C), ) {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :
theorem category_theory.monoidal_of_chosen_finite_products.triangle {C : Type u} (ℬ : Π (X Y : C), ) (X Y : C) :
theorem category_theory.monoidal_of_chosen_finite_products.left_unitor_naturality {C : Type u} (ℬ : Π (X Y : C), ) {X₁ X₂ : C} (f : X₁ X₂) :
= .hom f
theorem category_theory.monoidal_of_chosen_finite_products.right_unitor_naturality {C : Type u} (ℬ : Π (X Y : C), ) {X₁ X₂ : C} (f : X₁ X₂) :
theorem category_theory.monoidal_of_chosen_finite_products.associator_naturality {C : Type u} (ℬ : Π (X Y : C), ) {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :
def category_theory.monoidal_of_chosen_finite_products {C : Type u} (ℬ : Π (X Y : C), ) :

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

Equations
@[protected, instance]
@[nolint]

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 symmetric_of_chosen_finite_products.

Equations
Instances for category_theory.monoidal_of_chosen_finite_products.monoidal_of_chosen_finite_products_synonym
@[protected, instance]
Equations
theorem category_theory.monoidal_of_chosen_finite_products.braiding_naturality {C : Type u} (ℬ : Π (X Y : C), ) {X X' Y Y' : C} (f : X Y) (g : X' Y') :
=
theorem category_theory.monoidal_of_chosen_finite_products.hexagon_forward {C : Type u} (ℬ : Π (X Y : C), ) (X Y Z : C) :
theorem category_theory.monoidal_of_chosen_finite_products.hexagon_reverse {C : Type u} (ℬ : Π (X Y : C), ) (X Y Z : C) :
theorem category_theory.monoidal_of_chosen_finite_products.symmetry {C : Type u} (ℬ : Π (X Y : C), ) (X Y : C) :
(ℬ Y X).is_limit).hom (ℬ X Y).is_limit).hom =

The monoidal structure coming from finite products is symmetric.

Equations