# nLab cartesian closed category

### Context

#### Monoidal categories

monoidal categories

## With traces

• trace

• traced monoidal category?

category theory

# Contents

## Definition

A cartesian closed category (sometimes: ccc) is a category with finite products which is closed with respect to its cartesian monoidal structure.

The internal hom $\left[S,X\right]$ in a cartesian closed category is often called exponentiation and is denoted ${X}^{S}$.

A cartesian closed functor between cartesian closed categories $C$, $D$ is a functor $F:C\to D$ that is product-preserving and that is also exponential-preserving, meaning that the canonical map

$F\left({a}^{b}\right)\to F\left(a{\right)}^{F\left(b\right)},$F(a^b) \to F(a)^{F(b)},

corresponding to the composite

$F\left({a}^{b}\right)×F\left(b\right)\cong F\left({a}^{b}×b\right)\stackrel{F\left({\mathrm{eval}}_{a,b}\right)}{\to }F\left(a\right),$F(a^b) \times F(b) \cong F(a^b \times b) \stackrel{F(eval_{a, b})}{\to} F(a),

is an isomorphism.

## Some basic consequences

A category is cartesian closed if it has finite products and if for any two objects $X$, $Y$, there is an object ${Y}^{X}$ (thought of as a “space of maps from $X$ to $Y$”) such that for any object $Z$, there is a bijection between the set of maps $Z\to {Y}^{X}$ and the set of maps $Z×X\to Y$, and this bijection is natural in $Z$.

There is an evaluation map ${\mathrm{ev}}_{X,Y}:{Y}^{X}×X\to Y$, which by definition is the map corresponding to the identity map ${Y}^{X}\to {Y}^{X}$ under the bijection. Using the naturality, it may be shown that the bijection $\mathrm{hom}\left(Z,{Y}^{X}\right)\to \mathrm{hom}\left(Z×X,Y\right)$ takes a map $\varphi :Z\to {Y}^{X}$ to the composite

$Z×X\stackrel{\varphi ×{1}_{X}}{\to }{Y}^{X}×X\stackrel{{\mathrm{ev}}_{X,Y}}{\to }Y$Z \times X \stackrel{\phi \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y

and the universal property of ${Y}^{X}$ may be phrased thus: given any $\psi :Z×X\to Y$, there exists a unique map $\varphi :Z\to {Y}^{X}$ for which $\psi ={\mathrm{ev}}_{X,Y}\circ \left(\varphi ×{1}_{X}\right)$.

Taking $Z=1$ (the terminal object), maps $1\to {Y}^{X}$ (or “points” of ${Y}^{X}$) are in bijection with maps $X\stackrel{{\pi }_{2}^{-1}}{\to }1×X\to Y$. So the “underlying set” of ${Y}^{X}$, namely $\mathrm{hom}\left(1,{Y}^{X}\right)$, is identified with the set of maps from $X$ to $Y$. Let us denote the point corresponding to $f:X\to Y$ by $\left[f\right]:1\to {Y}^{X}$. Then, by definition,

$\left(1×X\stackrel{\left[f\right]×{1}_{X}}{\to }{Y}^{X}×X\stackrel{{\mathrm{ev}}_{X,Y}}{\to }Y\right)=\left(1×X\stackrel{{\pi }_{2}}{\to }X\stackrel{f}{\to }Y\right)$(1 \times X \stackrel{[f] \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y) = (1 \times X \stackrel{\pi_2}{\to} X \stackrel{f}{\to} Y)

The following lemma says that the internal evaluation map ${\mathrm{ev}}_{X,Y}$ indeed behaves as an evaluation map at the level of underlying sets.

###### Lemma

Given a map $f:X\to Y$ and a point $x:1\to X$, the composite

$1\stackrel{⟨\left[f\right],x⟩}{\to }{Y}^{X}×X\stackrel{{\mathrm{ev}}_{X,Y}}{\to }Y$1 \stackrel{\langle [f], x \rangle}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y

is the point $fx:1\to Y$.

###### Proof

We have

$\begin{array}{ccc}1\stackrel{⟨\left[f\right],x⟩}{\to }{Y}^{X}×X\stackrel{{\mathrm{ev}}_{X,Y}}{\to }X& =& 1\stackrel{{\delta }_{1}}{\to }1×1\stackrel{\left[f\right]×x}{\to }{Y}^{X}×X\stackrel{{\mathrm{ev}}_{X,Y}}{\to }Y\\ & =& 1\stackrel{{\delta }_{1}}{\to }1×1\stackrel{1×x}{\to }1×X\stackrel{\left[f\right]×{1}_{X}}{\to }{Y}^{X}×X\stackrel{{\mathrm{ev}}_{X,Y}}{\to }Y\\ & =& 1\stackrel{{\delta }_{1}}{\to }1×1\stackrel{1×x}{\to }1×X\stackrel{{\pi }_{2}}{\to }X\stackrel{f}{\to }Y\\ & =& 1\stackrel{{\delta }_{1}}{\to }1×1\stackrel{{\pi }_{2}}{\to }1\stackrel{x}{\to }X\stackrel{f}{\to }Y\\ & =& 1\stackrel{x}{\to }X\stackrel{f}{\to }Y\end{array}$\array{ 1 \stackrel{\langle [f], x \rangle}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} X & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{[f] \times x}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y\\ & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{1 \times x}{\to} 1 \times X \stackrel{[f] \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y\\ & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{1 \times x}{\to} 1 \times X \stackrel{\pi_2}{\to} X \stackrel{f}{\to} Y\\ & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{\pi_2}{\to} 1 \stackrel{x}{\to} X \stackrel{f}{\to} Y\\ & = & 1 \stackrel{x}{\to} X \stackrel{f}{\to} Y }

where the penultimate equation uses naturality of the projection map ${\pi }_{2}$.

###### Definition

Internal composition ${c}_{X,Y,Z}:{Z}^{Y}×{Y}^{X}\to {Z}^{X}$ is the unique map such that

$\left({Z}^{Y}×{Y}^{X}×X\stackrel{c×{1}_{X}}{\to }{Z}^{X}×X\stackrel{{\mathrm{ev}}_{X,Z}}{\to }Z\right)=\left({Z}^{Y}×{Y}^{X}×X\stackrel{1×{\mathrm{ev}}_{X,Y}}{\to }{Z}^{Y}×Y\stackrel{{\mathrm{ev}}_{Y,Z}}{\to }Z\right)$(Z^Y \times Y^X \times X \stackrel{c \times 1_X}{\to} Z^X \times X \stackrel{ev_{X, Z}}{\to} Z) = (Z^Y \times Y^X \times X \stackrel{1 \times ev_{X, Y}}{\to} Z^Y \times Y \stackrel{ev_{Y, Z}}{\to} Z)

One may show that internal composition behaves as the usual composition at the underlying set level, in that given maps $g:Y\to Z$, $f:X\to Y$, we have

$\left(1\stackrel{⟨\left[g\right],\left[f\right]⟩}{\to }{Z}^{Y}×{Y}^{X}\stackrel{{c}_{X,Y,Z}}{\to }{Z}^{X}\right)=\left[gf\right]:1\to {Z}^{X}$(1 \stackrel{\langle [g], [f] \rangle}{\to} Z^Y \times Y^X \stackrel{c_{X, Y, Z}}{\to} Z^X) = [g f]: 1 \to Z^X

## Properties

### Inheritance by reflective subcategories

In showing that a given category is cartesian closed, the following theorem is often useful (cf. A4.3.1 in the Elephant):

###### Theorem

If $C$ is cartesian closed, and $D\subseteq C$ is a reflective subcategory, then the reflector $L:C\to D$ preserves finite products if and only if $D$ is an exponential ideal (i.e. $Y\in D$ implies ${Y}^{X}\in D$ for any $X\in C$). In particular, if $L$ preserves finite products, then $D$ is cartesian closed.

### Exponentials of cartesian closed categories

The following observation was taken from a post of Mike Shulman at MathOverflow.

If $𝒞$ is small and $𝒟$ is complete and cartesian closed, then ${𝒟}^{𝒞}$ is also complete and cartesian closed. Completeness is clear since limits in ${D}^{C}$ are computed pointwise. As for cartesian closure, we can compute exponentials in essentially the same way as for presheaves, motivated by $𝒟$-enriched category theory:

${G}^{F}\left(x\right)={\int }_{y\in 𝒞}\prod _{𝒞\left(x,y\right)}G\left(y{\right)}^{F\left(y\right)}.$G^F(x) = \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} G(y)^{F(y)}.

Then we can compute

$\begin{array}{ccc}{𝒟}^{𝒞}\left(H,{G}^{F}\right)& =& {\int }_{x\in 𝒞}𝒟\left(H\left(x\right),{G}^{F}\left(x\right)\right)\\ & =& {\int }_{x\in 𝒞}𝒟\left(H\left(x\right),{\int }_{y\in 𝒞}\prod _{𝒞\left(x,y\right)}G\left(y{\right)}^{F\left(y\right)}\right)\\ & =& {\int }_{x\in 𝒞}{\int }_{y\in 𝒞}\prod _{𝒞\left(x,y\right)}𝒟\left(H\left(x\right),G\left(y{\right)}^{F\left(y\right)}\right)\\ & =& {\int }_{y\in 𝒞}𝒟\left({\int }^{x\in 𝒞}\sum _{𝒞\left(x,y\right)}H\left(x\right),G\left(y{\right)}^{F\left(y\right)}\right)\\ & =& {\int }_{y\in 𝒞}𝒟\left(H\left(y\right),G\left(y{\right)}^{F\left(y\right)}\right)\\ & =& {\int }_{y\in 𝒞}𝒟\left(H\left(y\right)×F\left(y\right),G\left(y\right)\right)\\ & =& {𝒟}^{𝒞}\left(H×F,G\right).\end{array}$\array{ \mathcal{D}^{\mathcal{C}}\left(H,G^F\right) &=& \int_{x\in \mathcal{C}} \mathcal{D}\left(H(x), G^F(x)\right)\\ &=& \int_{x\in \mathcal{C}} \mathcal{D}\left(H(x), \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} G(y)^{F(y)}\right)\\ &=& \int_{x\in \mathcal{C}} \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} \mathcal{D}\left(H(x), G(y)^{F(y)}\right)\\ &=& \int_{y\in \mathcal{C}} \mathcal{D}\left( \int^{x\in \mathcal{C}} \sum_{\mathcal{C}(x,y)} H(x), G(y)^{F(y)}\right)\\ &=& \int_{y\in \mathcal{C}} \mathcal{D}\left(H(y), G(y)^{F(y)}\right)\\ &=& \int_{y\in \mathcal{C}} \mathcal{D}\left(H(y)\times F(y), G(y)\right)\\ &=& \mathcal{D}^{\mathcal{C}}(H\times F, G). }

Here the antepenultimate step uses the co-Yoneda lemma. This appears to involve colimits in $𝒟$ as well, but the existence of these colimits is not actually an extra assumption: the co-Yoneda lemma tells us that ${\int }^{x\in 𝒞}{\sum }_{𝒞\left(x,y\right)}H\left(x\right)$ exists and is isomorphic to $H\left(y\right)$.

Similarly, the above argument can be interpreted to say that even if $𝒟$ is not complete, then the exponential ${G}^{F}$ in ${𝒟}^{𝒞}$ exists if and only if the particular limits above exist, and in that case they are isomorphic.

A more abstract argument using comonadicity and the adjoint triangle theorem, which also applies to locally cartesian closed categories, can be found in Theorem 2.12 of

• Street and Verity, The comprehensive factorization and torsors, TAC

and is reproduced in the setting of closed monoidal categories at closed monoidal category.

### Functional completeness theorem

###### Theorem 1

Let $C$ be a cartesian closed category, and $c$ an object of $C$. Then the Kleisli category of the comonad $c×-:C\to C$, denoted $C\left[c\right]$, is also a cartesian closed category.

Remark: The Kleisli category of the comonad $c×-$ on $C$ is canonically equivalent to the Kleisli category of the monad $\left(-{\right)}^{c}$ on $C$.

###### Proof of Theorem 1

Let $a$ and $b$ be objects of $C\left[c\right]$. Claim: the product $a×b$ in $C$, considered as an object of $C\left[c\right]$, is the product of $a$ and $b$ in $C\left[c\right]$, according to the following series of natural bijections:

$\begin{array}{cc}\underline{z\to a\phantom{\rule{2em}{0ex}}z\to b}& C\left[c\right]\\ \underline{c×z\to a,c×z\to b}& C\\ \underline{c×z\to a×b}& C\\ z\to a×b& C\left[c\right]\end{array}$\array{ \underline{z \to a \qquad z \to b} & C[c] \\ \underline{c \times z \to a, c \times z \to b} & C \\ \underline{c \times z \to a \times b} & C \\ z \to a \times b & C[c] }

Claim: the exponential ${a}^{b}$ in $C$, considered as an object of $C\left[c\right]$, is the exponential of $a$ and $b$ in $C\left[c\right]$, according to the following series of natural bijections:

$\begin{array}{cc}\underline{z\to {a}^{b}}& C\left[c\right]\\ \underline{c×z\to {a}^{b}}& C\\ \underline{c×z×b\to a}& C\\ z×b\to a& C\left[c\right]\end{array}$\array{ \underline{z \to a^b} & C[c] \\ \underline{c \times z \to a^b} & C \\ \underline{c \times z \times b \to a} & C \\ z \times b \to a & C[c] }

where in the last step, we used the prior claim that the product of objects in $C$, when viewed as an object of $C\left[c\right]$, gives the product in $C\left[c\right]$.

Observe that the object $c$ in $C\left[c\right]$ has an element $e:1\to c$, corresponding to the canonical isomorphism $c×1\cong c$ in $C$. We call this element the “generic element” of $c$ in $C\left[c\right]$, according to the following theorem. This theorem can be viewed as saying that in the doctrine of cartesian closed categories, $C\left[c\right]$ is the result of freely adjoining an arrow $1\to c$ to $C$.

###### Theorem (Functional completeness)

Let $C$ and $D$ be cartesian closed categories, and let $F:C\to D$ be a cartesian closed functor. Let $c$ be an object of $C$, and let $t:F\left(1\right)\to F\left(c\right)$ be an element in $D$. Then there exists an extension of $F$ to a cartesian closed functor $\stackrel{˜}{F}:C\left[c\right]\to D$ that takes the generic element $e:1\to c$ in $C\left[c\right]$ to the element $t$, and this extension is unique up to isomorphism.

###### Proof (sketch)

On objects, $\stackrel{˜}{F}\left(a\right)=F\left(a\right)$. Let $f:a\to b$ be a map of $C\left[c\right]$, i.e., let $g:c×a\to b$ be the corresponding map in $C$, and define $\stackrel{˜}{F}\left(f\right)$ to be the composite

$F\left(a\right)\cong 1×F\left(a\right)\stackrel{t×1}{\to }F\left(c\right)×F\left(a\right)\cong F\left(c×a\right)\stackrel{F\left(g\right)}{\to }F\left(b\right)$F(a) \cong 1 \times F(a) \stackrel{t \times 1}{\to} F(c) \times F(a) \cong F(c \times a) \stackrel{F(g)}{\to} F(b)

It is straightforward to check that $\stackrel{˜}{F}$ is a cartesian closed functor and is, up to isomorphism, the unique cartesian closed functor taking $e$ to $t$.

Revised on October 12, 2012 22:48:58 by Mike Shulman (192.16.204.218)