The “Strictification” Theorem

I want to get in another post in the current line before I head off to Portugal on Tuesday. This theorem is another heavy one to prove, so if the proof of the Coherence Theorem was overwhelming you might just want to skim this one and remember the result: Any monoidal category is monoidally equivalent to a strict monoidal category — one whose objects form an honest monoid without any “up to isomorphism” dodging about. This will justify the usual laxity with which we treat associativity and unit laws in monoidal categories, writing without regard to parentheses and such.

When we naively write down a monoidal product like this we’re treating it as a list of objects of , and we take the product of two lists just by concatenation. So let’s start by defining the collection of objects of to be the free monoid on the objects of , which is exactly this collection of lists. We’ll write a typical list as . Then we have the concatenation product and the empty list for an identity object. All the monoid rules hold “on the nose” already, so we don’t need to worry about associators and all.

We don’t have any arrows in our category yet, but let’s press on a bit first to define a map . If this has any hope of being the object function of a monoidal functor we’ll need . We also need to figure out how should deal with a monoidal product. What we’re going to do is just choose to make the result have all its parentheses on the right. We define to get (for example) .

Now we’ll go back and add arrows to in just such a way as to make into a monoidal functor. Given two lists and in I’ll define . Notice that this makes the functor fully faithful by definition, and that every object in is , so we’re well on our way to having an equivalence of categories!

What’s missing now? Well, we still don’t know quite how to take the monoidal product of arrows in , so it’s still not quite a monoidal category yet. We can use the isomorphisms of hom-sets we just set up to do this. Given and in their monoidal product is an arrow in . We define it to be the composite:

Here the middle arrow is the monoidal product of and in , and the outer two arrows are the (unique!) ways to change parentheses as needed. The uniqueness follows from the Coherence Theorem, so we have a well-defined monoidal product on .

So now is a monoidal functor. We take to be the identity , and we let be the (unique!) arrow moving all the parentheses to the right. The Coherence Theorem gives us this uniqueness, and also handles the diagrams required for a monoidal functor.

Now for the other direction we’ll just go ahead and define by setting and . We also define by noticing that , so we can just use the identity. We define similarly.

I’ll leave the cleanup to you: does satisfy coherence conditions for a monoidal functor, is the identity functor, and there is a monoidal natural isomorphism from to the identity functor on . It’s all pretty striaghtforward, though you’ll have to appeal to the Coherence Theorem a couple times like we have above.