Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 7 of 7
Recently, I read the proof of the coherence theorem for monoidal categories in CWM (Sec. VII.2). After a rather long struggle, I hope that I finally understand this proof (although my own summary turned out to be unbelievably long). I would very much like to verify that I did not get it completely wrong, and so I have a couple of question regarding this proof. (I hope it is appropriate to ask this in the Forum, and I sincerely apologize if this is not the case).
So, here goes:
In the beginning of Sec. VII.2 of CWM, it is emphasized that
coherence does not concern particular monoidal categories, and it is only
possible to prove that every ”formal” diagram commutes. If I
understand correctly a
hint from Tom Leinster’s course notes, one example where a ”too
general coherence” fails may be extracted from Isbell’s proof that
moving to skeleta does not guarantee that all monoidal categories are
strict (there, it is shown that if is the denumerable set in a
skeleton of , then the parallel arrows cannot be equal).
Is there also an example of a category in which two distinct
associators turn out to be parallel yet unequal?
I was very confused by the following sentences in CWM (p. 166): ”\dots while its edges are to be identical with certain arrows in . Call them the ”basic” arrows. Here, each instance of associativity and each instance of is basic …” But if we refer to all arrows of of the above kind, aren’t we getting exactly into the sort of problem described in Item 1 above? For example, isn’t is possible that and in some particular monoidal category in which the parallel arrows and are not equal?
If I understand correctly, one should define some ”syntactic” arrows inductively (together with dom and cod functions that assign to each such ”syntactic” arrow an appropriate binary word, as well as a way to interpret them in ), and the coherence is only for those arrows of that are interpretations of the syntactic arrows. Is this idea correct? I’m afraid I’ve overcomplicated matters here, but I couldn’t find a different solution.
The part of the proof concerning the reduction from the general case to the case of associators only (on p. 168) is mentioned very briefly. It seems to me that to prove both steps of this part (first assuring that all associators in a path are at the end, and then to prove coherence for the first part of the path (that now has only unitors)), requires a not so short induction if all details are written down. Am I missing something here?
Looking around, I’ve seen some helpful remarks of Todd on the web that refer to a simpler proof of Joyal and Street (which I haven’t read yet). I’ve also seen that there are some ”purely logic” proofs that should be simple (I haven’t read them either). My question is: Is it still recommended to read Mac Lane’s proof when learning coherence for the first time?
Finally, where can I find ML’s original 1963 paper? It doesn’t seem to appear anywhere on the web.
Thanks very much in advance!
Yaron
Hi Yaron –
I do think Mac Lane is a fine first source from which to read a proof of the coherence theorem. I don’t know where to find that Rice University study, where Mac Lane first published his proof, anywhere online. But in some sense that shouldn’t matter, because it turned out that there was some redundancy in his description of monoidal categories, which Max Kelly straightened out in 1964. The proof in CWM is not a bad source, except that it wimps out slightly when it comes to treating the unit, as you noted in your point 4. The overall idea of the proof is however sound.
One comment which I hope will clarify matters is that the coherence theorem is really all about the structure of the free monoidal category generated by a single object, denoted . If you have experience with building free structures of other types (e.g., free groups), the construction of a free monoidal category, in this case on one object, is similar in spirit, but maybe just slightly more involved. It’s maybe not a bad idea to work through that construction once. The free monoidal category generated by a set of objects is quite similar, and in fact there is a systematic way to build the free monoidal category generated by a category , by means of something called a “wreath product” of and .
Anyway, the correct formal statement of Mac Lane’s theorem is that all diagrams in commute. That is, that any two morphisms which share the same domain and codomain in are equal.
My recommendation then is that you try to read through the proof one more time as applying specifically to . If denotes the generating object, then objects of are formal bracketed words in and such as . The morphisms of are equivalence classes of directed paths in a certain directed graph whose vertices are the objects. The edges in this directed graph are defined by recursion:
If , , are objects, then there is an edge labeled from to . Similarly, there are graph edges labeled and , , , . These are the “basic edges”.
If there is an edge labeled from to , then for any object there are edges labeled and . (These give “expanded instances” of associators, unitors, etc.).
Any morphism in can be built up as a formal composite of these expanded instances of basic edges – the directed paths play the role of the formal composites – but we need to impose an equivalence relation on directed paths to force the evident to be functorial, to be natural with inverse , the coherence conditions to hold, and so on. Thus the morphisms are certain equivalence classes of paths.
A lot of Mac Lane’s proof makes a lot more sense when you hold this picture in mind. For example, ignoring all structure that has to do with units and unitors, as in the first part of Mac Lane’s proof, the rank that he uses to perform the induction can be equivalently described as the length of the longest path of expanded instances of that takes you from a given bracketing of copies of to the final bracketing, with all parentheses to the right. Any move along an expanded instance of will then move to an object of lesser rank.
The keystone of his proof is a “diamond lemma” which is very reminiscent of proofs of confluence used in rewriting theory. In each case, completing or filling out the diamond involves a commutative square, and the cases fall into three general patterns, one involving functoriality of , one involving naturality of , and one involving the pentagon condition.
I am rediscovering the fact that even though I understand this proof, it isn’t so easy to describe in a few words! A different way of visualizing it is to imagine that we are building a 2-dimensional CW complex. The 0-skeleton is the set of objects of , the 1-skeleton comes from the directed graph, and the 2-skeleton is obtained by adjoining 2-cells whose boundaries are the (commutative) diagrams which express basic instances of functoriality, naturality, and the coherence conditions. The coherence theorem says that this 2-dim CW complex has trivial fundamental group in each component.
Hope this helps. (?)
Hi Todd,
Thank you very much for your answer, it is most appreciated and very helpful!
I think that the formal arrows you describe are exactly some of those ”syntactic arrows” I was talking about. Because I didn’t know of what you explained about the way is constructed, I only thought of it as a directed graph, with vertices the binary words and edges those arrows (where here is just a symbol) etc. The arrows can be interpreted in a monoidal category , and the pair of functions consisting of interpreting binary words (vertices) and arrows is a morphism of graphs from the above graph to the underlying graph of . Then coherence is the fact that interpreting any two parallel paths and then composing the arrows in results in two identical arrows in .
In CWM, (which is there called ) is already built with a single element in every hom-set, and it is proved that this category is indeed the object part of a universal arrow from to , where is the forgetful functor from (monoidal categories with strict monoidal functors) to (this is the way I understand “free on one element”). I will now try to understand this using the construction in your answer: First to build F[1] as you said (hom-sets are equivalence classes etc.), and then verifying that all diagrams there commute and that we indeed have a universal arrow (i.e., that it is free). If I understand correctly, the way you described to build can be obtained by first taking the free category on the graph that I have, and then perhaps identifying some arrows.
By the way, I understand (from ML’s proof) that coherence (as described in the first paragraph here) implies that ML’s is the free monoidal category on one element. What I don’t understand is the opposite direction: In ML it is said that coherence is nothing but the statement that is free, and I don’t immediately see how this implies coherence (every diagram in the above graph commutes when interpreted in ).
Thanks again, Yaron
I don’t immediately see how this implies coherence (every diagram in the above graph commutes when interpreted in )
I’m maybe not sure what the objection is, but my immediate reaction is that we might follow Eric Forgy when he advocated the view some months ago that “a functor preserves commutative diagrams” (as the most intuitive way of saying what a functor is for people with a background similar to his). Does that speak to your concern?
Yes, I understand that functors preserve commutative diagrams, so obviously every commutative diagram (that is, every diagram) in is mapped to a commutative diagram in B (given our unique monoidal functor W–>B). This defines certain diagrams of that commute, but how can I verify that these diagrams are exactly those obtained from interpreting paths of the “syntactic” graph G_n in ? (For me, the more intuitive definition of coherence is that any two paths from to in G_n, when interpreted in , compose to the same arrow of ) I suppose that I should use the fact that our functor is monoidal (not just a functor) and induction.
Sorry – don’t take my last comment as implying you didn’t realize this; it was just a way of drawing you out further, nothing more.
I guess we’re back to the alternative viewpoint I was offering in my first comment. The was described in a manifestly syntactic way, and the coherence theorem identifies this monoidal category as monoidally isomorphic to Mac Lane’s . A (strict) monoidal functor from to obviously interprets paths in the syntactic graph correctly, but since the coherence theorem then identifies this with a strict monoidal functor from to , all should be well. (hm, strange problems with rendering latex here; can’t get arrows to appear)
Thanks, Todd! This is exactly the explanation I needed.
1 to 7 of 7