# mathlibdocumentation

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.

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

Equations
@[simp]

The monoidal structure coming from finite products is symmetric.

Equations
@[simp]
theorem category_theory.monoidal_of_has_finite_products.tensor_obj (C : Type u) (X Y : C) :
X Y = (X Y)

@[simp]
theorem category_theory.monoidal_of_has_finite_products.tensor_hom (C : Type u) {W X Y Z : C} (f : W X) (g : Y Z) :

@[simp]

@[simp]

@[simp]

@[simp]

A category with an initial object and binary coproducts has a natural monoidal structure.

Equations

The monoidal structure coming from finite coproducts is symmetric.

Equations
@[simp]

@[simp]
theorem category_theory.monoidal_of_has_finite_coproducts.tensor_obj (C : Type u) (X Y : C) :
X Y = (X ⨿ Y)

@[simp]
theorem category_theory.monoidal_of_has_finite_coproducts.tensor_hom (C : Type u) {W X Y Z : C} (f : W X) (g : Y Z) :

@[simp]

@[simp]

@[simp]

@[simp]