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.
Matteo Capucci (he/him) (Sep 14 2021 at 14:30):Screenshot_20210914-162720_Firefox.jpg
Matteo Capucci (he/him) (Sep 14 2021 at 14:30):I'm interested in proving coherence theorems for some structures I defined, so I'm looking at MacLane's proof for monoidal categories (zeroth question: are there other coherence theorems around?)
On the nLab, the page about such theorem starts like this:
Matteo Capucci (he/him) (Sep 14 2021 at 14:30):I'm very confused, how can having more equalities of arrows around be a problem?
Nathanael Arkor (Sep 14 2021 at 14:34):@tslil (they) recently wrote a paper explaining this example in more detail: A common misinterpretation of Isbell's obstruction to monoidal strictification.
Matteo Capucci (he/him) (Sep 14 2021 at 14:36):Also it feels like coherence theorems should be really trivial to prove, it doesn't seem to be the case.
In a sense, this is due to the fact that if your coherence laws are right, you covered all the possible 'elementary' ways to make two given datum interact.
Matteo Capucci (he/him) (Sep 14 2021 at 14:36):tslil (they) recently wrote a paper explaining this example in more detail: A common misinterpretation of Isbell's obstruction to monoidal strictification.
Uh, that seems helpful! Thanks for the reference
Matteo Capucci (he/him) (Sep 14 2021 at 14:42):Wow, that's a really cool paper! Very sharp! Indeed the argument felt smelly
Matteo Capucci (he/him) (Sep 14 2021 at 14:43):It remains open why coherence can't be stated as 'every diagram made from associators and unitors commutes'
Zhen Lin Low (Sep 14 2021 at 14:50):If you try to make that precise you will end up with a statement of the form "the free monoidal category on X is monoidally equivalent to the free strict monoidal category on X".
James Deikun (Sep 14 2021 at 16:30):Matteo Capucci (he/him) said:
I'm very confused, how can having more equalities of arrows around be a problem?
The basic idea is it's the same way you can make a disc (contractible) into a noncontractible surface by gluing two random points together.
John Baez (Sep 14 2021 at 19:08):Matteo Capucci (he/him) said:
I'm very confused, how can having more equalities of arrows around be a problem?
I don't understand. Coherence theorems often assert that two isomorphisms are equal, not that two equalities are equal. Are you trying to talk in some HoTT-inspired way where you say "equality" to mean "isomorphism"?
John Baez (Sep 14 2021 at 19:11):Also it feels like coherence theorems should be really trivial to prove.
It does? Try to use the pentagon identity and naturality of the associator in a monoidal category to prove that all isomorphisms built using the associator going from
to
are equal. Does this strike you as "really trivial"?
Jacques Carette (Sep 15 2021 at 02:06):Or try to prove Laplaza's coherence theorem for symmetric rig categories. Even stating it is quite difficult.
Matteo Capucci (he/him) (Sep 15 2021 at 11:19):Matteo Capucci (he/him) said:
I'm very confused, how can having more equalities of arrows around be a problem?
I don't understand. Coherence theorems often assert that two isomorphisms are equal, not that two equalities are equal. Are you trying to talk in some HoTT-inspired way where you say "equality" to mean "isomorphism"?
No no, I'm not doing that. I'm saying that coherence laws are axioms that impose equalities between arrows. If my mdoel happen to have other equalities around, it shouldn't invalidate the validity of the coherence laws.
Matteo Capucci (he/him) (Sep 15 2021 at 11:25):Also it feels like coherence theorems should be really trivial to prove.
It does? Try to use the pentagon identity and naturality of the associator in a monoidal category to prove that all isomorphisms built using the associator going from
to
are equal. Does this strike you as "really trivial"?
Of course they're not trivial!
What I meant is, they should be 'trivially trivial' in the sense sometimes we use in category theory: there should be a nice conceptual reason for why the coherence hold. Indeed, they 'feel' inevitable!
For example some theorems in category theory (like Yoneda) hold because of the lack of anything that could make them go wrong. Or in another sense, because your proof is basically constrained to use the 'generic structure' there is around, hence once you construct the objects you talk about, they have to be well-defined because everything else is.
It's a vague concept, I know, and potentially wrong.
James Deikun (Sep 15 2021 at 11:26):The problems that are pointed out aren't for equalities of morphisms, but for equalities of objects. Equalities of objects mean you can make new and unexpected diagrams out of the coherence morphisms, including ones that it's really unreasonable to ask that they commute.
Morgan Rogers (he/him) (Sep 15 2021 at 11:27):I'm hoping that the work @Amar Hadzihasanovic presented at CT might result in a path to the kind of intuitive results that you're imagining, though, @Matteo Capucci (he/him)
Matteo Capucci (he/him) (Sep 15 2021 at 14:33):The problems that are pointed out aren't for equalities of morphisms, but for equalities of objects. Equalities of objects mean you can make new and unexpected diagrams out of the coherence morphisms, including ones that it's really unreasonable to ask that they commute.
Wouldn't this be disallowed in a 'formal diagram', where only structure morphisms can be used (and thus not the extra equalities, seen as newly introduced morphisms 'of the category')?
Zhen Lin Low (Sep 15 2021 at 14:34):Zhen Lin Low said:
If you try to make that precise you will end up with a statement of the form "the free monoidal category on X is monoidally equivalent to the free strict monoidal category on X".
As I said...
Matteo Capucci (he/him) (Sep 15 2021 at 14:38):Indeed, I was coming back to say I realized I circled back there :sweat_smile:
Matteo Capucci (he/him) (Sep 15 2021 at 14:38):Ok now I'm enlightened
Matteo Capucci (he/him) (Sep 15 2021 at 14:38):I'm hoping that the work Amar Hadzihasanovic presented at CT might result in a path to the kind of intuitive results that you're imagining, though, Matteo Capucci (he/him)
I'd like to understand more about that!
Amar Hadzihasanovic (Sep 16 2021 at 07:33):Yes, I'm hoping that it will lead to ways in which you can take coherent “pieces” and have systematic ways of composing them together to give something coherent as well. On the other hand, when you are not able to further decompose the “pieces”, you still need to do the work of finding a coherent presentation.
Amar Hadzihasanovic (Sep 16 2021 at 07:35):It is also the case that while there can be systematic ways of finding a coherent presentation, there is an artistic component in finding “simple” ones that may not be made synthetic in this way.
Amar Hadzihasanovic (Sep 16 2021 at 07:37):For example Mac Lane first went for the “systematic” way (computing critical branchings in a rewrite system) in defining monoidal categories.
Amar Hadzihasanovic (Sep 16 2021 at 07:39):That had 5 different (parametric) equations, iirc. Then Kelly found that when the coherence cells are isomorphisms, you can derive some of the equations from others, which is why now we only have the triangle and the pentagon.
Amar Hadzihasanovic (Sep 16 2021 at 07:42):I think Kelly found this by fiddling around and there doesn't seem to be any way to systematise or generalise that part of the work (indeed, in a lax monoidal category where associators and unitors are non-invertible you do need the extra equations).