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.
Swap the two sides of a binary_fan
.
Equations
If a cone t
over P Q
is a limit cone, then t.swap
is a limit cone over Q P
.
Equations
- I.swap_binary_fan = {lift := λ (s : category_theory.limits.cone (category_theory.limits.pair Q P)), I.lift (category_theory.limits.binary_fan.swap s), fac' := _, uniq' := _}
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.
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.
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
- category_theory.limits.binary_fan.assoc Q s = category_theory.limits.binary_fan.mk (s.fst ≫ sXY.fst) (Q.lift (category_theory.limits.binary_fan.mk (s.fst ≫ sXY.snd) s.snd))
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
- category_theory.limits.binary_fan.assoc_inv P s = category_theory.limits.binary_fan.mk (P.lift (category_theory.limits.binary_fan.mk s.fst (s.snd ≫ sYZ.fst))) (s.snd ≫ sYZ.snd)
If all the binary fans involved a limit cones, binary_fan.assoc
produces another limit cone.
Equations
- P.assoc Q R = {lift := λ (t : category_theory.limits.cone (category_theory.limits.pair X sYZ.X)), R.lift (category_theory.limits.binary_fan.assoc_inv P t), fac' := _, uniq' := _}
Given two pairs of limit cones corresponding to the parenthesisations of X × Y × Z
,
we obtain an isomorphism between the cone points.
Equations
- category_theory.limits.binary_fan.associator P Q R S = (P.assoc Q R).cone_point_unique_up_to_iso S
Given a fixed family of limit data for every pair X Y
, we obtain an associator.
Construct a left unitor from specified limit cones.
Equations
- category_theory.limits.binary_fan.left_unitor P Q = {hom := t.snd, inv := Q.lift (category_theory.limits.binary_fan.mk (P.lift {X := X, π := {app := category_theory.discrete.rec (pempty.rec (λ (n : pempty), ((category_theory.functor.const (category_theory.discrete pempty)).obj X).obj {as := n} ⟶ (category_theory.functor.empty C).obj {as := n})), naturality' := _}}) (𝟙 X)), hom_inv_id' := _, inv_hom_id' := _}
Construct a right unitor from specified limit cones.
Equations
- category_theory.limits.binary_fan.right_unitor P Q = {hom := t.fst, inv := Q.lift (category_theory.limits.binary_fan.mk (𝟙 X) (P.lift {X := X, π := {app := category_theory.discrete.rec (pempty.rec (λ (n : pempty), ((category_theory.functor.const (category_theory.discrete pempty)).obj X).obj {as := n} ⟶ (category_theory.functor.empty C).obj {as := n})), naturality' := _}})), hom_inv_id' := _, inv_hom_id' := _}
Implementation of the tensor product for monoidal_of_chosen_finite_products
.
Equations
- category_theory.monoidal_of_chosen_finite_products.tensor_obj ℬ X Y = (ℬ X Y).cone.X
Implementation of the tensor product of morphisms for monoidal_of_chosen_finite_products
.
Equations
- category_theory.monoidal_of_chosen_finite_products.tensor_hom ℬ f g = (category_theory.limits.binary_fan.is_limit.lift' (ℬ X Z).is_limit ((ℬ W Y).cone.π.app {as := category_theory.limits.walking_pair.left} ≫ f) ((ℬ W Y).cone.π.app {as := category_theory.limits.walking_pair.right} ≫ g)).val
A category with a terminal object and binary products has a natural monoidal structure.
Equations
- category_theory.monoidal_of_chosen_finite_products 𝒯 ℬ = {tensor_obj := λ (X Y : C), category_theory.monoidal_of_chosen_finite_products.tensor_obj ℬ X Y, tensor_hom := λ (_x _x_1 _x_2 _x_3 : C) (f : _x ⟶ _x_1) (g : _x_2 ⟶ _x_3), category_theory.monoidal_of_chosen_finite_products.tensor_hom ℬ f g, tensor_id' := _, tensor_comp' := _, tensor_unit := 𝒯.cone.X, associator := λ (X Y Z : C), category_theory.limits.binary_fan.associator_of_limit_cone ℬ X Y Z, associator_naturality' := _, left_unitor := λ (X : C), category_theory.limits.binary_fan.left_unitor 𝒯.is_limit (ℬ 𝒯.cone.X X).is_limit, left_unitor_naturality' := _, right_unitor := λ (X : C), category_theory.limits.binary_fan.right_unitor 𝒯.is_limit (ℬ X 𝒯.cone.X).is_limit, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
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
The monoidal structure coming from finite products is symmetric.
Equations
- category_theory.symmetric_of_chosen_finite_products 𝒯 ℬ = {to_braided_category := {braiding := λ (X Y : category_theory.monoidal_of_chosen_finite_products.monoidal_of_chosen_finite_products_synonym 𝒯 ℬ), category_theory.limits.binary_fan.braiding (ℬ X Y).is_limit (ℬ Y X).is_limit, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}, symmetry' := _}