Todd Trimble
Functional completeness for cartesian closed categories

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×xb̲ 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 x \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 August 17, 2012 at 00:10:54 by Todd Trimble