mathlib documentation

category_theory.monoidal.of_has_finite_products

The natural monoidal structure on any category with finite (co)products.

A category with a monoidal structure provided in this way is sometimes called a (co)cartesian category, although this is also sometimes used to mean a finitely complete category. (See https://ncatlab.org/nlab/show/cartesian+category.)

As this works with either products or coproducts, and sometimes we want to think of a different monoidal structure entirely, we don't set up either construct as an instance.

Implementation

We had previously chosen to rely on has_terminal and has_binary_products instead of has_finite_products, because we were later relying on the definitional form of the tensor product. Now that has_limit has been refactored to be a Prop, this issue is irrelevant and we could simplify the construction here.

See category_theory.monoidal.of_chosen_finite_products for a variant of this construction which allows specifying a particular choice of terminal object and binary products.

The braiding isomorphism can be passed through a map by swapping the order.

theorem category_theory.limits.prod.associator_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) {X' : C} (f' : Y₁ (Y₂ Y₃) X') :