The notions of coherence theorems and of strictification theorems are strongly related. In the case of monoidal categories, the coherence theorem states that every formal diagram in a monoidal category commutes, while the strictification theorem says that every monoidal category is monoidally equivalent to a strict monoidal category (see coherence and strictification for monoidal categories).
It is often possible to prove a strictification theorem using a coherence theorem and vice versa. The usual approach to proving both typically involves proving one directly, then proving the other from the first. Here, we shall sketch each approach, in the prototypical example of monoidal categories.
An explicit description of the free algebras for a doctrine is often helpful, if not essential, in proving a strictification theorem, since in a strict structure where constraints become equalities, many more diagrams will turn out to commute (being composed of identities). On the other hand, given a strictification theorem, if we have an explicit description of the strict structure (which is generally easier to come by), we can often deduce a characterization of the free algebras for the weak structure.
One thing to beware of is that, even for structures whose free-algebra coherence theorem is of the form “all diagrams commute”, it does not necessarily follow that all such algebras can be fully strictified.
Confusing, the terms coherence theorem and strictification theorem are often interchanged. While they are related, and many structures of interest satisfy both coherence and strictification theorems, they are distinct.
For now, see section VII.2 of Mac Lane and Mac Lane's proof of the coherence theorem for monoidal categories.
For now, see Heunen.
For now, see Theorem XI.3.2 (page 259) of Mac Lane.
For now, see Theorem XI.3.1 (page 257) of Mac Lane.
Chris Heunen, Categories and Quantum Informatics: Coherence, (2018), (url)
Created on September 25, 2024 at 10:18:18. See the history of this page for a list of all contributions to it.