The Unapologetic Mathematician

Mathematics for the interested outsider

The Internal Monoidal Product

As we’re talking about enriched categories, we’re always coming back to the monoidal category \mathcal{V}. This has an underlying category \mathcal{V}_0, which is then equipped with a monoidal product — an ordinary functor \otimes:\mathcal{V}_0\times\mathcal{V}_0\rightarrow\mathcal{V}_0. But as usual we don’t want to work with ordinary categories and functors unless we have to.

Luckily, we can turn this monoidal product into a \mathcal{V}-functor between \mathcal{V}-categories: \mathrm{Ten}:\mathcal{V}\otimes\mathcal{V}\rightarrow\mathcal{V}. Here, \mathrm{Ten} refers to “tensor product”. On objects we do the same thing as before — \mathrm{Ten}(X,Y)=X\otimes Y — because the objects of the \mathcal{V}-category \mathcal{V} are the same as those of the ordinary category \mathcal{V}_0. But now we have to consider how this functor should act on the hom-objects. So we recall that we define the internal hom-functor as \hom_\mathcal{V}(X,Y)=Y^X, using the closed structure on \mathcal{V}.

So to have a \mathcal{V}-functor we need morphisms \mathrm{Ten}:\hom_{\mathcal{V}\otimes\mathcal{V}}((X_1,Y_1),(X_2,Y_2))\rightarrow\hom_\mathcal{V}(X_1\otimes Y_1,X_2\otimes Y_2). On the left we defined the hom-object for the product \mathcal{V}-category as \hom_\mathcal{V}(X_1,X_2)\otimes\hom_\mathcal{V}(Y_1,Y_2), which is then defined as X_2^{X_1}\otimes Y_2^{Y_1}. On the right we have the exponential (X_2\otimes Y_2)^{X_1\otimes Y_1}.

But by the closure adjunction an arrow X_2^{X_1}\otimes Y_2^{Y_1}\rightarrow(X_2\otimes Y_2)^{X_1\otimes Y_1} is equivalent to an arrow (X_2^{X_1}\otimes Y_2^{Y_1})\otimes(X_1\otimes Y_1)\rightarrow(X_2\otimes Y_2). Now we can just swap around the factors on the left to get (X_2^{X_1}\otimes X_1)\otimes(Y_2^{Y_1}\otimes Y_1), and then inside each set of parentheses we can use the evaluation morphism we get from the closure adjunction, leaving us with X_2\otimes Y_2. Putting together the swap and the evaluations we get the arrow we want. And then the closure adjunction flips this to the morphism we needed to define the monoidal product on hom-objects.

The underlying ordinary functor \mathrm{Ten}_0 of the \mathcal{V}-functor \mathrm{Ten} is the old monoidal product \otimes again. On objects we already have the same action, so we need to check that the underlying function of the morphism \mathrm{Ten}:X_2^{X_1}\otimes Y_2^{Y_1}\rightarrow(X_2\otimes Y_2)^{X_1\otimes Y_1} is the same as the function \otimes:\hom_{\mathcal{V}_0}(X_1,X_2)\times\hom_{\mathcal{V}_0}(Y_1,Y_2)\rightarrow\hom_{\mathcal{V}_0}(X_1\otimes Y_1,X_2\otimes Y_2). We already know that the underlying set of B^A is \hom_{\mathcal{V}_0}(A,B) and the cartesian product of hom-sets underlies the monoidal product of hom-objects, so we at least know that the underlying source and target objects are correct.

So what’s the underlying function? We have the arrow \mathrm{Ten}:X_2^{X_1}\otimes Y_2^{Y_1}\rightarrow(X_2\otimes Y_2)^{X_1\otimes Y_1} and we need to produce a function \mathrm{Ten}_0:\hom_{\mathcal{V}_0}(\mathbf{1},X_2^{X_1})\times\hom_{\mathcal{V}_0}(\mathbf{1},Y_2^{Y_1})\rightarrow\hom_{\mathcal{V}_0}(\mathbf{1},(X_2\otimes Y_2)^{X_1\otimes Y_1}). In each of these hom-sets we can use the closure adjunction to get a function \hom_{\mathcal{V}_0}(X_1,X_2)\times\hom_{\mathcal{V}_0}(Y_1,Y_2)\rightarrow\hom_{\mathcal{V}_0}(X_1\otimes Y_1,X_2\otimes Y_2). But this is clearly function (f,g)\mapsto f\otimes g for the ordinary tensor product.

In light of this tight relationship between \mathrm{Ten} and \otimes, I’ll usually just write \otimes for each. Again, when I don’t specify whether I’m talking about the ordinary or the enriched functor I’ll default to the enriched version.


August 28, 2007 - Posted by | Category theory

No comments yet.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: