nLab
coherence theorem for monoidal categories

Context

Monoidal categories

Higher category theory

higher category theory

Basic concepts

Basic theorems

Applications

Models

Morphisms

Functors

Universal constructions

Extra properties and structure

1-categorical presentations

Contents

Idea

The coherence theorem for monoidal categories, like many coherence theorems, has several forms (or, alternatively, refers to several different theorems):

  1. Every diagram in a monoidal category made up of associators and unitors which is “formal” commutes.

  2. Every diagram in a free monoidal category made up of associators and unitors commutes.

  3. The free monoidal category on some given data is equivalent to the free strict monoidal category on the same data.

  4. Every monoidal category is monoidally equivalent to a strict monoidal category.

  5. Every monoidal category is equivalent to an unbiased monoidal category?.

  6. The forgetful 2-functor MonCatStrMonCatMonCat \to StrMonCat has a strict left adjoint and the components of the unit are equivalences in MonCatMonCat.

Proofs

Discussion

(I plan to get back to this and make emendations, but for now I’ve just pasted in some discussion from the nForum – Todd.)

Most people, when they first hear about strictifications, imagine that strictifying a monoidal category is like taking a quotient, in order to identify associativities with identities. That’s actually the wrong picture, and it leads to a lot of confusion. The right picture is that a monoidal category MM can be monoidally embedded in a strict monoidal category M stM^{st}, in which associativity and unit isomorphisms of MM are assembled into what Joyal calls “contractible networks”, or cliques (aka anaobjects). The cliques that so arise are then the objects of the strictification.

So, for example, a 4-fold tensor product like (a b(b cc d))d(a^b \otimes (b^c \otimes c^d)) \otimes d is a vertex in a clique which consists of all five ways of bracketing a bb cc dda^b \otimes b^c \otimes c^d \otimes d and the groupoid of associativities between them. Or more precisely, it consists of the infinitely many such bracketings with units inserted (e.g., ((a bI)(b cc d))(Id)((a^b \otimes I) \otimes (b^c \otimes c^d)) \otimes (I \otimes d)), as objects of the groupoid generated by associativity and unit isomorphisms between them. By Mac Lane’s coherence theorem (“all diagrams commute”), there is exactly one morphism between any two vertices in the clique, meaning that the groupoid is equivalent to a terminal groupoid, and therefore contractible.

Formally, a clique in a category CC consists of a contractible groupoid GG and a functor F:GCF: G \to C. A morphism between two cliques (G,F:GC)(G, F: G \to C), (G,F:GC)(G', F': G' \to C) is a collection of morphisms F(g)F(g)F(g) \to F'(g'), where (g,g)(g, g') ranges over Ob(G)×Ob(G)Ob(G) \times Ob(G'), making all triangles in sight commute. (In fact, by contractibility, any one of the F(g)F(g)F(g) \to F'(g') uniquely determines all the rest.) To form the monoidal strictification M stM^{st}, we take as objects those cliques in the monoidal category MM which arise by application of the “all diagrams commute” formulation of Mac Lane’s coherence theorem (which specifies the structure of the free monoidal category on one generator as a disjoint sum of contractible groupoids), and the morphisms in M stM^{st} are defined to be morphisms of cliques. The precise description is laid out here, where it is indicated that the evident embedding i:MM sti: M \to M^{st} is an equivalence in MonCatMonCat.

In any case, because MM is embedded in M stM^{st}, any diagram we are trying to prove commutative in MM is physically there in M stM^{st}, but any associativities and units in the diagram get absorbed into cliques, or rather: any such associativity is one of the components F(g)F(g)F(g) \to F'(g') of, and uniquely determines, an identity morphism of cliques. Therefore any such associativity in MM is reinterpreted as an identity in M stM^{st}, and the diagram we are trying to prove commutative in MM uniquely generates a corresponding “larger” diagram of cliques in the strict monoidal category M stM^{st}. So it is enough to prove the diagram commutes when interpreted in a strict monoidal category: we can then interpret the result in M stM^{st}, and the original diagram in MM, which is embedded in the clique diagram, is then automatically commutative as well.

One may have to practice visualizing this before it all sinks in, but it’s a tremendously potent principle.

References

Revised on October 7, 2012 04:51:11 by Mike Shulman (192.16.204.218)