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.
Kevin Carlson (May 05 2025 at 04:22):A coherence theorem often says something like "every pseudo-structure is equivalent to a strict one." There is a thread of formalizing of this vague sentence via 2-monad theory that proves, in great generality (though not quite covering all accessible 2-monads on locally presentable 2-categories), that you in fact have a left 2-adjoint to the inclusion of strict algebras into pseudo-algebras, so you have an extremely natural equivalence as in the quoted sentence.
Kevin Carlson (May 05 2025 at 04:23):It's often a surprise to students meeting this material for the first time that this theorem is almost totally irrelevant to the coherence theorems that are the most interesting historically and in practice, such as Mac Lane's theorem that every monoidal category can be strictified, because pseudo-algebras for the 2-monad whose strict algebras are strict monoidal categories, i.e. the free monoid monad, involve a category with a structure map where ; thus there is an -ary multiplication for on every all of which commute with each other in nice ways. This is an unbiased monoidal category, and the content of Mac Lane's proof that "every diagram commutes" can be interpreted at least as well as saying that every monoidal category in the usual presentation is equivalent to an unbiased one as to a strict one!
Kevin Carlson (May 05 2025 at 04:23):Locally, let's call an unbiasing theorem such a theorem that every biased structure of some kind is equivalent to an unbiased one--in terms of 2-monads, that strict algebras for some finitely presented 2-monad are equivalent to pseudo-algebras for some other 2-monad, I guess. I can give textbook references for such theorems for monoidal categories, bicategories, and (pseudo) double categories, but I realized recently that I have more or less no idea about a general framework into which to fit such theorems. (I thought a bit about flexible 2-monads, but again I don't see how it helps. I suppose we ought to be able to say something to the effect that the 2-monad for monoidal categories is a flexible replacement for that for strict monoidal categories, but that still doesn't help prove that the usual presentation is correct, does it?)
Kevin Carlson (May 05 2025 at 04:23):To stop my yammering, the question is: what general framework do unbiasing theorems fit into? Do we know lots of them, or do they all require a bunch of concrete combinatorial work that doesn't readily generalize to new presentations of new 2-monads?
Mike Shulman (May 05 2025 at 05:36):I don't know of any "general unbiasing theorem" that includes all or most of the known examples. There could be general classes of them, e.g. perhaps there is an unbiasing theorem that applies to algebras over any Cat-operad, but my instinct is that there'll be combinatorial work in each case.
Morgan Rogers (he/him) (May 05 2025 at 07:24):Without having any thing meaningful to contribute on the side of references, I want to say that "unbiasing theorem" is a great name, and I would like very much for it to stick.
James Deikun (May 05 2025 at 08:40):Contrarily I think there very well could be general unbiasing theorems strong enough to be useful, since they're extremely unremarkable for 1-monads. I feel like the reason they don't seem to exist is that the mindsets for doing deep work on 2-monads and for working with finite presentations of algebras don't really cohere very easily and so the subfield is waiting for the right kind of interdisciplinary person to break it open.
Nathan Corbyn (May 05 2025 at 10:55):The core of MacLane’s theorem can be reduced to normalisation for monoids: see here. This makes me feel that general unbiasing theorems really arise from a normalisation result for the theory presenting the corresponding 2-monad combined with the general strictification result Kevin mentions. Normalisation is well known to be highly non-trivial when possible and seldom possible, which probably explains why we don’t have a general unbiasing theorem.
Nathan Corbyn (May 05 2025 at 10:55):It would be very interesting to try and make this precise
James Deikun (May 05 2025 at 12:56):I mean, normalization is also used to prove that two presentations present the same theory at the 0-level, but that doesn't prevent there from being strong metatheoretic results that every biased presentation has an (easily constructed, if large) unbiased equivalent. I think MacLane's theorem actually serves a lot of roles and it can be hard to untangle them.
Nathan Corbyn (May 05 2025 at 13:04):The role of normalisation here is to compute the chain of coherence isomorphisms. Just having an equivalent unbiased presentation is not enough to give you this.
James Deikun (May 05 2025 at 13:15):You don't have to actually compute the chain for every case to know it exists. There could definitely be other ways of knowing things like the h-level of the paths generated by a given set of generators and equations.
Nathanael Arkor (May 05 2025 at 15:42):Kevin Carlson said:
A coherence theorem often says something like "every pseudo-structure is equivalent to a strict one."
People do often call statements of this kind "coherence theorems", but I think this is inaccurate: they should be called "strictification theorems" (and indeed some authors do maintain this distinction). Then it's less clear to me whether there is a meaningful difference between coherence theorems (which give characterisations of when diagrams in free structures commute) and "unbiasing theorems" (or more simply "biasing theorems").
Nathanael Arkor (May 05 2025 at 15:43):For coherence theorems at least, Kelly's work on clubs was specifically developed for this purpose. Kelly shows how to obtain coherence theorems for several 2-algebraic structures, but as far as I know, no-one has really taken his approach much further subsequently (although he left open various questions).
Mike Shulman (May 05 2025 at 19:00):James Deikun said:
every biased presentation has an (easily constructed, if large) unbiased equivalent
I would say that the construction of a 2-monad from a presentation is the construction of an unbiased equivalent to a biased presentation. The question as I understood it was rather if, given an unbiased theory, can we construct a biased one that is "minimal" in some sense.
Kevin Carlson (May 05 2025 at 19:03):Hmm, I see what you're saying, but I'm not sure that's all I was wanting. You can construct a 2-monad from any presentation via general nonsense, but "there exists a 2-monad whose strict algebras are monoidal categories" is again not the interesting result, right? It's proving that that 2-monad is equivalent to the free monoid monad.
Kevin Carlson (May 05 2025 at 19:04):But I guess that folds roughly into the question as you formulated it, with the shift that I'm probably more interested in understanding how to check that an arbitrary proposed presentation is correct than just in constructing or verifying minimal ones.
James Deikun (May 05 2025 at 19:06):I was thinking of something similar, not finding minimal presentations which is hard even for 1-monads, but checking that two presentations generate the same 2-monad.
James Deikun (May 05 2025 at 19:08):(In this case the monoid-triangle-pentagon presentation and the "all arity products and all isomorphisms and all equations between isomorphisms" presentation.)
Mike Shulman (May 05 2025 at 19:38):Sure. Of course, checking that two presentations generate the same thing is undecidable in general.
James Deikun (May 05 2025 at 20:26):True, but people still do it a lot. It's not really considered an extreme endeavor for "typical" presentations.
Mike Shulman (May 06 2025 at 00:24):Of course, for specific presentations. But my point is that the undecidability means it'll be tricky to prove general theorems.