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.
Eduardo Ochs (Mar 10 2022 at 04:16):Hi all, I rewrote my paper on an extensible diagrammatic language for drawing the "missing diagrams" in CT and I would like to ask one thing here before submitting it (tomorrow!)... its abstract - below - makes a bold claim - in boldface...
Eduardo Ochs (Mar 10 2022 at 04:17):Most texts on Category Theory are written in a very terse style, in which people pretend a) that all concepts are visualizable, and b) that the readers can reconstruct the diagrams that the authors had in mind based on only the most essential cues. As an outsider I spent years believing that the techniques for drawing diagrams were part of the oral culture of the field, and that the insiders could read texts on CT reconstructing the "missing diagrams" in them line by line and paragraph by paragraph, and drawing for each page of text a page of diagrams with all the diagrams that the authors had omitted. My belief was wrong: there are lots of conventions for drawing diagrams scattered through the literature, but that unified diagrammatic language did not exist. In this chapter I will show an attempt to reconstruct that (imaginary) language for missing diagrams: we will see an extensible diagrammatic language, called DL, that follows the conventions of the diagrams in the literature of CT whenever possible and that seems to be adequate for drawing "missing diagrams" for Category Theory. Our examples include the "missing diagrams" for adjunctions, for the Yoneda Lemma, for Kan extensions, and for geometric morphisms, and how to formalize them in Agda.
Eduardo Ochs (Mar 10 2022 at 04:19):So, if anyone here feels that he/she/they know how to supply the "missing diagrams" for many categorical texts, please say "HI"...
Eduardo Ochs (Mar 10 2022 at 04:21):Here's one diagram from the paper:
sshot.png
Eduardo Ochs (Mar 10 2022 at 04:25):And here is a link to the paper itself:
http://angg.twu.net/LATEX/2022on-the-missing.pdf
Zhen Lin Low (Mar 10 2022 at 04:54):Eduardo Ochs said:
Most texts on Category Theory are written in a very terse style, in which people pretend a) that all concepts are visualizable, and b) that the readers can reconstruct the diagrams that the authors had in mind based on only the most essential cues.
I consider myself an insider but I don't myself employ such a visual mode of thinking, so I never even noticed that people (or a majority, or whatever) pretend that all concepts are visualisable. (That is not say I don't use diagrams. I do – but mainly to clarify what I mean when I have lots of anonymous arrows identified primarily by their formal domain and codomain.)
Mike Shulman (Mar 10 2022 at 05:41):If your claim is that a formalized "diagrammatic language" doesn't exist that encompasses all the sorts of diagrams that people draw, then that may be true. But I don't think that contradicts an assertion that people can read a text on category theory and translate it into diagrams.
Chad Nester (Mar 10 2022 at 06:03):You might like the book "Categories, Allegories". It open by presenting a formal language of diagrams.
Chad Nester (Mar 10 2022 at 06:05):Although it might not be exactly what you're after.
Eduardo Ochs (Mar 10 2022 at 06:52):@Chad Nester, "Cats and Alligators" and the paper that Freyd published in 1976 were some of my main influences! Take a look here: http://angg.twu.net/LATEX/2022on-the-missing.pdf#page=15
Eduardo Ochs (Mar 10 2022 at 07:10):@Mike Shulman, I've met very few people who were willing to share how they drew their diagrams, and in all of the few opportunites that I had to chat with them I asked lots of questions about what each entity in their diagrams meant and how we could translate their diagrams to other languages that were more formal. I was quite inconvenient - not on purpose - and we always reached very quickly conventions that they didn't know how to explain and things that they didn't know how to formalize... and that I didn't understand.
Eduardo Ochs (Mar 10 2022 at 07:11):I hope that this paper would encourage them to show their diagrams to me and would help me to understand their diagrams... =/
Mike Shulman (Mar 10 2022 at 07:28):I suspect you are expecting too much formality of diagrams in order to consider them "explained".
Morgan Rogers (he/him) (Mar 10 2022 at 08:03):Eduardo Ochs said:
Here's one diagram from the paper:
sshot.png
What is being clarified by the diagram here? Is the positioning meaningful?
Jules Hedges (Mar 10 2022 at 10:40):I don't exactly agree in general that the answer to things not be explained clearly is more formalisation. But formalising diagrams is still a super interesting question. Sometimes @Conor McBride talks about formalising diagrams too - in his case the goal is to communicate universal properties "in their native language" to a computer. Something he emphasises is that many diagrams have a sort of "dynamics" coming from the order of quantifiers. For example the definition of a pullback comes in 5 phases: given 2 arrows there exist 2 more arrows such that for any 2 more arrows, an arrow exists, and is equal to any other given arrow
Eduardo Ochs (Mar 10 2022 at 12:48):@Morgan Rogers (he/him), yes - the left half has the shape of an adjunction, the right half has the shape of the Yoneda Lemma (with a deleted node), and that whole diagram has exactly the same shape as the preceding one in the paper because it is a particular case of the preceding one. The list of conventions in section 2 includes several conventions on how diagrams with the same shape can be used.
Graham Manuell (Mar 10 2022 at 16:12):I wrote a paper where I tried to be very careful to include all the relevant diagrams and so on and the reviewer told me to remove them...
Graham Manuell (Mar 10 2022 at 16:15):Also kind of related: for a number of years I was under the impression that if you glued commutative diagrams together the resulting diagram would always be commutative. Of course, in reality there are certain topological obstructions to this. I haven't ever seen anyone ever discuss this in an introductory text or in a particularly comprehensive way. Though I admittedly haven't read Categories, Allegories and I think it might mention something about this. (Actually, many texts don't give any definition at all for what it means for diagram to be commutative.)
Matteo Capucci (he/him) (Mar 10 2022 at 18:31):Graham Manuell said:
Also kind of related: for a number of years I was under the impression that if you glued commutative diagrams together the resulting diagram would always be commutative. Of course, in reality there are certain topological obstructions to this.
True! That's Stokes theorem for commutative diagrams :) it only works if you around a commutative diagram. Or, in other words, if every 'irreducible' subdiagram of the glueing is commutative.
Matteo Capucci (he/him) (Mar 10 2022 at 18:32):IIRC Emily Riehl's 'Categories in context' covers the basic of diagram chasing in the first chapter, I always found that a very good choice.