nLab
cartesian monoidal category

A cartesian monoidal category is a monoidal category whose monoidal structure is given by the category-theoretic product (and so whose unit is a terminal object). Any category with finite products can be considered as a cartesian monoidal category (as long as we have either (1) a specified product for each pair of objects, (2) a global axiom of choice, or (3) we allow the monoidal product to be an anafunctor). Note that the term cartesian category usually means a category with finite products but can also mean a finitely complete category.

Cartesian monoidal categories have a number of special and important properties, such as the existence of diagonal maps ${\Delta }_x:x\to x\otimes x$ and augmentations $e_x:x\to I$ for any object $x$. In applications to computer science we can think of $\Delta$ as ‘duplicating data’ and $e$ as ‘deleting’ data. These maps make any object into a comonoid. In fact, any object in a cartesian monoidal category becomes a comonoid in a unique way.

Moreover, one can show that any monoidal category equipped with suitably well-behaved diagonals and augmentations must in fact be cartesian monoidal. More precisely: suppose $C$ is a monoidal category equipped with monoidal natural transformations

$${\Delta }_x:x\to x\otimes x$$\Delta_x : x \to x \otimes x

and

$$e_x:x\to I$$e_x : x \to I

such that the following composites are identity morphisms:

$$x\stackrel{{\Delta }_x}{⟶}x\otimes x\stackrel{e_x\otimes 1}{⟶}I\otimes x\stackrel{{\ell }_x}{⟶}x$$x \stackrel{\Delta_x}{\longrightarrow} x \otimes x \stackrel{e_x \otimes 1}{\longrightarrow} I \otimes x \stackrel{\ell_x}{\longrightarrow} x

$$x\stackrel{{\Delta }_x}{⟶}x\otimes x\stackrel{1\otimes e_x}{⟶}x\otimes I\stackrel{r_x}{⟶}x$$x \stackrel{\Delta_x}{\longrightarrow} x \otimes x \stackrel{1 \otimes e_x}{\longrightarrow} x \otimes I \stackrel{r_x}{\longrightarrow} x

where $r$, $\ell$ are the right and left unitors. Then $C$ is cartesian.

Heuristically: a monoidal category is cartesian if we can duplicate and delete data, and ‘duplicating a piece of data and then deleting one copy is the same as not doing anything’.

A related theorem describes cartesian monoidal categories as monoidal categories satisfying two properties involving the unit object. First, we say a monoidal category $C$ is semicartesian if the unit for the tensor product is terminal. If this is true, any tensor product of objects $x\otimes y$ comes equipped with morphisms

$$p_x:x\otimes y\to x$$p_x : x \otimes y \to x

$$p_y:x\otimes y\to y$$p_y : x \otimes y \to y

given by

$$x\otimes y\stackrel{1\otimes e_y}{⟶}x\otimes I\stackrel{r_x}{⟶}x$$x \otimes y \stackrel{1 \otimes e_y}{\longrightarrow} x \otimes I \stackrel{r_x}{\longrightarrow} x

and

$$x\otimes y\stackrel{e_x\otimes 1}{⟶}I\otimes y\stackrel{{\ell }_y}{⟶}y$$x \otimes y \stackrel{e_x \otimes 1}{\longrightarrow} I \otimes y \stackrel{\ell_y}{\longrightarrow} y

respectively, where $e$ stands for the unique morphism to the terminal object and $r$, $\ell$ are the right and left unitors. We can thus ask whether $p_x$ and $p_y$ make $x\otimes y$ into the product of $x$ and $y$. If so, it is a theorem that $C$ is a cartesian monoidal category. (This theorem is probably in Eilenberg and Kelly’s paper on closed categories, but they may not have been the first to note it.)

A cartesian monoidal category which is also closed is called a cartesian closed category.