nLab
cartesian closed category

Context

Monoidal categories

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 [S,X][S,X] in a cartesian closed category is often called exponentiation and is denoted X SX^S.

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

F(a b)F(a) F(b),F(a^b) \to F(a)^{F(b)},

corresponding to the composite

F(a b)×F(b)F(a b×b)F(eval a,b)F(a),F(a^b) \times F(b) \cong F(a^b \times b) \stackrel{F(eval_{a, b})}{\to} F(a),

is an isomorphism.

Examples

Some basic consequences

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

There is an evaluation map ev X,Y:Y X×XYev_{X, Y}: Y^X \times X \to Y, which by definition is the map corresponding to the identity map Y XY XY^X \to Y^X under the bijection. Using the naturality, it may be shown that the bijection hom(Z,Y X)hom(Z×X,Y)\hom(Z, Y^X) \to \hom(Z \times X, Y) takes a map ϕ:ZY X\phi: Z \to Y^X to the composite

Z×Xϕ×1 XY X×Xev X,YYZ \times X \stackrel{\phi \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y

and the universal property of Y XY^X may be phrased thus: given any ψ:Z×XY\psi: Z \times X \to Y, there exists a unique map ϕ:ZY X\phi: Z \to Y^X for which ψ=ev X,Y(ϕ×1 X)\psi = ev_{X, Y} \circ (\phi \times 1_X).

Taking Z=1Z = 1 (the terminal object), maps 1Y X1 \to Y^X (or “points” of Y XY^X) are in bijection with maps Xπ 2 11×XYX \stackrel{\pi_{2}^{-1}}{\to} 1 \times X \to Y. So the “underlying set” of Y XY^X, namely hom(1,Y X)\hom(1, Y^X), is identified with the set of maps from XX to YY. Let us denote the point corresponding to f:XYf: X \to Y by [f]:1Y X[f]: 1 \to Y^X. Then, by definition,

(1×X[f]×1 XY X×Xev X,YY)=(1×Xπ 2XfY)(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 ev X,Yev_{X, Y} indeed behaves as an evaluation map at the level of underlying sets.

Lemma

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

1[f],xY X×Xev X,YY1 \stackrel{\langle [f], x \rangle}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y

is the point fx:1Yf x: 1 \to Y.

Proof

We have

1[f],xY X×Xev X,YX = 1δ 11×1[f]×xY X×Xev X,YY = 1δ 11×11×x1×X[f]×1 XY X×Xev X,YY = 1δ 11×11×x1×Xπ 2XfY = 1δ 11×1π 21xXfY = 1xXfY\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 π 2\pi_2.

Definition

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

(Z Y×Y X×Xc×1 XZ X×Xev X,ZZ)=(Z Y×Y X×X1×ev X,YZ Y×Yev Y,ZZ)(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:YZg: Y \to Z, f:XYf: X \to Y, we have

(1[g],[f]Z Y×Y Xc X,Y,ZZ X)=[gf]:1Z 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 CC is cartesian closed, and DCD\subseteq C is a reflective subcategory, then the reflector L:CDL\colon C\to D preserves finite products if and only if DD is an exponential ideal (i.e. YDY\in D implies Y XDY^X\in D for any XCX\in C). In particular, if LL preserves finite products, then DD is cartesian closed.

Exponentials of cartesian closed categories

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

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

G F(x)= y𝒞 𝒞(x,y)G(y) F(y). G^F(x) = \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} G(y)^{F(y)}.

Then we can compute

𝒟 𝒞(H,G F) = x𝒞𝒟(H(x),G F(x)) = x𝒞𝒟(H(x), y𝒞 𝒞(x,y)G(y) F(y)) = x𝒞 y𝒞 𝒞(x,y)𝒟(H(x),G(y) F(y)) = y𝒞𝒟( x𝒞 𝒞(x,y)H(x),G(y) F(y)) = y𝒞𝒟(H(y),G(y) F(y)) = y𝒞𝒟(H(y)×F(y),G(y)) = 𝒟 𝒞(H×F,G).\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 𝒟\mathcal{D} as well, but the existence of these colimits is not actually an extra assumption: the co-Yoneda lemma tells us that x𝒞 𝒞(x,y)H(x)\int^{x\in \mathcal{C}} \sum_{\mathcal{C}(x,y)} H(x) exists and is isomorphic to H(y)H(y).

Similarly, the above argument can be interpreted to say that even if 𝒟\mathcal{D} is not complete, then the exponential G FG^F in 𝒟 𝒞\mathcal{D}^{\mathcal{C}} 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 CC be a cartesian closed category, and cc an object of CC. Then the Kleisli category of the comonad c×:CCc \times - \colon C \to C, denoted C[c]C[c], is also a cartesian closed category.

Remark: The Kleisli category of the comonad c×c \times - on CC is canonically equivalent to the Kleisli category of the monad () c(-)^c on CC.

Proof of Theorem 1

Let aa and bb be objects of C[c]C[c]. Claim: the product a×ba \times b in CC, considered as an object of C[c]C[c], is the product of aa and bb in C[c]C[c], according to the following series of natural bijections:

zazb̲ C[c] c×za,c×zb̲ C c×za×b̲ C za×b C[c]\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 ba^b in CC, considered as an object of C[c]C[c], is the exponential of aa and bb in C[c]C[c], according to the following series of natural bijections:

za b̲ C[c] c×za b̲ C c×z×ba̲ C z×ba C[c]\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 CC, when viewed as an object of C[c]C[c], gives the product in C[c]C[c].

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

Theorem (Functional completeness)

Let CC and DD be cartesian closed categories, and let F:CDF \colon C \to D be a cartesian closed functor. Let cc be an object of CC, and let t:F(1)F(c)t: F(1) \to F(c) be an element in DD. Then there exists an extension of FF to a cartesian closed functor F˜:C[c]D\tilde{F} \colon C[c] \to D that takes the generic element e:1ce \colon 1 \to c in C[c]C[c] to the element tt, and this extension is unique up to isomorphism.

Proof (sketch)

On objects, F˜(a)=F(a)\tilde{F}(a) = F(a). Let f:abf \colon a \to b be a map of C[c]C[c], i.e., let g:c×abg \colon c \times a \to b be the corresponding map in CC, and define F˜(f)\tilde{F}(f) to be the composite

F(a)1×F(a)t×1F(c)×F(a)F(c×a)F(g)F(b)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 F˜\tilde{F} is a cartesian closed functor and is, up to isomorphism, the unique cartesian closed functor taking ee to tt.

Revised on March 17, 2014 04:40:31 by Anonymous Coward (77.177.93.51)