What is the explicit bijection between $\text{Cat} (A \times B, C) \cong \text{Cat} (A, C^B)$?

Question

From Category Theory by Mac Lane:

For small categories $A, B, C$ establish a bijection between $\text{Cat} (A \times B, C) \cong \text{Cat} (A, C^B)$.

I'm having trouble coming up with the bijection between these two sets.

I see that it would have to be some function $f : \text{Cat} (A \times B, C) \rightarrow \text{Cat} (A, C^B)$ such that $f :(F:A \times B \rightarrow C) \rightarrow (F':A \rightarrow C^B) $ where $F$ and $F'$ are functors, but I can't figure out a way to define $f$ so that there's an appropriate inverse.

Anyone have any ideas as to how to explicitly define the bijection?

Answer 1

If $A,B,C$ are sets, you have a bijection between the sets of functions $C^{A\times B}$ and $(C^B)^A$. Given $F\colon A\times B\to C$ then you may curry the function of two variables, treating it as a function-valued function of one variable, by temporarily holding the second argument fixed. This (or a generalization of this) is also known as the hom-tensor adjunction in a category theoretic context.

Explicitly, if $F(-,-)$ is a function of two variables, I may (as almost just a matter of notation), elect to fix an $a$ value and hold it constant. I leave the second argument variable. Then $F(a,-)$ may be viewed as a function $B\to C$, which takes $b$ to the value $F(a,b)$. For each $a$ I can do this. For each $a$ I turn $F$ into a function $B\to C$. Thus I have constructed a function $A\to C^B.$ this is called currying $F$. $\text{curry}(F)(a)$ is the map that takes $b$ to $F(a,b).$

So to recap in short, $\text{curry}(F)=f(F)$ is the function taking the value on a function $F\colon A\times B\to C$ of $f(F)(a)(b)=F(a,b)$.

Then the inverse $g\colon (C^B)^A\to C^{A\times B}$ is defined, for $F'\colon A\to C^B$, as $g(F')(a,b)=F'(a)(b).$ This may be called the de-currying of $F'$.

It follows immediately that $f\colon C^{A\times B}\to (C^B)^A$ and $g\colon (C^B)^A \to C^{A\times B}$ are inverse.

For functors of categories it is the same, but the functors act on arrows as well, in the obvious way. One must also verify these maps obey the functor axioms.