nLab coherence and strictification for symmetric monoidal categories

Idea

The coherence theorem and strictification theorem for symmetric monoidal categories may each take several forms.

Coherence theorems

1. Every diagram in a free symmetric monoidal category made up of associators and unitors and symmetries (braidings), and in which both sides have the same underlying permutation, commutes.

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

3. Every symmetric monoidal category is equivalent to an unbiased symmetric monoidal category?.

Strictification theorems

1. Every symmetric monoidal category is symmetric-monoidally equivalent to a symmetric strict monoidal category.

2. The forgetful 2-functor $SymStrMonCat \to SymMonCat$ has a strict left adjoint and the components of the unit are equivalences in $SymMonCat$.

Note that in a symmetric strict monoidal category, the associators and unitors are identities, but the symmetry is not in general.

Related pages

• coherence and strictification for monoidal categories

References

• Saunders Mac Lane. “Natural associativity and commutativity”. Rice University Studies 49, 28-46 (1963). (Rice Digital Scholarship Archive)

• Saunders Mac Lane. Categories for the Working Mathematician (Chapter 11).

• Andre Joyal and Ross Street. “Braided tensor categories”. Adv. Math 1993

• Paul Wilson, Dan Ghica, Fabio Zanasi: String Diagrams for Strictification and Coherence, Logical Methods in Computer Science (2024) [arXiv:2201.11738]

See also section 5 of

• Saunders Mac Lane, Topology and Logic; as a Source of Algebra (Retiring Presidential Address), Bulletin of the AMS 82:1, January 1976. (euclid)