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.
Things Change
I am no longer a lecturer in Yale’s mathematics department. I am now an assistant professor in Tulane’s.