Internalizations commute

Okay, back in the saddle. We know about monoid objects and group objects, and also the slight variant of abelian group objects. These are functors (preserving some sort of product structure) from the toy categories , , and to our target category , respectively. We could also write out all the properties of (unital) rings in terms of a category — the “theory of rings” — and then use this to define “ring objects

We know, though, that a ring is a monoid object in the category of abelian groups. And the category of abelian groups is the category of abelian group objects in . That is, . And then we get monoid objects (rings) by considering .

But what is a functor from one category into the category of functors from a second category into a third? What is ? This is just a functor from the product category to ! Thus . This should look familiar — it says that (to whatever extent it’s well-defined) the category of categories is a closed category!

Now we also know that the product of two categories is “weakly symmetric” — is equivalent to . And thus the categories of functors from either one of these to a third category are equivalent — . Putting this together with the “currying” above we find that .

So let’s bring this back to internalizations. We find that and are equivalent. A monoid object in is equivalent to an abelian group object in .

And we saw evidence of this before. We’ve taken abelian groups and built free monoid objects on them, and we’ve taken monoids and built free abelian group objects on them. And the rings we get from each case are isomorphic to each other.

This whole setup generalizes. For any two algebraic structures we can describe by “theory of” categories, we can add both structures to an object of a category in either order. the processes of “internalizing” the two structures into the category commute with each other.

Now, for an exercise you can work out the naïve approach mentioned above. Write down the definition of from first principles, just like we did for monoids and groups and such. Then show that the resulting category is equivalent to .