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.
Ali Caglayan (Apr 07 2024 at 14:23):I'm looking for an (oo,1)-categorical version of MacLane's coherence theorem. Now I don't actually care for the strictification aspect, but rather the ability to produce a 2-cell. Essentially I'm looking for a reference for: Suppose f and f' are morphsisms consisting of only unitors, associators, inverses and various morphsisms between objects, then there exists a 2-cell between them.
The closest thing I've found is example 1.6.19 in Lurie's Derived Algebraic Geometry II: Noncommutative algebra. But this produces an equivalence of (oo,1)-categories to one where associativity holds strictly. Whilst nice, it doesn't tell me (at least not directly) how to produce a 2-cell between arbitrary "formal" morphisms in a monoidal category.
Does anybody know if what I am asking for is even true or doable, and if so where is it written down?
Ali Caglayan (Apr 07 2024 at 14:25):My background motivation for this is that I've managed to almost prove such a statement in HoTT for wild categories (oo-cats with higher coherence omitted) however the final step of the proof seems to require that my original category is a 1-category. I'm interested to know if there is a way to generalise MacLanes coherence with an oo-categorical version which I am looking for.
Brendan Murphy (Apr 08 2024 at 00:37):I think you can take the homotopy category and apply coherence theorem there? The classes of f, f' are the same composites of unitors, associators, and inverses (I'm not sure what you have in mind for the other morphisms?) in the monoidal structure on the homotopy category and so by the coherence theorem they are equal. By defintion of the homotopy category we get that f, f' are isomorphic via a 2 cell
Brendan Murphy (Apr 08 2024 at 00:38):And maybe this explains why you have a almost working proof for wild categories? After set-truncation you should get an ordinary monoidal category and can apply the coherence theorem. This may be wrong, I don't think about HoTT much
Brendan Murphy (Apr 08 2024 at 01:00):There should be a way of thinking about this in terms of monoidal categories = algebras over the (degreewise contractible) A_oo operad but I'm not entirely sure what the formal statement would be (and passing to homotopy categories is much simpler anyways)
Ali Caglayan (Apr 10 2024 at 13:23):Brendan Murphy said:
And maybe this explains why you have a almost working proof for wild categories? After set-truncation you should get an ordinary monoidal category and can apply the coherence theorem. This may be wrong, I don't think about HoTT much
Right, after set truncation everything works. But that also means I cannot get that 2-cell out untruncated. I'm a bit confused as to why the homotopy category is sufficient to get the 2-cell outside of HoTT. I suppose that these "homotopy category captures all the important info at this level" theorems aren't very constructive and don't have a crank you can turn in order to get the 2-cell out.
Ali Caglayan (Apr 10 2024 at 13:25):So basically I'm asking is there a way to get an explicit description? I guess with the homotopy category suggestion the answer is no, but I'm wondering what else can be done.
Brendan Murphy (Apr 10 2024 at 18:06):Ah okay yeah I think I see the issue about doing this internal to HoTT. You don't just want a 2 cell but a 2 cell unique up to contractible choice (if you don't want to truncate anything). This should the case for honest monoidal (oo, 1)-categories, by the operad thing, but it seems very infinitary and thus hard to do in HoTT. Maybe some A_n-monoidal category for low n would have enough coherence to get an essentially unique 2 cell but I'm not sure if that's how it works
Brendan Murphy (Apr 10 2024 at 18:07):Yeah I don't think the last thing I said works, you'll always have some nontrivial behavior at the top level
Ali Caglayan (Apr 10 2024 at 18:08):Well actually I don't need it to be unique, just for it to exist. I'm not even sure in general if it can be unique.
Brendan Murphy (Apr 10 2024 at 18:09):I think it will be unique in general because of the coherence theorem one dimension up
Brendan Murphy (Apr 10 2024 at 18:11):So how does your attempted proof for wild categories go? Do you try to run the proof for the coherence theorem in a proof relevant way basically? I'd like to see it if you can post a github gist or smth
Ali Caglayan (Apr 10 2024 at 18:13):Specifically about the proof in question. I have a functor Nf : M -> [N, N] -> N -> M where the monoidal structure on M is translated to a monoidal structure on [N, N] where N consists of normalised words, i.e. one way associated tensor products. The issue is showing that for any two morhpisms f and f' Nf(f) and Nf(f') has a two-cell between them. In HoTT langauge a sufficient condition for this is for M to be a set. The issue is that in practice M is never a set if I want to have interesting applications.
Ali Caglayan (Apr 10 2024 at 18:13):This is the paper I used: https://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf
Ali Caglayan (Apr 10 2024 at 18:14):This paper however implicitly assumes UIP even if they claim not to use it.
Brendan Murphy (Apr 10 2024 at 18:14):Lol I had that exact paper in mind
Ali Caglayan (Apr 10 2024 at 18:15):The reason I am asking on the categories Zulip is I want to know if anything like this already exists in the literature for monoidal oo-cats. It seems like MacLane's proof should go through without needing to assume too much coherence.
Ali Caglayan (Apr 10 2024 at 18:16):I can put my proof on GitHub if you want to take a look.
Ali Caglayan (Apr 10 2024 at 18:17):https://github.com/Alizter/HoTT/blob/monoidal-coherence-demo/theories/FreeMonoidalCategory.v
Brendan Murphy (Apr 10 2024 at 18:18):I think it's not something people think much about because the coherence is usually encoded in the definition. Eg the operadic defintion says a monoidal category is an algebra over a (non symmeteic) operad with a contractible space of n-ary operations for each n, so any of the two formal composites you're talking about (lifted to be natural transformations) live in a contractible space
Ali Caglayan (Apr 10 2024 at 18:19):At some point I switched from a definition of [N, N] as a mapping space between groupoids to one as a functor category but I don't think any information is gained or lost. But it does mean I haven't finished some of the proof of the naturality between Nf and id.
Ali Caglayan (Apr 10 2024 at 18:19):If you look at the end you will see that the only real blocker is showing the functorial action of Nf is unique upto a 2-morphism.
Ali Caglayan (Apr 10 2024 at 18:20):Obviously if we knew f == f' to begin with then Nf would just have a 2-functorial action and we would be done. But that's exactly what we are trying to show.
Ali Caglayan (Apr 10 2024 at 18:20):Also ignore anything that says HSet i avoided any truncation in the proof that final mention was me experimenting a bit.
Ali Caglayan (Apr 10 2024 at 18:23):Basically this is extracting coherence of monoidal oo-cats from the coherence of the underlying monoidal bicat. Not really true, but an intuition of what I'm trying to do.
Ali Caglayan (Apr 10 2024 at 18:24):So if somebody has a machine that fills monoidal pasting diagram in an oo-category let me know. :)
Brendan Murphy (Apr 10 2024 at 18:26):Oh maybe it's worth looking at the (oo, 2)-categorical pasting theorem paper by Hackney, Ozornova, Riehl, and Rovelli? I don't know if it's applicable to your situation though
Ali Caglayan (Apr 10 2024 at 18:28):I hadn't seen that before. I'll take a look at it later.