nLab coherence theorem for monoidal categories



Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products



Internal monoids



In higher category theory

Higher category theory

higher category theory

Basic concepts

Basic theorems





Universal constructions

Extra properties and structure

1-categorical presentations



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

  1. Every “formal” diagram in a monoidal category made up of associators and unitors 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 StrMonCatMonCatStrMonCat \to MonCat has a strict left adjoint and the components of the unit are equivalences in MonCatMonCat.



(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.


See also section 5 of

See also

Last revised on February 7, 2024 at 09:38:44. See the history of this page for a list of all contributions to it.