pathterminuspages/math/aboutcontactabout me

6.Exponentation and Cartesian Closed Categories



2.Dual Category
3.Mono-, Epi- and Isomorphisms
4.Initial and Terminal Objects
5.Products and Coproducts
@6.Exponentation and Cartesian Closed Categories

We begin by studying $Set$. For two objects, $A$ and $B$, we have the set $$ B^A = \{ f : A \rightarrow B \} $$ of size $$ |B|^{|A|} $$ We can shortly reason about this. Say we have the objects given as $$ A = \{ a,b,c \} $$ and $$ B = \{ 1,2 \} $$ OK. The element $a \in A$ can map to either $1$ or $2$. For each choice $b \in A$ has the same two possible targets. Hence we have $2 \cdot 2 \cdot 2$ choices in total.

We want to charectarize $B^A$ in terms of arrows instead of elements. Now observe this special evaluation function $$ eval : (B^A \times A) \rightarrow B $$ given as $$ eval(f,a) = f(a) $$ Given $f : A \rightarrow B$ and $a \in A$ we have that $f(a) \in B$. Given some function $$ g : (C \times A) \rightarrow B $$ we have exactly one function $$ curry(g) : C \rightarrow B^A $$ Such that $$ eval \circ (curry(g),id_A) = g $$ This $curry$ function is just one that applies an argument, $c$, to a function $g$. This concept is known from functional programming languages where a function with more than one argument applies them one at a time, and then returns a new function. That is it is given by $$ curry(g)(c) = g_c $$ We can prove the above. Let $c \in C,a \in A, f : A \rightarrow B \in B^A$. Now $$ (eval \circ (curry(g),id_A ))(c,a) = eval(g_c,a) = g(c,a) $$

Definition - Exponential Object

Now. Let $\mathcal{C}$ a category with all binary products. Let $A,B$ objects of $\mathcal{C}$. An object $B^A$ is an exponential object if there is an arrow $$ eval_{AB} : (B^A \times A) \rightarrow B $$ such that for any object $C$ and arrow $g : (C \times A) \rightarrow C$ there is a unique arrow $curry(g) : C \rightarrow B^A$ such that $$ eval_{AB} \circ (curry(g) \times id_A) = g $$

If $\mathcal{C}$ has an exponential $B^A$ for every pair of objects $A$ and $B$, then $\mathcal{C}$ is said to have exponentiation.

Definition - Cartesian Closed Category (CCC)

A $\textbf{CCC}$ is a category with a terminal object, binary products and exponentiation.

CommentsGuest Name:Comment: