The Braided Coherence Theorem

I find myself up earlier than expected this morning, so I thought I’d bang out the proof I’d promised of the “coherence theorem” for braided monoidal categories.

Recall that we’re considering a braided monoidal category with underlying “ordinary category” — the same category, just forgetting that it’s braided and monoidal. Then the statement is that the category of braided monoidal functors from to is equivalent to .

To make our lives a bit easier, we’ll use the strictification theorem to pass from the (weak) monoidal category to a monoidally equivalent strict monoidal category , with underlying category . Now the braiding on induces (via the equivalence) one on . The new statement is that the category of strictly monoidal functors from to is isomorphic to . Then the result we really want (about ) will follow.

One direction is easy: we take a functor and evaluate it at the object to get an object . A monoidal natural transformation has, in particular, the component , which makes “evaluate at ” a functor.

For the other direction, we’ll pick an object of and use it to construct a strictly braided monoidal functor from to that sends to , and then show that an arrow in induces a natural transformation between the functors built on and . We’ll see that everything in sight is unique, so this construction actually provides an “on the nose” inverse functor to “evaluate at “.

So, we’ve got an object and we set . Then for to be monoidal we must set , since is (remember that the “tensor power” is defined just like regular exponentiation: take the tensor product of copies of the object in question). This completely defines the functor on objects.

Now any morphism in is an element of some braid group . Let’s look at simply crossing the left strand over the right in : this is , so to have a strictly braided functor we must set . In , the crossings of one strand over the one to its right generate the whole group. If we cross strand over strand we’ll call the generator . In terms of the category , we can write as , so monoidality forces us to set .

We do have to check that the relations of the braid group are satisfied. But if then we have because the monoidal product in is a functor. And we see that because this is exactly an instance of the triangle relation for the braiding on !

So once we pick the single object everything else about is uniquely determined. If we have an arrow then we must set the component of the induced natural transformation to be . Then monoidality forces to be . The construction is indeed a functor sending to the category of strictly monoidal functors from to , and it is clearly inverse to evaluation at .