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
So, I went to the library yesterday and decided to follow back some of the references in Kelly’s Basics of Enriched Category Theory (fall break woo!), specifically the actual definition of coherence by Mac Lane (it’s in a tiny pamphlet bound on one end with a big piece of clear plastic and on the other end with what looks like a small clipboard!), and the proceedings of the 1965 conference on categorical algebra in San Diego.
Unsurprisingly, the first one wasn’t all that interesting (although it was a pretty big shock to see an argument in category theory by induction on rank!), but the second one was very curious indeed, specifically the article of Eilenberg-Kelly (which is probably longer than Kelly’s whole book on the basics of enriched category theory =p). Anyhow, it seems like Kelly pretty much skips all of the proofs in the entire first chapter of his book, since giving full proofs becomes pretty insane without the coherence theorem. For example, consider proving the -bifunctor compatibility condition on two families of functors , when for all objects .
First, one has to prove that the condition is necessary, i.e. any bifunctor satisfies the compatibility condition. This takes a page and a half of large-form diagrams. However, proving the converse, i.e. the existence and uniqueness of the bifunctor restricting to the proper partial functors when the compatibility condition is satisfied is a whole new level of crazy. The first diagram literally takes up the entire page, and the second diagram is so big that the labels don’t even fit on the diagram.
Then the question:
Is there a good heuristic for producing these gigantic coherence diagrams by somehow pretending that the associativities commute strictly, then expanding it out to shuffle around the associativities? I realize that such a heuristic is actually legitimate in the case of weak-monoidal categories and bicategories by the coherence theorem, but, say, when dealing with something like tricategories, are such heuristics still effective?
I feel like we’ve been through this most of this before. But since you wound up answering your own question in the first part of your last sentence, at least for monoidal categories and bicategories, I’ll just address the very last part.
Tricategories are triequivalent to Gray monoids, which are by definition monoids in the symmetric monoidal closed category of strict 2-categories and strict 2-functors, where the monoidal structure is adjoint to the hom between 2-categories which consists of strict 2-functors, pseudonatural transformations, and modifications. The associativity constraint of Gray monoids is the identity, by definition of Gray monoids.
Edit: I said that a little bit wrong; I should have said “Gray-enriched categories” instead of “Gray monoids”. But the overall point is the same.
@Todd: I wasn’t talking about theorems. What I was trying to ask was something like, “in your experience as a category theorist, what is an effective way to do the computation when the diagrams get huge like that?” I mentioned strictifying associativities as an example of a technique I could think of offhand.
Well, your actual question was, “are such heuristics still effective”, and in the specific case of tricategories, my implicit answer was “yes”, because Gray monoids are things one can effectively calculate with. A good example might be in the theory of cartesian bicategories, where people can and do routinely act as if they are Gray monoids.
It sounds like you are working in the general area of coherence theory, which one can formalize as the study of free structured categories where the structure is governed by something like a doctrine, and particularly the problem of deciding equality of morphisms (how can we decide if a diagram commutes?). A very general technique which works in many practically arising large diagrams is to check whether the two morphisms which make up the boundary of the big diagram (you are trying to decide commutes) give rise to the same Kelly-Mac Lane graph which tracks instances of extranaturality in the diagram. (If these terms are unfamiliar to you, I can explain.) In many practical cases of interest, the answer is that the diagram indeed commutes if the graphs are the same.
In the case of the book Basic Concepts of Enriched Category Theory, basically all the big diagrams that appear come under the ambit of the theorem I have just described in rough terms. (The more precise statement, which I’ll give you even though you said you didn’t want theorems, is that a formal diagram in a free symmetric monoidal closed category generated by a category commutes provided that the two legs of the diagram yield the same KM graph, and if the domain and codomain of the diagram are each isomorphic to objects whose formal expressions can be written without the aid of the unit object; for example, if the domain is , this is isomorphic to .) In practical terms, this is the type of thing workers use.
The full coherence problem for symmetric monoidal closed categories, including the case of diagrams where mention of the unit cannot be eliminated, is more difficult, but a number of solutions exist. This was the topic of my doctoral dissertation.
If these terms are unfamiliar to you, I can explain.
I appreciate it!
I assume you’ve heard of extranatural transformations, by which I mean to include both ordinary transformations and extraordinary transformations. The original paper which introduced these formally is also by Eilenberg and Kelly,
A generalization of the functorial calculus, J. Algebra 3 366–375 (1966)
as mentioned in the nLab article. It’s still worth a read. Now, for many types of algebraic structure one can impose on categories, particularly those with a “linear” flavor in the sense of Girard’s linear logic such as monoidal categories, symmetric monoidal categories, monoidal closed categories, and also fancier notions along these lines which involve braidings instead of just symmetries, one can write down for each morphism (definable in the theory) an extranaturality (or Kelly-Mac Lane – KM) graph which is basically just an edgewise or linkwise pairing-up of atomic variable subformulas of object expressions according to instances of extranaturality. For example, in the theory of monoidal closed categories there is a formal extranatural morphism
which is ordinary-natural in the variable and extraordinary-natural in the variable , and the KM graph will have an edge linking together the two instances of , and another linking the two instances of . Formally, the KM is a partition of variable subformula instances into 2-element sets each containing two instances of the same variable, but it is nicer and more suggestive to draw this graphically. (In the article above, you will see a picture of a typical KM graph.) Extranatural transformations can frequently be composed in a well-defined way (see the Eilenberg-Kelly article for details, or you can think about lemmas 1-3 in the article above), and the composition is mirrored by gluing together the KM graphs. Well-definedness of composition is detected by whether the gluing produces no loops, and the extranaturality type of the composite (along the lines of lemmas 1-3) can be read off from the gluing.
I believe Basic Concepts of Enriched Category Theory also discusses these graphs and their utility somewhere near the beginning.
In good cases, especially for theories for which the KM graphs never produce loops when composed, the KM graphs (of formally defined morphisms) themselves form a category with the given algebraic structure type. The case of symmetric monoidal closed categories is typical in this regard. In that case, if you start with the free smc category generated by the terminal category say, there is a structure-preserving functor
and under good conditions, to decide whether a diagram in commutes, it is enough to check whether the legs of the diagram produce the same graph. The precise statement was outlined in my previous comment, and it is the main theorem of a big paper by Kelly and Mac Lane,
Coherence in Closed Categories, JPAA vol. 1 no. 1, 97-140, 1971
which is the fallback paper by which the commutativity of all those big (sometimes unmentioned) diagrams from Kelly’s book is justified. This in turn has its seeds in the wonderful realization by Lambek that cut-elimination theorems in logic can be applied toward coherence problems.
Nifty, thanks!
1 to 7 of 7