nLab cartesian monoidal category

Contents

Context

Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

Category theory

Contents

Definition

A cartesian monoidal category (usually just called a cartesian category), is a monoidal category whose monoidal structure is given by the category-theoretic product (and so whose unit is a terminal object).

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

A strong monoidal functor between cartesian categories is called a cartesian functor.

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).

The term cartesian category usually means a category with finite products but can also mean a finitely complete category, so we avoid that term.

Properties

Among general monoidal categories, the cartesian monoidal categories have a number of special and important properties, such as the existence of diagonal maps Δ x:xxx\Delta_x : x \to x\otimes x and augmentations e x:xIe_x: x \to I for any object xx, cf. the structural rules in the corresponding internal type theory: In applications to computer science we can think of Δ\Delta as ‘duplicating data’ and ee as ‘deleting’ data. These maps make any object into a comonoid: (see also at comonoid – In a cartesian monoidal category):

Example

(comonoid objects)
In fact, any object in a cartesian monoidal category becomes a comonoid in a unique way, and this is automatically a cocommutative comonoid structure. Furthermore, this comonoid structure is ‘natural’, meaning that the all morphisms between objects preserve their comonoid structure. In other words, any morphism f:xyf: x \to y is a comonoid homomorphism:

(ff)Δ x=Δ yf,i x=i yf. (f \otimes f) \circ \Delta_x = \Delta_y \circ f, \quad i_x = i_y \circ f .

Moreover, one can show (e.g. Fox 1976 or Heunen-Vicary 2012, p. 79 (p. 85 of the pdf)) that any symmetric monoidal category equipped with suitably well-behaved diagonal and augmentation maps must in fact be cartesian monoidal. More precisely: suppose CC is a symmetric monoidal category equipped with monoidal natural transformations

Δ x:xxx \Delta_x : x \to x \otimes x

and

e x:xI e_x : x \to I

such that the following composites are identity morphisms:

xΔ xxxe x1Ix xx x \stackrel{\Delta_x}{\longrightarrow} x \otimes x \stackrel{e_x \otimes 1}{\longrightarrow} I \otimes x \stackrel{\ell_x}{\longrightarrow} x
xΔ xxx1e xxIr xx x \stackrel{\Delta_x}{\longrightarrow} x \otimes x \stackrel{1 \otimes e_x}{\longrightarrow} x \otimes I \stackrel{r_x}{\longrightarrow} x

where rr, \ell are the right and left unitors. Then CC is cartesian.

Heuristically: a symmetric 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 CC is semicartesian if the unit for the tensor product is terminal. If this is true, any tensor product of objects xyx \otimes y comes equipped with morphisms

p x:xyx p_x : x \otimes y \to x
p y:xyy p_y : x \otimes y \to y

given by

xy1e yxIr xx x \otimes y \stackrel{1 \otimes e_y}{\longrightarrow} x \otimes I \stackrel{r_x}{\longrightarrow} x

and

xye x1Iy yy x \otimes y \stackrel{e_x \otimes 1}{\longrightarrow} I \otimes y \stackrel{\ell_y}{\longrightarrow} y

respectively, where ee stands for the unique morphism to the terminal object and rr, \ell are the right and left unitors. We can thus ask whether p xp_x and p yp_y make xyx \otimes y into the product of xx and yy. If so, it is a theorem that CC 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.)

Cartesian categories may be freely generated from sets, categories, signatures, etc., as explained at free cartesian category.

Free and cofree cartesian monoidal categories

As outlined above, cartesianity is an algebraic structure on top of a monoidal structure. This means that the 2-category of cartesian monoidal categories CartMonCat\mathbf{CartMonCat} is monadic over MonCat\mathbf{MonCat}, i.e. there is a free-forgetful adjunction

UF:CartMonCatMonCat U \dashv F : \mathbf{CartMonCat} \leftrightarrows \mathbf{MonCat}

Thomas Fox showed in (Fox 1976) that Cart\mathbf{Cart} is also comonadic, that is, that UU admits a right adjoint CUC \dashv U, given by constructing the category of comonoids in a given monoidal category M\mathbf{M}.

References

The characterization of cartesian monoidal categories as symmetric monoidal categories with extra structure:

Discussion with an eye towards finite quantum mechanics in terms of dagger-compact categories is in

  • Chris Heunen, Jamie Vicary, Lectures on categorical quantum mechanics, 2012 (pdf)

  • Kosta Došen and Zoran Petrić. The maximality of cartesian categories. Mathematical Logic Quarterly: Mathematical Logic Quarterly 47.1 (2001): 137-144.

Last revised on August 23, 2023 at 11:27:51. See the history of this page for a list of all contributions to it.