Functor Categories as Exponentials
The notation we used for the enriched category of functors between two enriched categories gives away the game a bit: this will be the exponential between the two categories.
First off, the arrows that we used to read off the
-component of a natural transformation turn out to fit into a more general structure. As we might hope there’s an “evaluation” functor
that takes a
-functor from
to
and evaluates it on an object of
to give an object of
. The partial functors are
and
. That this is actually a
-functor follows yet again from that litany of naturalities we keep referring to.
Now the -functor
induces an ordinary functor
. Remember here that
is a 2-category — a category enriched over ordinary categories — so each hom-object is a category, and an arrow from one hom-object to another is a functor. In particular, given a functor
we get a functor
. And then we compose with the evaluation functor to get a functor
. It turns out that this functor is an isomorphism of categories.
This means that every functor is of the above form for some unique
. Let’s look at the partial functors of
and
.
The first of these equations completely determines the functor in that
must assign to an object of
. The second uniquely determines the action of
on hom-objects because
is the counit of an end, and it comes with a universal property. Thus the above map is bijective on objects. But since it’s a functor we also need it to be bijective on morphisms — natural transformations in this case.
So, if we’ve got functors and
from
to
, with images
and
from
. Now we need to check that every
-natural
is of the form
for some unique
-natural
. But by the equation above between the second partial functors, this says that
. Thus
is the
-natural transformation
.
We now have a 2-natural isomorphism (natural isomorphism enriched over ):
. Equivalently, this means that
is 2-natural in each variable. Using this naturality it’s straightforward to show that given
and
we get a
-functor
by composing functors.
All of this fits together to say that the 2-functor has a right adjoint
when
exists for all
. At this point, the existence tends to hinge on a lot of smallness technicalities. The 2-category of all
-categories is thus “partially closed”, in a similar way to the 2-category of all ordinary categories. However, if we restrict to small
-categories we actually do have a symmetric, monoidal, closed 2-category.
In either case, partial closedness together with the Fubini theorem is enough for us to get the standard isomorphisms and
. This latter holds in the sense that either side exists if the other one does.