Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory infinity integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorYaron
    • CommentTimeJul 10th 2011

    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 nnForum, and I sincerely apologize if this is not the case).

    So, here goes:

    1. 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 DD is the denumerable set in a skeleton of Set\mathbf{Set}, then the parallel arrows 1,α:D×(D×D)(D×D)×D1, \alpha: D\times(D\times D)\to (D\times D)\times D cannot be equal).
      Is there also an example of a category in which two distinct associators turn out to be parallel yet unequal?

    2. I was very confused by the following sentences in CWM (p. 166): ”\dots while its edges vwv\to w are to be identical with certain arrows v bw bv_b\to w_b in BB. Call them the ”basic” arrows. Here, each instance α:u b(v bw b)(u bv b)w b\alpha\colon u_b\otimes(v_b \otimes w_b)\to (u_b \otimes v_b) \otimes w_b of associativity and each instance of α 1\alpha^{-1} is basic …” But if we refer to all arrows of BB 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 u b(v bw b)=u b(v bw b)u_b\otimes(v_b\otimes w_b) = u'_b\otimes(v'_b\otimes w'_b) and (u bv b)w b=(u bv b)w b(u_b\otimes v_b)\otimes w_b = (u'_b\otimes v'_b)\otimes w'_b in some particular monoidal category in which the parallel arrows α u b,v b,w b\alpha_{u_b,v_b,w_b} and α u b,v b,w b\alpha_{u'_b,v'_b,w'_b} are not equal?

    3. 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 BB), and the coherence is only for those arrows of BB 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.

    4. 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?

    5. 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?

    6. 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!


    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 11th 2011
    • (edited Jul 11th 2011)

    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 F[1]F[1]. 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 CC, by means of something called a “wreath product” of F[1]F[1] and CC.

    Anyway, the correct formal statement of Mac Lane’s theorem is that all diagrams in F[1]F[1] commute. That is, that any two morphisms which share the same domain and codomain in F[1]F[1] are equal.

    My recommendation then is that you try to read through the proof one more time as applying specifically to F[1]F[1]. If xx denotes the generating object, then objects of F[1]F[1] are formal bracketed words in xx and II such as x((xI)x)x \otimes ((x \otimes I) \otimes x). The morphisms of F[1]F[1] 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 uu, vv, ww are objects, then there is an edge labeled α uvw\alpha_{u v w} from (uv)w(u \otimes v) \otimes w to u(vw)u \otimes (v \otimes w). Similarly, there are graph edges labeled α uvw 1\alpha_{u v w}^{-1} and ρ u\rho_u, ρ u 1\rho_{u}^{-1}, λ u\lambda_u, λ u 1\lambda_{u}^{-1}. These are the “basic edges”.

    • If there is an edge labeled ff from uu to vv, then for any object ww there are edges labeled fw:uwvwf \otimes w: u \otimes w \to v \otimes w and wf:wuwvw \otimes f: w \otimes u \to w \otimes v. (These give “expanded instances” of associators, unitors, etc.).

    Any morphism in F[1]F[1] 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 \otimes to be functorial, α\alpha to be natural with inverse α 1\alpha^{-1}, 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 α\alpha that takes you from a given bracketing of nn copies of xx to the final bracketing, with all parentheses to the right. Any move along an expanded instance of α\alpha 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 \otimes, one involving naturality of α\alpha, 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 F[1]F[1], 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. (?)

    • CommentRowNumber3.
    • CommentAuthorYaron
    • CommentTimeJul 11th 2011
    • (edited Jul 11th 2011)

    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 F[1]F[1] is constructed, I only thought of it as a directed graph, with vertices the binary words and edges those arrows α u,v,w\alpha_{u,v,w} (where here α\alpha is just a symbol) β1 w\beta\otimes 1_w etc. The arrows can be interpreted in a monoidal category BB, 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 BB. Then coherence is the fact that interpreting any two parallel paths and then composing the arrows in BB results in two identical arrows in BB.

    In CWM, F[1]F[1] (which is there called WW) 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 UU, where UU is the forgetful functor fromMoncatMoncat (monoidal categories with strict monoidal functors) to SetSet (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 F[1]F[1] 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 WW 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 WW is free, and I don’t immediately see how this implies coherence (every diagram in the above graph commutes when interpreted in BB).

    Thanks again, Yaron

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 13th 2011

    I don’t immediately see how this implies coherence (every diagram in the above graph commutes when interpreted in BB)

    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?

    • CommentRowNumber5.
    • CommentAuthorYaron
    • CommentTimeJul 13th 2011

    Yes, I understand that functors preserve commutative diagrams, so obviously every commutative diagram (that is, every diagram) in WW is mapped to a commutative diagram in B (given our unique monoidal functor W–>B). This defines certain diagrams of BB that commute, but how can I verify that these diagrams are exactly those obtained from interpreting paths of the “syntactic” graph G_n in BB? (For me, the more intuitive definition of coherence is that any two paths from uu to vv in G_n, when interpreted in BB, compose to the same arrow of BB) I suppose that I should use the fact that our functor WBW\to B is monoidal (not just a functor) and induction.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 13th 2011
    • (edited Jul 13th 2011)

    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 F[1]F[1] was described in a manifestly syntactic way, and the coherence theorem identifies this monoidal category as monoidally isomorphic to Mac Lane’s WW. A (strict) monoidal functor from F[1]F[1] to BB obviously interprets paths in the syntactic graph correctly, but since the coherence theorem then identifies this with a strict monoidal functor from WW to BB, all should be well. (hm, strange problems with rendering latex here; can’t get arrows to appear)

    • CommentRowNumber7.
    • CommentAuthorYaron
    • CommentTimeJul 13th 2011

    Thanks, Todd! This is exactly the explanation I needed.