The Unapologetic Mathematician

Mathematics for the interested outsider

Internal Hom Functors

As Todd Trimble pointed out, things get really nice when a category is enriched over itself. That is, the morphisms from one object to another in \mathcal{V} themselves have the structure of an object of \mathcal{V}. This trivially the case for \mathbf{Set}, because there’s a set of functions from one set to another. We also know that in \mathbf{Ab} there’s an abelian group of homomorphisms from one abelian group to another. We say that the category has an “internal hom functor”, because the hom functor lands back inside the category itself, rather than in the category of sets.

For the moment, let’s consider a category \mathcal{V} that is not only monoidal (which is needed to have an enriched category), but also symmetric and closed. Remember that “closed” means we have an adjunction \underline{\hphantom{X}}\otimes B\dashv (\underline{\hphantom{X}})^B for each object B. In \mathbf{Set} the set A^B is the set of functions from B to A, while in \mathbf{Ab} it’s the abelian group of homomorphisms from B to A. We see that these are already the internal hom functors we’re looking for in these situations.

So in general let’s take our symmetric, monoidal, closed category \mathcal{V}, with underlying ordinary category \mathcal{V}_0. The adjunction between the monoidal structure and the exponential has a counit — an arrow A^B\otimes B\rightarrow A — which corresponds to “evaluation” in both of our sample cases. That is, it takes a function f:B\rightarrow A and an element b\in B and gives an element f(b)\in A. We can use this to build a category.

Start with the objects of \mathcal{V}_0, and define the hom-object from B to A as A^B (using the exponential functor from the closed structure). We need to find arrows A^B\otimes B^C\rightarrow A^C and \mathbf{1}\rightarrow A^A, and we’ll use the adjunction to do it. For composition, we have the arrow

(A^B\otimes B^C)\otimes C\rightarrow A^B\otimes(B^C\otimes C)\rightarrow A^B\otimes B\rightarrow A

where the first step is the associator and the other two are evaluations. This is an element of \hom_{\mathcal{V}_0}((A^B\otimes B^C)\otimes C,A), so the adjunction sends it to an element of \hom_{\mathcal{V}_0}(A^B\otimes B^C,A^C), as we require. For identities, we can just use the left-unit arrow \mathbf{1}\otimes A\rightarrow A and pull the same trick. Now properties of adjoints give us the required relations to make this a category enriched over \mathcal{V}.

And finally we can check that V(A^B)=\hom_{\mathcal{V}_0}(\mathbf{1},A^B)\cong\hom_{\mathcal{V}_0}(B,A), so the “underlying set” of A^B is actually the set of morphisms from B to A in the underlying category \mathcal{V}_0. This justifies our suspicions that the \mathcal{V}-category we just built is in fact \mathcal{V} itself, now as a category enriched over itself.

August 23, 2007 Posted by John Armstrong | Category theory | | 2 Comments