Todd Trimble Functional completeness for cartesian closed categories

Theorem 1

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

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

Proof of Theorem 1

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

\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^b$ in $C$ , considered as an object of $C[c]$ , is the exponential of $a$ and $b$ in $C[c]$ , according to the following series of natural bijections:

\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[c]$ , gives the product in $C[c]$ .

Observe that the object $c$ in $C[c]$ has an element $e \colon 1 \to c$ , corresponding to the canonical isomorphism $c \times 1 \cong c$ in $C$ . We call this element the “generic element” of $c$ in $C[c]$ , according to the following theorem. This theorem can be viewed as saying that in the doctrine? of cartesian closed categories, $C[c]$ 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 \colon C \to D$ be a cartesian closed functor. Let $c$ be an object of $C$ , and let $t: F(1) \to F(c)$ be an element in $D$ . Then there exists an extension of $F$ to a cartesian closed functor $\tilde{F} \colon C[c] \to D$ that takes the generic element $e \colon 1 \to c$ in $C[c]$ to the element $t$ , and this extension is unique up to isomorphism.

Proof (sketch)

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

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 $\tilde{F}$ is a cartesian closed functor and is, up to isomorphism, the unique cartesian closed functor taking $e$ to $t$ .

Revised on August 17, 2012 at 00:10:54 by Todd Trimble