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.
After reading through Leinster’s “Higher Operads, Higher Categories”, and especially in understanding the definition of a contraction on a globular set, I found it helpful to think of various “coherence” theorems in category theory as asserting contractibility of some space. There might appear to be many ways to do something, but in fact there’s a “unique” way to do so, where uniqueness is interpreted in a higher categorical sense as contractibility.
However, I recently finished reading through MacLane’s “Categories for the Working Mathematician”, and I found the description of braided coherence quite interesting. In the previous framework, I was tempted to view braided monoidal categories as degenerate tricategories, which have a “contractibility” formulation of their coherence - an Eckmann-Hilton argument then produces the commuting diagrams for braided monoidal categories.
However, the approach MacLane took seemed conceptually different. The form of the coherence theorem was determining the free braided monoidal category generated by a single object, in terms of the category of braids. For a general braided monoidal category , is also braided monoidal, and so the canonical map from Braid sending the generator to the identity functor provided a description of which diagrams are expected to commute. The advantage of this approach is that the equalities in the “free” structure should correspond precisely to the equalities that are guaranteed to hold in every structure.
So now I’m wondering how to reconcile these points of view. Should I view coherence theorems as ultimately asserting contractibility of some groupoid? Or should I view them as identifying what the “free” structure given the axioms is?
Perhaps another example of this I could share is Riehl's definition of adjunctions and monads from this video.
Here, she starts by essentially describing what the "free" adjunction and "free" monad should be (the latter being essentially the augmented simplex category) - the simplicial identities then help to encode all the equalities you should expect for an arbitrary adjunction and monad. It also provides a strategy for generalising to higher categories, by taking a higher-categorical version of these free structures.
In my own experience learning category theory, I remember that monads "clicked" a little more when I viewed their rules as "there's a unique way to get to from ", and their algebras as "there's a unique way to get to from ". In light of this talk, I can see that this is a shadow of the augmented simplex category representing the "free" monad, since the generator "" is terminal. Similarly with adjunctions, where I tried to think of all possible composites I could obtain from the left and right adjoints, and what equalities were guaranteed between these, as a way of trying to see the "global" structure of their coherence.
To me this seems to point more towards the "coherence as freeness" perspective? Especially in the case of adjunctions and monads, there's an inherent "laxness/orientation" in the coherence which I'm not sure how to encode in terms of contractibility.
If you want to make the idea of coherence as contractibility precise, then you also have to talk about free structures, no? A simple example is the coherence theorem for isomorphisms. It says that in the category C freely generated by objects and an isomorphism , the mapping space is contractible. (It does not say that is contractible for every category with an isomorphism .) More precisely, is equivalent to the terminal category. Of course this is a very strong coherence theorem; in other situations one must make do with a weaker result.
Yes I was wondering about that - it seemed to me that perhaps “coherence as freeness” was the more accurate perspective, and then it’s additionally true that a lot of (but not all) free structures in higher category theory have some form of contractibility present?
In part this question was inspired by learning about classifying topoi recently, and how one use of the generic model of a geometric theory is to deduce what equations should hold in all models. To me that’s an instance of a free object providing a “coherence theorem”.
"Coherence as freeness" is a vacuous perspective. Knowing what equations a free object "should" satisfy is the same as already knowing all the laws, including coherences. The purpose of framing coherence theorems in terms of free objects is, instead, to make precise the distinction between coherences, which are laws, and the phenomena we might see in non-free objects where coherences interact with "coincidental" equalitions that hold in a particular object. For example, we can only phrase a coherence theorem in terms of a mapping space being contractible for a free object, because a non-free object may have some other morphisms intruding and making it non-contractible.
Although contractibility itself is not an essential property of coherences, there is something like contractibility that is essential. What distinguishes the operations and laws that are called coherences from those that are not is that the former are in some sense "unimportant" because they can be "contracted away". Actual contractibility is the extreme case, but we don't call something a coherence unless we at least hypothesize that the structure it lives in is equivalent, in some appropriate sense, to some algebraically and/or geometrically simpler structure. We see this in the undirected case in various strictification and semi-strictification results, and in the directed case we see normalization results such as for skew multicategories.
I think that makes sense to me, and I feel for the most part satisfied in viewing coherence as freeness. I'll try to see how far I can take this and whether I run into any issues describing coherence theorems this way.
Ruby Khondaker (she/her) said:
After reading through Leinster’s “Higher Operads, Higher Categories”, and especially in understanding the definition of a contraction on a globular set, I found it helpful to think of various “coherence” theorems in category theory as asserting contractibility of some space. There might appear to be many ways to do something, but in fact there’s a “unique” way to do so, where uniqueness is interpreted in a higher categorical sense as contractibility.
However, I recently finished reading through MacLane’s “Categories for the Working Mathematician”, and I found the description of braided coherence quite interesting. In the previous framework, I was tempted to view braided monoidal categories as degenerate tricategories, which have a “contractibility” formulation of their coherence - an Eckmann-Hilton argument then produces the commuting diagrams for braided monoidal categories.
However, the approach MacLane took seemed conceptually different. The form of the coherence theorem was determining the free braided monoidal category generated by a single object, in terms of the category of braids. For a general braided monoidal category , is also braided monoidal, and so the canonical map from Braid sending the generator to the identity functor provided a description of which diagrams are expected to commute. The advantage of this approach is that the equalities in the “free” structure should correspond precisely to the equalities that are guaranteed to hold in every structure.
So now I’m wondering how to reconcile these points of view. Should I view coherence theorems as ultimately asserting contractibility of some groupoid? Or should I view them as identifying what the “free” structure given the axioms is?
Take to be a model for a theory (in a very broad sense), so . To talk about coherence, assume at least that contains a binary operation presented as a map out of a limit.
Here is the relevant binary limit. If is a product, you can picture a magma. If is a pullback over source and target data, you can picture a magmoid (a graph with a composition, and nothing else).
Now, recall that in a presheaf category, every presheaf is a colimit of representables, and the same calculation applies more generally in locally presentable settings where is given by a limit sketch. Concretely, has the canonical presentation:
.
Here is the category of elements of . Therefore, since sends colimits in the first variable to limits, we get:
So can be seen as a limit of the values of on the "generating types" of .
If one wants to speak synthetically, one can package this limit as a representative of the underlying set of a possible type in . In that case, we can write:
Heuristically, encodes a kind of formal gluing of the generating types of . If does not already contain such a , we can always complete the theory so that it does, which is not uncommon with theories (and is close in spirit to what coherators do).
Now, to make itself into a model compatible with , you would need operations on , for instance a binary operation:
But in practice you do not want an arbitrary . You want to be compatible with the original operation (and with the source and target maps if you are thinking globularly). A convenient way to express this is to ask for a structural map in the theory:
so that the induced map relates back to in the expected way.
Interpreting this compatibility requirement globularly leads us back to the usual yoga of "pasting and contractions". Specifically, the object should arise as a gluing (pushout) of lower globes or discs describing a composite. The extra datum of a map is precisely a contraction or filler condition saying that this glued boundary admits a coherent composite landing in the basic disc . In that sense, requiring to carry a model structure for that is compatible with that of forces the theory to contain (or to be completed by) the contractible gluings of discs that witness coherence.
Maybe I should specify a little bit more what my argument above is about. In my post above, I am trying to explain why the free approach and the homotopy approach are really describing the same workflow.
In both cases, one builds formal composites from generators and then chooses axioms that act as canonical fillers identifying certain composites. The difference is mainly the language used to describe the output.
Why did I focus on ? In the post I write
The reason is that endomorphisms are a natural testing ground, and a good feedback point, for coherence axioms. As soon as you try to combine two endomorphisms pointwise, the missing axioms show up. This is also why one sees in Mac Lane's characterization. It's essentially the endpoint where pointwise constructions on endomorphisms force you to confront exactly the coherence identifications you need.
Why is the main feedback endpoint for finding axioms? The mechanism is that coherence constraints are checked pointwise. If you define a pointwise operation on endomorphisms by
then the first serious obstruction is to relate
to
using only canonical structure. Unwinding this forces you to compare
with and then with
The nontrivial step is the shuffle map
The point is not the specific formula, but the fact that trying to make pointwise operations behave forces you to isolate a small list of canonical shuffles built from associators and, in the braided case, the braiding. Those shuffles are exactly the kind of data that become axioms, or are forced by axioms, in a coherence theorem.
Why did I rewrite as a limit? The limit expression
is meant as a formal version of the pointwise intuition (previously described). A choice of compatible elements in each determines an endomorphism (as long as those choices satisfy the required compatibility conditions) and a limit is precisely the way to encode the compatible tuples of those choices. So one can think of an element of
as a coherent tuple and then the pointwise tensor operation on is supposed to give us the tuple
In that language, the shuffle is exactly what identifies two different regroupings of the same tuple components. This is also why limits keep reappearing in homotopy theory: they encode global structure as compatible local data.
How does this connect back to homotopies (or fillers) and the map ? In the post I introduced as a synthetic name for a gluing that encodes endomorphism data. The map is then the theory-level way to say that elements of the form are intrinsically part of the theory. The existence of the map is in fact suggesting a whole spectrum of new possible commutative diagrams in . When translated to elements, these commutative diagrams in provide maps like . That is the sense in which finding axioms is finding fillers.
So what's the conclusion for free versus homotopy? On the free side, one builds the free structure on generators and quotients by the axioms, and a coherence theorem identifies the resulting normal forms. On the homotopy side, one views the same generators as cells or discs, and one views axioms as fillers that attach higher cells identifying boundaries.
In the plain monoidal case, the fillers collapse rebracketing ambiguity so the coherence groupoid is contractible in the relevant sense. In the braided case, the fillers enforce braid relations but do not collapse the remaining loops, which is why braid groups survive in the free braided structure.
The role of and is that they make this filler problem appear in the simplest form, namely as pointwise shuffles of tuple components that must be identified if the induced operation on endomorphisms is to be coherent.
Thank you for the detailed explanation Rémy! It’s given me a much better understanding of the way in which the freeness and homotopy-theoretic perspectives on coherence relate to each other.