mathlib documentation

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.

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.

Equations

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

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

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

Equations

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

Equations

Implementation of the tensor product for monoidal_of_chosen_finite_products.

Equations
theorem category_theory.monoidal_of_chosen_finite_products.tensor_comp {C : Type u} [category_theory.category C] (ℬ : Π (X Y : C), category_theory.limits.limit_cone (category_theory.limits.pair X Y)) {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :

@[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