Monoidal Functors and Natural Transformations

Now that we’ve got monoidal categories as the category-level analogue of monoids we need the category-level analogue of monoid homomorphisms. Recall that a monoid homomorphism is a function from the underlying set of one monoid to that of another that preserves the monoid compositions and identities. Since functors are the category-level version of functions, the natural thing to do is to ask for functors that preserves the monoidal category structure.

Of course it can’t be just that simple. As usual, we want to only ask for things to work out “up to isomorphism”. That is, given monoidal categories and — I’ll write and for both monoidal products and both identities and trust context to make clear which is which — we don’t want to insist that a functor satisfies and and so on. Instead we want natural isomorphisms to replace these equations.

So there should be an isomorphism in . As specified objects of , both and are given by functors from the category to , and an isomorphism between the objects is automatically a natural isomorphism between these functors.

There should also be a natural isomorphism . That is, for every pair of objects and of there’s an isomorphism in , and these commute with arrows and in .

And, strictly speaking, we need such a natural isomorphism for every functor built from and . For example, there should be a natural isomorphism . And, of course, all these isomorphisms should fit together well. This makes for a lot of data, and how are we going to manage it all?

The Coherence Theorem will come to our rescue! There’s a unique natural isomorphism built from s, s, and s taking (say) to in (call it ) and another unique such isomorphism in (call it ). So we can build the above isomorphism as . Now all we need is the natural isomorphisms for completely right-parenthesized products with no slots filled with identity objects.

And we can build these from the natural isomorphisms and (and make sure all the isomorphisms fit together well) — as long as these satisfy a few coherence conditions to make sure they play well with the associator and other structural isomorphisms:

Similarly to the terminology for monoidal categories, if the natural isomorphisms and are actually identities (and thus so are all the others built from them) then we call a “strict monoidal functor”. Alternatively, some prefer to call what I’ve defined above a “weak monoidal functor”.

We aren’t quite done yet, though. At the level of sets we have sets and functions between them. Up at the category level we have categories, functors, and now also natural transformations, so we should also focus on the natural transformations that preserve monoidal structures. A monoidal natural transformation between monoidal functors is a natural transformation satisfying and .

Now we have all the analogous tools for monoidal categories as we used for just plain categories to define equivalence. We say that two monoidal categories and are monoidally equivalent if there are monoidal functors and with monoidal natural isomorphisms and .

It’s useful to verify at this point that the set of isomorphism classes of objects of a monoidal category form a monoid with as its composition and (the isomorphism class of) as identity, a monoidal functor induces a homomorphism of monoids , and an equivalence between and induces an isomorphism between the monoids and . These are all pretty straightforward, and they’re good for getting used to the feel of how equalities weaken to isomorphisms as we move from sets to categories.