You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Rafaël Bocquet (May 15 2020 at 17:21):Hello everyone. I am wondering if there is a standard reference for the equivalence between different statements of the coherence theorem for monoidal categories (or for other algebraic theories) (https://ncatlab.org/nlab/show/coherence+theorem+for+monoidal+categories). In particular for the fact that the statement "every diagram in a freely generated monoidal category made up of associators and unitors commutes" implies the statement "every monoidal category is monoidally equivalent to a strict monoidal category".
Rafaël Bocquet (May 15 2020 at 17:28):(I have a proof, I am mainly looking for references that I can cite)
Most of the proofs that I find instead prove the second statement directly by the means of a representation theorem.
John Baez (May 15 2020 at 19:56):I don't know all the best references here. I forget how much Mac Lane actually did.
Philip Saville (May 15 2020 at 23:02):as far as I'm aware there isn't a standard reference for this direction of the argument. (As I guess you've seen already, it's not in the usual places, eg Mac Lane's book, his Natural associativity and commutativity paper or the Mac Lane-Pare paper on coherence for bicategories, while the Kelly/Power/Joyal/Street/etc approaches deal with the representation theorem approach.)
Out of interest: what's your approach for proving the equivalence version from the 'all diagrams commute' statement? I can see how to show the free monoidal category (on, say, a set) is monoidally equivalent to a free strict monoidal category, but I can't see how to do it for an arbitrary monoidal category...
Valeria de Paiva (May 18 2020 at 17:42):Philip Saville said:
as far as I'm aware there isn't a standard reference for this direction of the argument. (As I guess you've seen already, it's not in the usual places, eg Mac Lane's book, his Natural associativity and commutativity paper or the Mac Lane-Pare paper on coherence for bicategories, while the Kelly/Power/Joyal/Street/etc approaches deal with the representation theorem approach.)
Out of interest: what's your approach for proving the equivalence version from the 'all diagrams commute' statement? I can see how to show the free monoidal category (on, say, a set) is monoidally equivalent to a free strict monoidal category, but I can't see how to do it for an arbitrary monoidal category...
well, for me the standard references for this were Mints and Soloviev, as described in Phil Scott's "Some aspects of categories in Computer Science", Handbook of Algebra, edited by M. Hazewinkel. (I've typed Mints coherence category in Google)
Rafaël Bocquet (May 20 2020 at 18:03):Philip Saville said:
Out of interest: what's your approach for proving the equivalence version from the 'all diagrams commute' statement? I can see how to show the free monoidal category (on, say, a set) is monoidally equivalent to a free strict monoidal category, but I can't see how to do it for an arbitrary monoidal category...
The fact that all diagrams commute can be used to prove that the free monoidal category generated by a set of objects, a family of morphisms and a family of equalities between morphisms is equivalent to the free strict monoidal category on the same data. It may seem weird to include equalities between morphisms in the generating data, but the idea is that monoidal categories are presented by a generalized algebraic theory with 3 sorts, for objects, morphisms and equalities between morphisms.
The proof that I know then constructs a suitable quotient of the freely generated monoidal category, using the fact that every diagram commutes to make sure that the choices of representative do not matter. This quotient is a retract of the corresponding free strict monoidal category (and is probably even isomorphic to it).
By the small object argument, every monoidal category is equivalent to some freely generated monoidal category. By combining these results, we get from any weak monoidal category , a zigzag of monoidal equivalences .
I'm not sure, but I think that in the case of monoidal categories, every monoidal category is a retract of a freely generated one. This would implies that all units of the adjunction between monoidal categories and strict monoidal categories are monoidal equivalences, not only the units for the freely generated monoidal categories.
Todd Trimble (May 20 2020 at 18:18):As I know it, the idea is to set up a monoidal equivalence between your given monoidal category and the strict monoidal category of cliques , as described here in the nLab, where is essentially discrete by Mac Lane's theorem. I think the same technique is described in Geometry of Tensor Calculus by Joyal and Street (although it might be Braided Tensor Categories).
Philip Saville (May 21 2020 at 14:22):@Rafaël Bocquet interesting, thank you!
Also, @Todd Trimble is right - Joyal & Street sketch an argument using cliques in Generalised Tensor Calculus I (thanks Todd for the pointer, I'd not seen that paper before).
It turns out there's more ways to prove this result than I had thought. To me it seems harder to go this way --- from
"all diagrams commute" to "every X is equivalent to a strict X" --- than the reverse, and I suspect the disparity grows as the structure gets richer. Are there any particular reasons (beside technical interest) for choosing this route?
Todd Trimble (May 21 2020 at 14:40):Most coherence theorems are not of the "all diagrams commute" sort, and they usually wind up giving procedures for deciding which diagrams commute in free structures. Understanding the free structures is often a necessary preamble before saying "every X is equivalent to a strictish X": it's not necessarily known in advance what strict/semistrict/strictish should mean, or whether that way of thinking about a coherence theorem is appropriate.
Rafaël Bocquet (May 21 2020 at 15:12):I'm proving the equivalence of different dependent type theories, and in that setting going through the route of representation theorems (which are a way to use the fact that some things are already known to be strict/coherent, such as the associativity of function composition) is not possible (as far as I know).
Rafaël Bocquet (May 21 2020 at 15:13):@Todd Trimble Thanks for the reference!
Philip Saville (May 21 2020 at 15:54):both good points! Having just looked at some of these proofs, I could add that you also get a more concrete description of the strictification, and so of the normal / canonical forms for that structure.
(My ulterior motive is that I have an "every X is equivalent to a stricter X" result via Yoneda and a "free X is coherent" result proven in a completely different way, and I'm wondering what new things I can get by using the latter to prove a strictification result for all Xs without going via Yoneda.)