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.
Abderrahim Adrabi (Nov 28 2023 at 14:34):Hi Everyone,
What are books to start with to learn string diagrams?
Thanks
JR (Nov 28 2023 at 14:53):Abderrahim Adrabi said:
Hi Everyone,
What are books to start with to learn string diagrams?
Thanks
https://www.amazon.com/dp/1009317865/
Damiano Mazza (Nov 28 2023 at 15:00):It's not a book, but Peter Selinger's survey seems to me like a good place to start.
Abderrahim Adrabi (Nov 28 2023 at 17:17):Damiano Mazza said:
It's not a book, but Peter Selinger's survey seems to me like a good place to start.
Thank you
Ralph Sarkis (Nov 28 2023 at 17:33):It's not a book, but the Catsters videos is the place I started at.
Jean-Baptiste Vienney (Nov 28 2023 at 18:01):JR said:
Abderrahim Adrabi said:
Hi Everyone,
What are books to start with to learn string diagrams?
Thanks
I didn't know about this book! Weirldy enough they don't even talk about monoidal categories which I thought were the origin of string diagrams and the main structure they are useful for :man_shrugging:
Jean-Baptiste Vienney (Nov 28 2023 at 18:06):Like in Picturing Quantum Processes, they seem to think that talking about monoidal categories would be scary and that drawings are a good way to make people think that category theory is cool. That's not a bad idea after all. Maybe the pictures are more important than were they come from, I don't know. Except the marketing argument, they are somehow part of our physical world. But still, I like monoidal categories.
Kevin Arlin (Nov 28 2023 at 18:23):The pictures in that book don't come from monoidal categories, but from the 2-category of categories. Monoidal categories are the special case where there's only one object, or only one color of region in terms of the string diagrams.
Jean-Baptiste Vienney (Nov 28 2023 at 20:56):Okay, thanks for the explanation :)
Dylan Braithwaite (Nov 28 2023 at 22:17):It really depends what you want to learn about string diagrams for. String diagrams for Cat (the kind you see in Hinze and Marsden's book) have a different flavour to to string diagrams for monoidal categories (the sort you see in Selinger's survey paper). You can mostly divide the resources into these two categories:
String diagrams for categories and functors:
String diagrams for monoidal categories:
More specialised topics that heavily use string diagrams for monoidal categories:
Heiko Braun (Feb 29 2024 at 20:54):And they are also employed on this YouTube-channel: https://youtube.com/@MathProofsable
Joshua Meyers (Mar 19 2024 at 19:42):I know this thread is old but I'm surprised nobody have mentioned "The geometry of tensor calculus" by Joyal and Street, 1991. This is the rigorous work that goes into defining what string diagrams really are and proving that they behave as they should.
Ralph Sarkis (Mar 19 2024 at 19:53):Did someone formalize that paper in a proof assistant already?
Kevin Carlson (aka Arlin) (Mar 19 2024 at 21:28):I think it's controversial whether that paper has the right idea of what string diagrams "really are". It supposes that a string diagram is "really" a subset of the plane, whereas if you consider that a string diagram is "really" just the combinatorial connectivity data, then plausibly all this hard work about recumbent homotopies becomes unnecessary.
Ralph Sarkis (Mar 19 2024 at 21:41):Oh, I am also more used to the connectivity/hypergraph point of view, but I thought the Joyal and Street paper was the more mainstream one.
Kevin Carlson (aka Arlin) (Mar 19 2024 at 22:04):Well, all I can say is I've never seen a single later paper mention recumbent homotopies or admit that it's in the slightest concerned with the specific embedding of a string diagram in the plane.
Nathanael Arkor (Mar 19 2024 at 23:11):Plenty of people cite Joyal and Street to justify the correctness of reasoning with string diagrams, but it has always struck me as rather missing the point, since it seems far more reasonable to consider string diagrams (like pasting diagrams) as combinatorial structures rather than topological ones.
Mike Shulman (Mar 20 2024 at 02:44):Kate Ponto and I used Joyal-Street-like topological methods to justify our cylindrical string diagrams for shadows in Shadows and traces in bicategories, and David Jaz Myers did the same for string diagrams for double categories in String Diagrams For Double Categories and Equipments.
Mike Shulman (Mar 20 2024 at 02:45):Arguably this view is what the [[tangle hypothesis]] is about.
Mike Shulman (Mar 20 2024 at 03:02):I admit I haven't done much reading on other ways to justify string diagrams. But while it makes sense to me to think of a string diagram for a symmetric monoidal category as a purely combinatorial object that doesn't really even need to be embedded anywhere, it's not immediately clear to me how to use purely combinatorial data to describe something like a planar string diagram for non-symmetric monoidal categories, which is the sort of thing that Kate and I and David Jaz were concerned with. It's probably possible, but my guess would have been that the result would be further removed from what we actually write down. But maybe someone can set me straight?
John Baez (Mar 20 2024 at 04:57):I agree that the idea of string diagrams as smoothly embedded in was fundamental to a lot of advances in knot theory, and led to generalizations such as the [[tangle hypothesis]] and [[cobordism hypothesis]]. So it's certainly a powerful viewpoint in topology, nicely extending the already strong connection between homotopy theory and higher groupoids. But maybe the topological stance can be, or even should be, avoided by people who don't care about topology. I don't know.
John Baez (Mar 20 2024 at 05:02):It would be interesting to see how (or whether) the "purely combinatorial" stance works for various entries in the periodic table. Mike raised the question of monoidal categories. Then there are braided monoidal categories. And what about purely combinatorial surface diagrams for monoidal 2-categories, braided monoidal 2-categories, sylleptic monoidal 2-categories and symmetric monoidal categories?
John Baez (Mar 20 2024 at 05:10):I once thought about a purely combinatorial approach to string diagrams for symmetric monoidal categories where (summarizing roughly) you got a morphism in a symmetric monoidal category from a graph with:
and
But I quickly realized this would only work - we'd only get a well-defined morphism in a simple way from this data - if the category were not just symmetric monoidal but actually commutative monoidal, meaning a commutative monoid in Cat. This makes the associator, unitors and also the symmetry be identity morphisms.
John Baez (Mar 20 2024 at 05:13):@Jade Master and I formalized this idea in our paper Open Petri nets.
So, my point is that the "purely combinatorial" approach to string diagrams becomes really nice and easy for commutative monoidal categories. Otherwise you have to be a bit careful about the symmetry.
Amar Hadzihasanovic (Mar 20 2024 at 09:52):I have personally been very active on the combinatorics of pasting diagrams, and one could take the point of view that “string diagrams are Poincaré duals of pasting diagrams” so if one theory is combinatorialisable, then the other is.
But while this may have a core of truth, there are certainly very non-trivial aspects of the duality, in terms e.g. of topological moves or aspects that are “obvious” only on one side and not the other, and how to identify them and transport them along the duality.
On the other hand, @Christoph Dorn and Christopher Douglas have put a lot of effort into the development of [[framed combinatorial topology]], which includes as a special case a theory of “manifold diagrams” which are a higher-dimensional extension of Joyal-Street string diagrams, and yet are “fully combinatorialisable” in a precise sense, so they would definitely have a lot to say about this question.
Amar Hadzihasanovic (Mar 20 2024 at 10:00):My rough point of view on the question of “justification” is that Joyal-Street is basically never necessary to “justify” practical uses of string diagrams for computations in e.g. a symmetric monoidal category, since individual string diagrams can always be turned into (combinatorial) pasting diagrams in such a way that the usual pasting theorems for 2-categories “justify” them, and then individual steps of the computation tend to only use “topological moves” that can be easily decomposed into e.g. a small number of Reidemeister moves, which are individually sound/“justified” by the axioms of symmetric monoidal categories.
Amar Hadzihasanovic (Mar 20 2024 at 10:02):However Joyal-Street-type approaches are, of course, interesting in their own right for things like the already-cited tangle hypothesis and cobordism hypothesis, and can certainly also be useful when one is trying to make a statement about all valid string diagrams within a certain context, as opposed to justifying an individual string diagram.
Amar Hadzihasanovic (Mar 20 2024 at 10:04):The latter, I assume, was the use case for the “topological” methods in Ponto-Shulman or Myers, as mentioned above.
Dylan Braithwaite (Mar 20 2024 at 13:10):(deleted)
Mike Shulman (Mar 20 2024 at 16:55):Amar Hadzihasanovic said:
My rough point of view on the question of “justification” is that Joyal-Street is basically never necessary to “justify” practical uses of string diagrams for computations in e.g. a symmetric monoidal category, since individual string diagrams can always be turned into (combinatorial) pasting diagrams in such a way that the usual pasting theorems for 2-categories “justify” them, and then individual steps of the computation tend to only use “topological moves” that can be easily decomposed into e.g. a small number of Reidemeister moves, which are individually sound/“justified” by the axioms of symmetric monoidal categories.
This feels to me like saying that it isn't necessary to prove by induction that for all natural numbers , since for any individual natural numbers like 2 and 3 the statement can be justified by computing both sides to the same result.
Not exactly the same, but similar. Isn't the point of mathematics that we can prove general theorems about all possible situations and then just apply them, rather than checking each instance separately whenever we want to use it?
Mike Shulman (Mar 20 2024 at 16:56):Put differently: if whenever I use a string diagram I have to worry about whether all the manipulations I used can be justified in terms of the axioms of whatever kind of monoidal category I'm using, then what have I really gained from using string diagrams?
Amar Hadzihasanovic (Mar 20 2024 at 18:29):I never said that it is not "necessary" to prove results such as this. My point is slightly different. Sometimes you read statements such as "string diagrams were only put on a rigorous footing after Joyal-Street", or something to this effect. I think statements such as this can have a chilling effect on the use of string diagrams in contexts where a general result such as Joyal-Street is not available. To return your analogy, this would be like thinking that every use of the commutative property of addition of natural numbers was "not rigorous" until the first time the property was proven axiomatically using mathematical induction, which is nonsense.
Mike Shulman (Mar 20 2024 at 18:34):If someone uses the fact that 254+923 = 923+254 without having proven that addition is commutative in general, and without computing them both to 1177 to verify the equality, I would regard that as not rigorous.
Amar Hadzihasanovic (Mar 20 2024 at 18:41):The typical string-diagrammatic equation is more akin to 2+3 = 3+2 than to 254+923 = 923+254...
Mike Shulman (Mar 20 2024 at 18:42):And if a notation is being used widely but has not been formally justified, I would say the solution is to formally justify it, not tell people that it's not necessary to justify it.
John Baez (Mar 20 2024 at 18:42):I wouldn't be surprised if some early axioms for natural numbers postulated commutativity of addition instead of proving it by mathematical induction. That would still be rigorous, just not quite as good.
Even if you wanted to, it's actually a lot harder to frame a precise axiom saying "string diagrams work in cases where they should work".
Mike Shulman (Mar 20 2024 at 18:44):Personal note: in Duality and traces for indexed monoidal categories Kate and I used a string diagram calculus that we did not justify. About this we wrote
A proper proof of validity for these string diagrams would make this precise, but we do not have space to give such a proof here. Thus, properly speaking our string diagrams are only an informal guide to the necessary calculations.
John Baez (Mar 20 2024 at 18:48):Many branches of engineering and science have their own diagrams, which are extremely important but rarely made rigorous. I've been going around turning some of them into rigorous math. I hadn't expected it when I started, but one of the main advantages of doing this is that it lets people do interesting things with the them using software. For string diagrams we see this happening in homotopy.io and other systems.
Amar Hadzihasanovic (Mar 20 2024 at 18:48):Just if it needs to be clarified again, I am nowhere making a claim as strong as “Joyal-Street is not necessary” :) of course it's better to have it than not to have it!
I feel like I'm making quite an uncontroversial point, which perhaps is receiving a controversial reading, which is not the one that I intended.
Perhaps this is a better way of phrasing it: it is perfectly fine to use special instances of a conjecture that we are able to justify as being individually true, even if the conjecture has not been proven in general.
Mike Shulman (Mar 20 2024 at 18:53):I always tell my students that rigor is not a binary quality but a sliding scale, and the proper level of rigor depends on the audience you are writing for. I agree that in many or most cases arising in practice, an audience who is familiar with the relevant sort of monoidal category and string diagram can be trusted to "compile them out" in their head. That's less true for students and newcomers to the field, of course, which is one reason for making things precise. Implementing them in a computer is another, as is catching possible mistakes.
Mike Shulman (Mar 20 2024 at 18:55):Amar, would you agree with the comments made by Kevin and Nathanael earlier in this thread, which are the ones I was initially responding to?
Mike Shulman (Mar 20 2024 at 18:57):John Baez said:
I once thought about a purely combinatorial approach to string diagrams for symmetric monoidal categories where (summarizing roughly) you got a morphism in a symmetric monoidal category from a graph with:
- all the edges labeled by objects
- specified "input" vertices with just one edge going out,
- specified "output" vertices with just one edge going in,
and
- each other vertex labeled by a morphism from the tensor product of the objects labeling its incoming edges to the tensor product of the objects labeling its outgoing edges.
But I quickly realized this would only work - we'd only get a well-defined morphism in a simple way from this data - if the category were not just symmetric monoidal but actually commutative monoidal
I don't understand this. It seems to me that as long as you also specify an ordering of the input vertices and of the output vertices, and likewise for the incoming and outgoing edges of every other vertex, you ought to get a well-defined morphism in any symmetric monoidal category by just inserting symmetries in the necessary places. As long as the category is symmetric and not just braided, once the orderings are specified there should be a unique symmetry to put in each place. Am I missing something?
Amar Hadzihasanovic (Mar 20 2024 at 18:58):On the other hand, I think there is also a certain social bias about what is deemed to “need justification” in mathematical practice.
For example, Joyal-Street is, to the letter, a statement that morphisms in certain monoidal categories are in bijection with isomorphism classes of certain continuous functions (etc etc). This is informally read as justification that certain squiggles drawn on paper are “rigorous”, because the squiggles are perceived as being “closer” to the latter mathematical objects than the former. Yet I bet for any human it is easier to translate the squiggles into algebraic expressions to be evaluated in a monoidal category, than to translate them into some expression for a continuous function with codomain the real plane...
Mike Shulman (Mar 20 2024 at 19:00):I don't think it's unreasonable to rely more on our intuition for continuity than on our intuition for monoidal categories, since most of us have decades of experience with continuity of objects in the real world but only an abstract understanding of monoidal categories.
John Baez (Mar 20 2024 at 19:02):Mike Shulman said:
It seems to me that as long as you also specify an ordering of the input vertices and of the output vertices,
That's exactly what I was not doing!
Mike Shulman (Mar 20 2024 at 19:03):Hmm, ok now I see that you said at the end that "Otherwise you have to be a bit careful about the symmetry."
Amar Hadzihasanovic (Mar 20 2024 at 19:04):Mike Shulman said:
Amar, would you agree with the comments made by Kevin and Nathanael earlier in this thread, which are the ones I was initially responding to?
As I tried to say in my first reply, I do not quite agree with the statement that diagrams are “more” combinatorial than topological, or something to that effect. I do think that they are “both” topological and combinatorial, and that this is one of those dualities where each side is enlightening in its own way.
Mike Shulman (Mar 20 2024 at 19:05):I still haven't seen any purely combinatorial definition of string diagrams in a non-symmetric monoidal category.
Mike Shulman (Mar 20 2024 at 19:07):Were you saying that the Dorn-Douglas approach realizes this? I thought they were working with topological objects equipped with additional framing/stratification structure.
Amar Hadzihasanovic (Mar 20 2024 at 19:10):Well, I can formally justify every string diagram in https://arxiv.org/abs/2101.10361 as representing a morphism from a certain combinatorial diagram shape into the nerve of a 2-category or a Gray-category (they are different nerves). But these string diagrams have non-trivial “weak units” that need to be managed so it may not meet all your requirements.
Mike Shulman (Mar 20 2024 at 19:11):I mean, can you define in general what a string diagram is, and what its meaning in such a category is?
Amar Hadzihasanovic (Mar 20 2024 at 19:13):Yes, the theory of diagrammatic sets that I have been developing has been (among other things) about giving a combinatorial, general definition of diagrams in weak higher categories in arbitrary dimension.
Mike Shulman (Mar 20 2024 at 19:15):Can you specialize that to give an explicit combinatorial description of string diagrams for non-symmetric monoidal 1-categories?
Amar Hadzihasanovic (Mar 20 2024 at 19:15):I think of these mainly as pasting diagrams but one can dualise (and I often do). But on the “string/manifold”-diagrammatic level I think that one may also want some additional “trivialisation of units” with “units becoming 'empty space'”, which this approach does not meet (somewhat “by construction”).
Amar Hadzihasanovic (Mar 20 2024 at 19:17):Mike Shulman said:
Can you specialize that to give an explicit combinatorial description of string diagrams for non-symmetric monoidal 1-categories?
Yes, again with the “weak units” caveat.
Mike Shulman (Mar 20 2024 at 19:22):Have you written it out somewhere?
Reid Barton (Mar 20 2024 at 20:01):related prior discussion: https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-questions/topic/Rigorous.20string.20diagrams/near/203538376
Amar Hadzihasanovic (Mar 20 2024 at 20:32):Mike Shulman said:
Have you written it out somewhere?
Well, in the paper I linked above,
Some of the combinatorial background in the paper is a bit outdated re: my current understanding of things. Next month I'll put a book-length exposition of related matters on the arxiv, then hopefully at some point I'll revisit this paper.
Nathanael Arkor (Mar 20 2024 at 21:29):The intuition given when introducing string diagrams is typically along the lines of "string diagrams are the Poincaré dual of pasting diagrams". It seems to me that it is usually reasonable to take this as a definition of the notion of string diagram: then the validity of operations in string diagrams follows from their validity in pasting diagrams, with the advantage that the string diagrammatic calculus makes certain operations more visually intuitive.
Nathanael Arkor (Mar 20 2024 at 21:33):If I recall correctly, when I spoke to @David Jaz at CT, he said that if he were to write his paper on string diagrams for double categories today, he would present them from an operadic rather than topological perspective. Perhaps he can comment on his perspective.
Christoph Dorn (Mar 21 2024 at 06:12):Amar Hadzihasanovic said:
On the other hand, Christoph Dorn and Christopher Douglas have put a lot of effort into the development of [[framed combinatorial topology]], which includes as a special case a theory of “manifold diagrams” which are a higher-dimensional extension of Joyal-Street string diagrams, and yet are “fully combinatorialisable” in a precise sense, so they would definitely have a lot to say about this question.
Thanks for the mention Amar! The framework of framed combinatorial topology, in particular notions of framed maps and stratified bundles, certainly makes definitions of manifold diagrams very simple. It also makes the Poincare duality with cellular diagrams straight-forward, see section 2.4 here. However, the relation to practical definitions of higher categories is still conjectural. @Lukas Heidemann is working on finally elucidating this relation, so hopefully we will have "more rigor" soon (:
Christoph Dorn (Mar 21 2024 at 06:14):Mike Shulman said:
Were you saying that the Dorn-Douglas approach realizes this? I thought they were working with topological objects equipped with additional framing/stratification structure.
As Amar mentions, the approach also yields a purely combinatorial perspective on manifold diagrams. Here's a super short exposition of the relevant definitions (sections 3 and B)
Malin Altenmüller (Mar 21 2024 at 11:44):Mike Shulman said:
Hmm, ok now I see that you said at the end that "Otherwise you have to be a bit careful about the symmetry."
Hi all, basically my PhD project is thinking about what "being a bit careful about the symmetry" means. Some of it is published here: it contains a fairly concrete definition of graphs embedded on surfaces. The idea is that if you define string diagrams (for SMC) as a specific kind of graph, then string diagrams for non-symmetric MC are a specific kind of graph embedding.
(I'm also working on a library for graph embeddings in Agda with the aim to implement diagrammatic reasoning for these kind of string diagrams.)
Mike Shulman (Mar 21 2024 at 15:46):Thanks for all the references! I'll believe you now that it's possible to give a purely combinatorial description of string diagrams. I was hoping that someone had written out explicitly what these descriptions give in the case of ordinary monoidal categories without making the reader do the specialization to in their head, and I didn't see that in my cursory perusal of the references, but it's possible that I missed it.
John Baez (Mar 21 2024 at 15:49):It would definitely be nice to see the case of good old monoidal categories spelled out. I'm suspecting that each vertex needs to be equipped with a cyclic ordering of the strings going into (or out of) it - topologists know well that graphs on oriented surfaces naturally come with this data - but this data by itself not enough to force the surface to be genus zero.
Mike Shulman (Mar 21 2024 at 15:50):I have to say that personally, talking about continuous embeddings of a topological graph in a plane is still more intuitive, and feels more closely connected to the pictures we draw, than any of these combinatorial gadgets. The combinatorial gadgets feel like an equivalent characterization of the diagrams rather than an actual description of them. When I draw a string diagram on a sheet of paper, I'm not thinking about (for instance) the cyclic ordering of the edges around each vertex, and I'm certainly not thinking about whatever consistency condition on these orderings is necessary to ensure that they actually do describe an embedding in a plane; I just directly draw an embedding in a plane.
John Baez (Mar 21 2024 at 15:51):That's how I feel too, but it's interesting that Amar spoke of the difficulty of translating your drawing into a formula for the embedding.
John Baez (Mar 21 2024 at 15:52):Of course you could fight back by arguing that the formula is yet another attempt to syntactically encode what's really a geometrical object.
Mike Shulman (Mar 21 2024 at 15:52):I like that.
Mike Shulman (Mar 21 2024 at 17:07):Another way to say the way I feel is: the work has to go somewhere. If the definition of a string diagram isn't topological, then somewhere, someone has to explain how we get from the actual pictures we draw to whatever that definition is.
Mike Shulman (Mar 21 2024 at 17:08):As I said when talking about different notions of theory:
It often seems to me that people (especially category theorists) have a tendency to say that because As can all be interpreted as Bs in some way, there is no need for the notion of A. But if we didn’t have the notion of A, then we wouldn’t be able to talk about how all As are interpreted as Bs! And if even if we only care about Bs in the end, if As occur in nature, then surely that only makes the process by which As are interpreted as Bs more important, since we have to perform it on any A we encounter in order to make it into the B we really care about.
Amar Hadzihasanovic (Mar 21 2024 at 18:19):Well, the string diagrams in rewalt are algorithmically generated from data structures that encode the "combinatorial diagrams" from my reference, so that exhibits quite a concrete connection between the combinatorics and the geometry :)
Mike Shulman (Mar 21 2024 at 19:13):That's good for one direction, but the more nontrivial one is starting with the geometry and generating the combinatorics, which is what Joyal-Street is about.
Nathanael Arkor (Mar 21 2024 at 20:28):Mike Shulman said:
Another way to say the way I feel is: the work has to go somewhere. If the definition of a string diagram isn't topological, then somewhere, someone has to explain how we get from the actual pictures we draw to whatever that definition is.
This feels to me similar to the relationship between concrete syntax, in terms of strings of symbols, and abstract syntax, in terms of structured trees. To give the complete picture, one really wants a precise treatment of both. However, I think it is really the abstract syntax that is the object of interest, and the concrete syntax is more of an implementation detail. With respect to string diagrams, the combinatorial description is like the abstract syntax, and the graphical depiction like the concrete syntax.
Mike Shulman (Mar 22 2024 at 04:30):I see the point, but I don't entirely agree, because of the point I made above about how I think. I would argue that when I read ordinary linear syntax like , I effectively parse it mentally into what is essentially equivalent to an abstract syntax tree. I think about parentheses as grouping, I understand order of operations, etc. But when I look at a string diagram, I don't mentally think about cyclic orderings on the edges adjacent to each vertex or any of the other data that's necessary to make the combinatorial description precise: I think about it as a topological object.
Nathanael Arkor (Mar 22 2024 at 05:57):I suppose it depends on the kind of string diagrams you consider, but for string diagrams for monoidal categories/2-categories, it's not necessary to consider any cyclic order on the edges: one has a list of inputs at the top, and a list of outputs at the bottom. (And similarly for double categories.) So one can read it just as one would a pasting diagram.
Mike Shulman (Mar 22 2024 at 06:08):But a formal combinatorial definition of a string diagram requires some information such as cyclic orderings in order to ensure that the diagram is "planar".
Amar Hadzihasanovic (Mar 22 2024 at 07:10):I can't say for every combinatorial definition, but the one I've been using is an “oriented incidence poset” which also records the relation between 1-cells and 0-cells i.e. the bounded regions in the string diagram -- so essentially the combinatorial data contains the information “this edge bounds this planar region from the left and this planar region from the right” -- which I think is not so far from the information that we are processing when looking at the pictures, i.e. we are looking at the nodes in relation to the incident edges, and the edges in relation to the surrounding regions of the plane.
Amar Hadzihasanovic (Mar 22 2024 at 07:14):In any case, I think “cyclic orderings” are, already in the name, a case of a combinatorial notion which appeals to our geometric intuition for an easier understanding: it's asking us to picture the ordering as placing elements on a circle.
Mike Shulman (Mar 22 2024 at 07:17):When I look at a planar string diagram in a monoidal category (as opposed to a bicategory or double category), I don't think about the regions into which the strings divide the plane at all.
Mike Shulman (Mar 22 2024 at 07:18):But I am also sensing that this conversation is passing (perhaps has already passed) the point of usefulness...
Amar Hadzihasanovic (Mar 22 2024 at 07:19):So I think it's a case of lines being blurred in general, I don't think one can separate the combinatorial from the topological side, nor it is right to treat one as the “real” thing -- so I don't particularly agree with the abstract vs concrete syntax perspective, either
Amar Hadzihasanovic (Mar 22 2024 at 07:21):Mike Shulman said:
When I look at a planar string diagram in a monoidal category (as opposed to a bicategory or double category), I don't think about the regions into which the strings divide the plane at all.
I think you are when making a judgment of “planarity”, but yes, probably pointless to argue about what is in somebody else's mind :)
Amar Hadzihasanovic (Mar 22 2024 at 07:23):When you think “I am drawing an embedding into the plane”, what you are doing is “making sure than my lines don't cross into a different bounded region of the plane”.
Amar Hadzihasanovic (Mar 22 2024 at 07:24):I.e. you are thinking of the edges as “boundaries” and not just topological intervals or something
Mike Shulman (Mar 22 2024 at 07:27):I would say I'm just "making sure that my lines don't cross" period.
Nathanael Arkor (Mar 22 2024 at 08:47):The way I'm thinking about string diagrams is by taking the dual, and encoding the data of the corresponding pasting diagram, for which no cyclic ordering is necessary. But probably this is sufficiently vague that it's not a satisfying response. I do think it would be helpful to write out a precise definition of string diagram in this manner. One more thing to add to the list...
Oscar Cunningham (Mar 22 2024 at 13:19):A diagram drawn on some paper has nothing to do with 'string diagrams' defined either combinatorially or by using the real numbers topologically, except as far as mathematicians think that those definitions are a good model for what is drawn on the paper. We have a good intuition that the real numbers correctly model the physical space that we imagine when we look at the diagram on the paper. So we therefore think that we can prove something about the paper diagrams by reducing the combinatorial definitions to the definitions via real numbers.
But I think that most mathematicians have spent a lot of time getting used to the real numbers, and convincing ourselves that they are a good model for physical space. If we spent equally long getting used to the combinatorial definitions of string diagrams we would probably also be convinced that they gave a good model of physical space. And then we wouldn't see any need to 'prove' that string diagrams work by reference to the real numbers.
John Baez (Mar 22 2024 at 17:37):Nathanael Arkor said:
I suppose it depends on the kind of string diagrams you consider, but for string diagrams for monoidal categories/2-categories, it's not necessary to consider any cyclic order on the edges: one has a list of inputs at the top, and a list of outputs at the bottom.
For me string diagrams for monoidal categories are most useful for monoidal categories where each object has a left and a right dual. The reason is that then these diagrams have a meaning that is diffeomorphism invariant. That is, you can apply any diffeomorphism of the rectangle the diagram is drawn on, and as long as it's the identity on the boundary, the meaning of the diagram is preserved! (We can weaken that "identity on the boundary" condition, too, but never mind.)
For this kind of string diagram, while the whole diagram has a well-defined top and bottom, the vertices inside do not. More precisely, the concept of a string coming into the vertex "at the top" or "at the bottom" is not invariant under the diffeomorphisms mentioned. But there's still a well-defined cyclic ordering of the edges incident to each vertex.
This is pretty standard knowledge among topologists who use string diagrams. There's a nice theory of graphs where for each vertex there's a cyclic ordering of the edges incident to that vertex. They are called 'fat graphs' or 'ribbon graphs'. (The Wikipedia article gives a topological definition, but there are also combinatorial definitions.)
Mike Shulman (Mar 22 2024 at 18:33):@Oscar Cunningham Perhaps. I'll believe it when I see it.
Aaron David Fairbanks (Mar 23 2024 at 21:35):It's not too hard to explain what planar string diagrams are in plain language. Once you understand them, it's unambiguous what manipulations are allowed. At least in that sense, a calculus of string diagrams can be used as a foundation in its own right. (Just like a foundational logical system is described in plain language rather than formalized in terms of anything else.)
In general this is how it goes for any kind of calculus you are using as a foundation: if you want, you can formalize it within some other meta framework designed to describe things like it. (You have to do this if you want to prove anything about it or formally make connections to other math.) Joyal and Street formalized string diagrams in our existing framework for topology. Combinatorial formalizations seem simpler to me, so I personally would like to see them more. I think I am agreeing with you @Oscar Cunningham.
Nathaniel Virgo (Mar 24 2024 at 09:16):One additional thing for this discussion: I often use topological intuitions about string diagrams (i.e. intuitions about lines on a page) not just as a formal tool for reasoning about existing structures but as a guide to intuition about what a good definition should look like. Because of this, I often wonder whether the relationship between the algebraic/combinatorial picture and the topological one is deeper than just one being a convenient syntax for the other.
Surely there must be some underlying reason why the good algebraic definitions are so often the ones that let you draw nice continuous pictures where all the transformations are local and all the structures that correspond to the same picture are canonically equivalent. I dream of a world where we understand this better, so that we can start with some kind of topologically-flavoured description of a structure and derive the algebraic definition from that instead of the other way around. (I have no idea if this is actually possible.)
Kevin Carlson (aka Arlin) (Mar 26 2024 at 18:17):Nathaniel's question sounds like one of the permanent threads in -category theory, which is the tension and interaction between combinatorial/algebraic definitions and topological ones, the ur-example being that an -groupoid can be modeled as either a topological space or as a Kan complex (or, on the third hand, as a type in homotopy type theory.) Since -groupoids are initial among appropriately-structured -categories, you can interpret any of these presentations of -groupoids in many different places, much as with string diagrams. I wonder whether it's reasonable to consider the relationship between "objects of a (say cocomplete) -category" and "topological spaces" as analogous to the relationship between "objects of a (say symmetric) monoidal category" and "certain subspaces of ."
Joshua Meyers (Mar 26 2024 at 19:51):I want to second @Mike Shulman's perspective --- I would be happy to see a combinatorial description of string diagrams but regardless of how reasonable it sounds in theory, I haven't seen it yet! Earlier in the thread there were some very general constructions cited with the claim that they specialize to string diagrams for monoidal categories, but I don't have the time to do the specialization myself; it would be great if the advocates of this approach would write out the combinatorial description in the case of monoidal categories I would really like to see it! thanks
otherwise, the Joyal-Street description is a bird in the hand...
Amar Hadzihasanovic (Mar 26 2024 at 20:06):The reason why I am not particularly interested in giving this independent description is that my motivation for developing such descriptions is to have a notion of diagram that is interpretable, as-is, not only in a monoidal category or more generally 2-category, but also, say, in a weak (infty, n)-category.
But there are some special things about dimension 2 which simply do not generalise, so the specialisation of the more general construction to dim 2 will contain data that is unnecessary in that special case. So if one is really uninterested in anything but planar monoidal category, I wouldn't recommend it! The whole point of it is the generalisability.
Amar Hadzihasanovic (Mar 26 2024 at 20:08):It seems like a waste of effort to write down a specialisation that is not as good as something that has been designed for that specific purpose, and nothing else.
John Baez (Mar 26 2024 at 20:15):On the other hand, people use string diagrams for monoidal categories far more than for weak (infinity,n)-categories, and they're easier to understand, so about 10 times as many people would read and cite a paper on string diagrams for monoidal categories, if it's well done.
Morgan Rogers (he/him) (Mar 26 2024 at 20:17):Only true for now @John Baez ! If Amar's work takes off and makes weak (infinity,n)-categories manageable to work with, we might find ourselves using them more and more ;)
Amar Hadzihasanovic (Mar 26 2024 at 20:18):@John Baez I guess I see this situation as having developed a constructive proof of a statement, valid — say — in every topos, and being asked to write down its specialisation to a Boolean topos where an easy classical proof already exists.
Many more people use classical logic than intuitionistic, but those same people will be unimpressed by the result!
Amar Hadzihasanovic (Mar 26 2024 at 20:22):My combinatorial 2-dim diagrams need a bunch of bookkeeping of weak units, which is wasted effort in strict 2-categories or monoidal categories, and only pays off in higher dimensions...
Joshua Meyers (Mar 26 2024 at 20:51):whoa I'd love to see a kind of string diagram that works natively in a general weak monoidal category where I don't have to always ask myself why it's okay to assume that a weak monoidal category is really strict...
maybe I'm misunderstanding the stakes of "bookkeeping of weak units"
John Baez (Mar 26 2024 at 20:52):Morgan Rogers (he/him) said:
Only true for now John Baez ! If Amar's work takes off and makes weak (infinity,n)-categories manageable to work with, we might find ourselves using them more and more ;)
I'm not saying his project is a bad idea, by any means! It's just that now there are lots of programmers, scientists, and non-category-theorist mathematicians interested in using string diagrams for monoidal 1-categories. The fraction of these who will take the trouble to learn about (infinity,n)-categories will be negligible - until the revolution comes, of course. So if Amar's framework can be specialized to monoidal 1-categories, someone should write a paper based on his, clearly stating the key theorems in the monoidal 1-category case, in a way that all these people can understand. That paper is the one all these people will read and cite.
Joshua Meyers (Mar 26 2024 at 20:54):Also: if you could specialize it not just to monoidal categories, but to all the categories in Selinger's survey and give combinatorial descriptions that make Joyal-Street style theorems fall out much more easily I would be very interested to read that
John Baez (Mar 26 2024 at 20:56):Yeah, go ahead and do twenty times as much work! :upside_down:
John Baez (Mar 26 2024 at 20:57):I was trying to suggest a way to help a lot of people and get a lot of credit for doing what might not be a huge amount of work.
Joshua Meyers (Mar 26 2024 at 20:58):Also: The claim that a bunch of people seemed to be making in this thread is that conventional string diagrams (as in Selinger's survey, or David Jaz's paper, etc.) are described better combinatorially than geometrically. I challenge anybody to back up this claim with an explicit combinatorial description. If the real claim was that this other kind of string diagram, for (infinity, n)-categories, is better described combinatorially, then I don't see why there should have been any disagreement in this thread. It is perfectly consistent that two different kinds of string diagrams would have different natural descriptions
Evan Patterson (Mar 26 2024 at 22:01):Joshua Meyers said:
Also: The claim that a bunch of people seemed to be making in this thread is that conventional string diagrams (as in Selinger's survey, or David Jaz's paper, etc.) are described better combinatorially than geometrically. I challenge anybody to back up this claim with an explicit combinatorial description.
I haven't followed this whole thread, so maybe I'm missing some context, but are you really claiming that people haven't proposed combinatorial descriptions? Here are a few:
And these are just some involving my colleage David Spivak (and in one case also me). More people have worked on this stuff and proposed other approaches.
Evan Patterson (Mar 26 2024 at 22:04):This stuff is very concrete and definite. We've implemented versions of it and use it regularly! Other groups have done similarly.
Aaron David Fairbanks (Mar 26 2024 at 22:13):Joshua Meyers said:
whoa I'd love to see a kind of string diagram that works natively in a general weak monoidal category where I don't have to always ask myself why it's okay to assume that a weak monoidal category is really strict...
String diagrams do work natively in a weak monoidal category. This is maybe not so well-known. I don't know of a paper that spells this out completely, but @Amar Hadzihasanovic and I have both considered writing something.
The kind of compositional structure that string diagrams most naturally describe is a "(colored) pro" -- it's like a multicategory, except the arrows can have multiple outputs as well as multiple inputs. Pros are essentially algebraic (just like categories or multicategories). I could spell out an essentially algebraic definition if someone wanted.
(A pro can equivalently be characterized as a strict monoidal category whose underlying monoid of objects is free. But let's prefer to think of a pro as a basic gadget in its own right. The reason being, we'll actually define monoidal categories in terms of pros. It's not a circular definition; you can define a pro without referring to monoidal categories.)
A pro is called "representable" if every list of objects (or equivalently, every pair of objects as well as the empty list) is isomorphic to a single object.
Theorem: The category of (weak) monoidal categories and (strong) monoidal functors is equivalent to the category of representable pros (in which the maps are just homomorphisms of pros, given by the essentially algebraic definition). Among other things, this theorem tells you that string diagrams work natively in a weak monoidal category.
(I think @Amar Hadzihasanovic also posted this same thing recently somewhere else on this Zulip, but it seems relevant here also and I want to spread the word wherever possible.)
You might look at this and be unimpressed, because you already knew that every monoidal category is equivalent to a strict one (and a pro is supposedly just some special kind of strict monoidal category). What's interesting is that "representable pro" is a good definition of "monoidal category". It's another way of presenting the same information as the usual definition. (Whenever I want to think about monoidal categories and monoidal functors I am secretly thinking about representable pros, because it's so much easier.) On the other hand, "strict monoidal category" is not a good definition of "monoidal category"; the category of monoidal categories is not equivalent to the category of strict monoidal categories and strict functors.
You can also see String diagrams for non-strict monoidal categories. I don't think they talk about pros, but I think it is basically the same story.
Cole Comfort (Mar 26 2024 at 22:31):String diagrams do work natively in a weak monoidal category. This is maybe not so well-known. I don't know of a paper that spells this out completely, but @Amar Hadzihasanovic and I have both considered writing something.
I think this is folk-lore. I have found it not as well-known as one might expect. There are papers which get at this point, including the one you have cited. As well as the work of Cockett and Seely on linearly distributive categories. There is also the work on Kelly-Maclane graphs from even earlier.
Joshua Meyers (Mar 26 2024 at 22:58):Aaron David Fairbanks said:
Joshua Meyers said:
whoa I'd love to see a kind of string diagram that works natively in a general weak monoidal category where I don't have to always ask myself why it's okay to assume that a weak monoidal category is really strict...
[...]
You can also see String diagrams for non-strict monoidal categories. I don't think they talk about pros, but I think it is basically the same story.
I've actually looked at this paper. It boils down to "interpret the string diagram in the strictification of M and then use the equivalence between M and the strictification of M" which makes sense. The issue is that the functor from the strictification of M to M is really complicated and has a ton of case analysis and lots of little lemmas to prove. I could work through it all but it would take a while. I could just choose to believe it but then I look at a string diagram and I don't even know what morphism in a (weak) monoidal category it's talking about...how do I parenthesize? where do I interpolate units and associators? etc. Maybe this is just a me problem
Joshua Meyers (Mar 26 2024 at 23:00):On the other hand, "strict monoidal category" is not a good definition of "monoidal category"; the category of monoidal categories is not equivalent to the category of strict monoidal categories and strict functors.
:open_mouth: This is frightening. Really shows that there is something substantial being pushed under the rug when people think it's okay to just assume everything is strict and not worry about it. I want to learn how this works for sure
John Baez (Mar 26 2024 at 23:18):Every weak monoidal category is equivalent to a strict one using strong monoidal functors, so you could argue that the problem is not strict monoidal categories but strict monoidal functors. (I will not so argue.) Every weak monoidal category is also equivalent to a skeletal one by means of strong monoidal functors - but not to a strict and skeletal one! This was worked out very nicely by Sinh in the case of 2-groups.
Aaron David Fairbanks (Mar 26 2024 at 23:19):Joshua Meyers said:
I could just choose to believe it but then I look at a string diagram and I don't even know what morphism in a (weak) monoidal category it's talking about...how do I parenthesize? where do I interpolate units and associators? etc. Maybe this is just a me problem
When we think of a monoidal category as a representable pro (and use string diagrams for it), all the parenthesization is explicit. For example, here is a picture of an associator component:
image.png
That's what the "representable" condition is about: every pair of objects and is isomorphic in the pro to a single object, i.e., their tensor product . (These isomorphisms and their inverses are labelled "" and "" in the attached picture.) Similarly, the empty list is isomorphic to a single object i.e., the monoidal unit .
Functoriality of tensor product, naturality of associator and unitors, pentagon, and triangle all fall out once we pick any particular parenthesization isomorphisms in the pro.
Dylan Braithwaite (Mar 26 2024 at 23:28):John Baez said:
you could argue that the problem is not strict monoidal categories but strict monoidal functors.
Indeed, this paper proves (in theorem 5.7) that when you quotient monoidal functors by natural isomorphism, the strictification adjunction becomes an equivalence.
Dylan Braithwaite (Mar 26 2024 at 23:32):I find it very hard to wrap my head around why this doesn't imply a 2-equivalence between them however
Kevin Carlson (aka Arlin) (Mar 26 2024 at 23:43):If two 2-categories have equivalent quotient-by-isomorphism-of-1-cells categories that doesn't imply that the underlying categories are equivalent (which is perhaps obvious) but also doesn't imply that are equivalent, which you're suggesting feels less obvious, Dylan. I'd consider the edge case that have just one object and one morphism (so they're doubly-delooped abelian groups.)
Dylan Braithwaite (Mar 26 2024 at 23:53):Kevin Carlson (aka Arlin) said:
If two 2-categories $A,B$ have equivalent quotient-by-isomorphism-of-1-cells categories $\tau_A,\tau_B,$ that doesn't imply that the underlying categories $A_0,B_0$ are equivalent (which is perhaps obvious) but also doesn't imply that $A,B$ are equivalent, which you're suggesting feels less obvious, Dylan. I'd consider the edge case that $A,B$ have just one object and one morphism (so they're doubly-delooped abelian groups.)
Yeah, I maybe phrased that last sentence too strongly. I certainly didn't mean that it suggests they should be equivalent, I know 2-equivalence and equivalence of the associated 1-categories are different things. I just meant that it seems to suggest the barrier to MonCat and StrMonCat being 2-equivalent is quite subtle, and I personally struggle to form any intuition for what fails in the 2-dimensional case that doesn't in the truncated case
Kevin Carlson (aka Arlin) (Mar 27 2024 at 00:16):Sure, so, the truncation of a 2-functor being an equivalence just says that the 2-functor itself is locally essentially surjective, right? So since the strictification 2-functor is presumably locally faithful, the problem has to be that it's not locally full. And it doesn't seem too shocking that not every monoidal transformation between strictifications of strong monoidal functors comes from a monoidal transformation between the original functors.
Joshua Meyers (Mar 27 2024 at 02:00):If we take morphisms in StrMonCat to be strong monoidal functors rather than strict monoidal functors, I don't see why it wouldn't be 2-equivalent to MonCat. In fact, it is a full 2-subcategory so it gives equivalences of hom-categories, and it is essentially surjective since strictification is a thing.
Joshua Meyers (Mar 27 2024 at 02:01):I realize now that you said "strict functors" -- it is not so surprising to me that StrMonCat would be inequivalent to MonCat if we only admit strict monoidal functors
Joshua Meyers (Mar 27 2024 at 02:07):Actually it is still somewhat surprising. This means that given strict monoidal categories and , the inclusion is not an equivalence. It is clearly fully faithful, so apparently it is not essentially surjective?? So there is some strong monoidal functor between strict monoidal categories which is not isomorphic to a strict monoidal functor? It would be great to see a simple example of this.
Aaron David Fairbanks (Mar 27 2024 at 02:35):Some misc. conjectures and facts. Anyone know how to answer these?
Kevin Carlson (aka Arlin) (Mar 27 2024 at 02:44):Nice example! I think I remember that strong monoidal functors from a group (as a discrete monoidal category) to an abelian group (as a monoidal category with one object) are group cohomology, even though there’s always just one strict monoidal functor.
John Baez (Mar 27 2024 at 02:52):That must be the second cohomology , since the laxator takes two objects of your first monoidal category and produces a morphism in your second monoidal category.
John Baez (Mar 27 2024 at 02:53):That must be related to Sinh's discovery that equivalence classes of monoidal categories with
are classified by , the third cohomology of with coefficients in the -module . Here we get the element of from the associator. If this element of is nonzero, the monoidal category we get is not equivalent to one that's both strict and skeletal!
John Baez (Mar 27 2024 at 02:56):It's worth noting that
so you can get nontrivial examples just taking - nice and small.
John Baez (Mar 27 2024 at 02:58):Those are great facts and conjectures, @Aaron David Fairbanks. I hope you put the facts on the nLab so I don't have to! It's good to get all these things sorted out and publicized.
Amar Hadzihasanovic (Mar 27 2024 at 06:03):Joshua Meyers said:
Aaron David Fairbanks said:
[...]
You can also see String diagrams for non-strict monoidal categories. I don't think they talk about pros, but I think it is basically the same story.I've actually looked at this paper. It boils down to "interpret the string diagram in the strictification of M and then use the equivalence between M and the strictification of M" which makes sense.
No, it does not boil down to that. That's the point that Aaron was making. If you think that that's the content of the paper, you need to read it more carefully. The equivalence between non-strict monoidal categories and representable pros is related to, but independent of strictification.
Joshua Meyers (Mar 27 2024 at 08:59):Amar Hadzihasanovic said:
Joshua Meyers said:
Aaron David Fairbanks said:
[...]
You can also see String diagrams for non-strict monoidal categories. I don't think they talk about pros, but I think it is basically the same story.I've actually looked at this paper. It boils down to "interpret the string diagram in the strictification of M and then use the equivalence between M and the strictification of M" which makes sense.
No, it does not boil down to that. That's the point that Aaron was making. If you think that that's the content of the paper, you need to read it more carefully. The equivalence between non-strict monoidal categories and representable pros is related to, but independent of strictification.
How does it not boil down to that?
Amar Hadzihasanovic (Mar 27 2024 at 09:02):The objects of the representable pro associated with a monoidal category are the objects of the monoidal category.
The objects of the strictification are, roughly, lists of objects of the monoidal category. They are not the same thing!
Joshua Meyers (Mar 27 2024 at 09:03):Amar Hadzihasanovic said:
The objects of the representable pro associated with a monoidal category are the objects of the monoidal category.
The objects of the strictification are, roughly, lists of objects of the monoidal category. They are not the same thing!
The paper I was claiming boils down to that doesn't mention pros though...
Amar Hadzihasanovic (Mar 27 2024 at 09:12):Yes, I believe the authors were not aware of the folklore that Cole mentioned nor the “appropriate” terminology, it was an independent rediscovery. But the content is essentially the same.
The thing that you need to appreciate is that there is an actual equivalence of 1-categories between the category of "representable coloured pros with a choice of 'tensoring' and 'unit' isomorphisms (what they call 'adapters')", with colour-preserving morphisms, and the category of monoidal categories and strong monoidal functors; whereas strictification of monoidal categories, as mentioned by Aaron, is definitely not an equivalence of 1-categories.
Amar Hadzihasanovic (Mar 27 2024 at 09:15):For what it's worth, I think that paper is a bit of a mess, and makes many unfortunate choices such as calling one side of this equivalence "strictification", even if it's not actually the strictification of a monoidal category ... unless you hit it with a bunch more functors, which is what the authors are doing under the hood
Joshua Meyers (Mar 27 2024 at 09:16):Huh? I'm not seeing any of this in the paper. They don't seem to even raise the question of whether the category of strict structures of some sort is 2-equivalent to MonCat. And why is their strictification not really a strictification?
Amar Hadzihasanovic (Mar 27 2024 at 09:24):Ok, looking at the paper I have to apologise to you, my recollection of it was warped -- I thought that the authors had realised the fact that I mention, but it does look like they didn't
Amar Hadzihasanovic (Mar 27 2024 at 09:28):I will try to make the point more precise. There is a (non-commutative) diagram of functors that looks like this:
Screenshot-from-2024-03-27-11-27-23.png
Amar Hadzihasanovic (Mar 27 2024 at 09:30):At the top of it, there is an actual equivalence of categories between the category of monoidal categories with strong monoidal functors and the category of coloured pros that are "representable" and have a choice of "adapter morphisms", together with their morphisms as coloured pros.
Martti Karvonen (Mar 27 2024 at 09:30):Regarding string diagrams for non-strict monoidal categories, what's wrong with just using ordinary string diagrams in that case? After all, once you fix the bracketing for the domain and codomain, the meaning of the diagram is uniquely fixed. Of course this needs the coherence theorem, but it's not like I need to replace the category in question with its strictification in order to interpret the diagram there.
Amar Hadzihasanovic (Mar 27 2024 at 09:32):The "strictification construction" that the authors describe in the paper we are discussing actually lands in . So if the authors were aware of this (folklore) result, they could have described this as an equivalence. This by itself completely justifies the use of string diagrams for non-strict monoidal categories.
Joshua Meyers (Mar 27 2024 at 09:33):Martti Karvonen said:
Regarding string diagrams for non-strict monoidal categories, what's wrong with just using ordinary string diagrams in that case? After all, once you fix the bracketing for the domain and codomain, the meaning of the diagram is uniquely fixed. Of course this needs the coherence theorem, but it's not like I need to replace the category in question with its strictification in order to interpret the diagram there.
It's not so simple. Suppose we fix the bracketing of the domain as and the first morphism in the string diagram has domain ? You will need to interpose unitors and associators possibly many times
Amar Hadzihasanovic (Mar 27 2024 at 09:34):But instead, they interpret it as an endofunctor on , by composing it with the sequence of functors around the square that I drew, which in turn
Amar Hadzihasanovic (Mar 27 2024 at 09:35):All of these functors are faithful, so you are not losing any information, and if you do this “round trip”, you do actually get the Mac Lane strictification of a monoidal category.
Martti Karvonen (Mar 27 2024 at 09:36):Joshua Meyers said:
Martti Karvonen said:
Regarding string diagrams for non-strict monoidal categories, what's wrong with just using ordinary string diagrams in that case? After all, once you fix the bracketing for the domain and codomain, the meaning of the diagram is uniquely fixed. Of course this needs the coherence theorem, but it's not like I need to replace the category in question with its strictification in order to interpret the diagram there.
It's not so simple. Suppose we fix the bracketing of the domain as and the first morphism in the string diagram has domain ? You will need to interpose unitors and associators possibly many times
Sure, but whatever choices you need to make to get the morphism to type-check result in a unique composite (by coherence).
Amar Hadzihasanovic (Mar 27 2024 at 09:36):But “taking this round trip” also adds a lot of garbage which is irrelevant to the question of string diagrams in non-strict monoidal categories (this is the reason why I think the paper is a bit of a mess).
Amar Hadzihasanovic (Mar 27 2024 at 09:37):@Martti Karvonen Yes, the point that you are making is precisely the informal content of the equivalence between and .
Joshua Meyers (Mar 27 2024 at 09:38):Martti Karvonen said:
Joshua Meyers said:
Martti Karvonen said:
Regarding string diagrams for non-strict monoidal categories, what's wrong with just using ordinary string diagrams in that case? After all, once you fix the bracketing for the domain and codomain, the meaning of the diagram is uniquely fixed. Of course this needs the coherence theorem, but it's not like I need to replace the category in question with its strictification in order to interpret the diagram there.
It's not so simple. Suppose we fix the bracketing of the domain as and the first morphism in the string diagram has domain ? You will need to interpose unitors and associators possibly many times
Sure, but whatever choices you need to make to get the morphism to type-check result in a unique composite (by coherence).
How do you do this rigorously? That is the question we are discussing
Amar Hadzihasanovic (Mar 27 2024 at 09:39):Again, it so happens that you have another way to “embed” the latter as a subcategory of the former, and this gives you the strictification. But this is irrelevant to the interpretation of string diagrams.
Amar Hadzihasanovic (Mar 27 2024 at 09:46):Now, to be fair, the authors also profess another aim in the paper, which is to reprove coherence in a different way -- and indeed, to prove that the functor landing in is an equivalence, you do need coherence.
But that also has nothing to do by itself with string diagrams in non-strict contexts, so it should probably not be the main technical content of a paper named that way.
Joshua Meyers (Mar 27 2024 at 09:58):Aaron David Fairbanks said:
Some misc. conjectures and facts. Anyone know how to answer these?
- Conjecture: The 1-category of monoidal categories and (strong) monoidal functors is not equivalent to the 1-category of strict monoidal categories and (strong) monoidal functors.
- John Baez tells us there is a skeletal monoidal category that is not (strong) monoidally equivalent to any strict skeletal one. It follows that there are isomorphism classes in not in the image of the inclusion from . (This shows the inclusion is not an equivalence, but it doesn't rule out there being some other weird equivalence.)
How does Baez's example show that the inclusion is not an equivalence? I'm not sure how you're doing the step you introduce with "It follows".
- Fact: The 2-category of monoidal categories and (strong) monoidal functors is equivalent to the 2-category of strict monoidal categories and (strong) monoidal functors.
- As Joshua Meyers said, we know this because every monoidal category is (strong) monoidally equivalent to a strict one.
- Fact: The 1-category of monoidal categories and (strong) monoidal functors is not equivalent to the 1-category of strict monoidal categories and strict monoidal functors.
- The former does not have an initial object whereas the latter does.
To elaborate on this, suppose was an initial object in the 1-category of monoidal categories and strong monoidal functors. Let be the strict monoidal category whose underlying monoid of objects is and where each pair of objects have a unique morphism between them. Then every constant functor to is strong monoidal.
This also shows that the 1-category of strict monoidal categories and strong monoidal functors is not equivalent to the 1-category of strict monoidal categories and strict monoidal functors.
- Conjecture: The 2-category of monoidal categories and (strong) monoidal functors is not equivalent to the 2-category of strict monoidal categories and strict monoidal functors.
- Joshua Meyers Here's an example of a (strong) monoidal functor between strict monoidal categories not isomorphic to a strict monoidal functor. (This shows the inclusion is not an equivalence, but it doesn't rule out there being some other weird equivalence.)
Consider the discrete strict monoidal category whose monoid of objects is the Booleans. Also consider the following strict monoidal category : its underlying monoid of objects is the naturals, and all objects > 0 have a unique morphism between them. There are no other nonidentity morphisms.
There is a unique strict monoidal functor from to , but there are other (strong) monoidal functors (equivalences, all isomorphic to each other) that are not isomorphic to it.
Nice example!
Joshua Meyers (Mar 27 2024 at 10:01):@Amar Hadzihasanovic how do you define a pro? how do you define representable? how do you define coloured? Or where can I find these definitions?
Amar Hadzihasanovic (Mar 27 2024 at 10:04):See this recent thread :)
Amar Hadzihasanovic (Mar 27 2024 at 10:05):(Actually that's about props vs symmetric monoidal cats, but just forget about symmetries.)
Amar Hadzihasanovic (Mar 27 2024 at 10:07):One way of describing a coloured pro is as a strict monoidal category whose objects form a free monoid on a set of "colours" (with the monoidal product on objects being the multiplication in the free monoid), and a morphism of coloured pros sends "colours" to "colours".
You can also (conceptually preferable) see them as independent compositional gadgets similar to operads/multicategories or properads.
Martti Karvonen (Mar 27 2024 at 10:08):Aaron David Fairbanks said:
Some misc. conjectures and facts. Anyone know how to answer these?
- Conjecture: The 1-category of monoidal categories and (strong) monoidal functors is not equivalent to the 1-category of strict monoidal categories and (strong) monoidal functors.
- John Baez tells us there is a skeletal monoidal category that is not (strong) monoidally equivalent to any strict skeletal one. It follows that there are isomorphism classes in not in the image of the inclusion from . (This shows the inclusion is not an equivalence, but it doesn't rule out there being some other weird equivalence.)
One way to show this is by showing that idempotents split in the 1-category of monoidal categories and strong monoidal functors but not when you restrict to strict monoidal categories, see section 6.2. of this paper by John Bourke.
Cole Comfort (Mar 27 2024 at 12:41):Amar Hadzihasanovic said:
For what it's worth, I think that paper is a bit of a mess, and makes many unfortunate choices such as calling one side of this equivalence "strictification", even if it's not actually the strictification of a monoidal category ... unless you hit it with a bunch more functors, which is what the authors are doing under the hood
What do you mean it is not the strictification? There is no canonical choice of strictification, which is the point of the coherence theorem in my view. In my reading, they have just produced a particular strictification, and have essentially reproven a version of the coherence theorem.
Cole Comfort (Mar 27 2024 at 12:44):I think that the exposition of string diagrams for non-strict monoidal/symmetric monoidal categories in the literature is quite lacking. And it is a shame that no one is allowed to publish this kind of folklore, because I believe it would be quite a useful resource to some people.
Joshua Meyers (Mar 27 2024 at 12:45):Is it really the case that no one is allowed to publish it? What about TAC Expositions? Or at least the arxiv...
Cole Comfort (Mar 27 2024 at 12:45):I think I have come across at least 3 different groups which have rediscovered this fact, which shows that people think this knowledge is important, and that it is unknown to them.
Cole Comfort (Mar 27 2024 at 12:46):Joshua Meyers said:
Is it really the case that no one is allowed to publish it? What about TAC Expositions? Or at least the arxiv...
I wasn't aware of TAC expositions. That would be a great venue. Maybe if I find a permanent job then I will try to write something for there.
Nathanael Arkor (Mar 27 2024 at 13:03):Cole Comfort said:
I think I have come across at least 3 different groups which have rediscovered this fact, which shows that people think this knowledge is important, and that it is unknown to them.
But this doesn't imply that they would be unable to publish it?
Nathanael Arkor (Mar 27 2024 at 13:08):Cole Comfort said:
I think that the exposition of string diagrams for non-strict monoidal/symmetric monoidal categories in the literature is quite lacking.
I admit I am still a little perplexed by even the term "string diagrams for non-strict monoidal categories", because my impression was that the entire point of string diagrams was that they could be used to reason about arbitrary monoidal categories. The authors of "String diagrams for non-strict monoidal categories" seem to agree with this. However, they claim it is still useful to be explicit about the non-strictness for examples, but I did not find their examples supported this claim. An alternative proof of the coherence theorem is one application, but it seems to me that, after one has proven the coherence theorem that way, one is justified in never using the more explicit notion of string diagram again. What am I missing?
Nathanael Arkor (Mar 27 2024 at 13:10):Cole Comfort said:
Amar Hadzihasanovic said:
For what it's worth, I think that paper is a bit of a mess, and makes many unfortunate choices such as calling one side of this equivalence "strictification", even if it's not actually the strictification of a monoidal category ... unless you hit it with a bunch more functors, which is what the authors are doing under the hood
What do you mean it is not the strictification? There is no canonical choice of strictification, which is the point of the coherence theorem in my view. In my reading, they have just produced a particular strictification, and have essentially reproven a version of the coherence theorem.
Perhaps the point of contention here is that the terms "strictification" and "coherence" are often used interchangeably, but they are technically different (but related) results? The correctness of string diagrams relies on coherence, rather than on strictification.
Aaron David Fairbanks (Mar 27 2024 at 14:36):Joshua Meyers said:
How does Baez's example show that the inclusion is not an equivalence? I'm not sure how you're doing the step you introduce with "It follows".
A monoidal isomorphism induces an isomorphism of underlying 1-categories, so it preserves skeletal-ness. So Baez's example tells us there are skeletal monoidal categories not monoidally isomorphic to any strict ones.
Aaron David Fairbanks (Mar 27 2024 at 14:39):Martti Karvonen said:
One way to show this is by showing that idempotents split in the 1-category of monoidal categories and strong monoidal functors but not when you restrict to strict monoidal categories, see section 6.2. of this paper by John Bourke.
Great, thanks! I'll check it out.
Aaron David Fairbanks (Mar 27 2024 at 15:07):What draws me to these "string diagrams for non-strict monoidal categories" personally is they help me think about monoidal functors. Think of the string diagram calculus as an essentally algebraic structure itself (this is what a colored pro is) and use that as a definition of monoidal category. Then monoidal functors turn out to be the straightforward homomorphisms: mapping the string diagrams and equalities underlying one monoidal category into the string diagrams and equalities underlying another monoidal category.
This is the only way I have been able to keep up with the conversation and give examples -- otherwise thinking about monoidal functors would make my brain hurt.
Aaron David Fairbanks (Mar 27 2024 at 15:21):Nathanael Arkor said:
However, they claim it is still useful to be explicit about the non-strictness for examples, but I did not find their examples supported this claim.
If you only knew the coherence theorem, but you didn't know about "string diagrams for non-strict monoidal categories" (particularly the equivalence of the 1-categories described above), then it would help you think about the morphisms in an individual monoidal category, but it wouldn't help you think about monoidal functors.
Amar Hadzihasanovic (Mar 27 2024 at 15:35):Cole Comfort said:
Amar Hadzihasanovic said:
For what it's worth, I think that paper is a bit of a mess, and makes many unfortunate choices such as calling one side of this equivalence "strictification", even if it's not actually the strictification of a monoidal category ... unless you hit it with a bunch more functors, which is what the authors are doing under the hood
What do you mean it is not the strictification? There is no canonical choice of strictification, which is the point of the coherence theorem in my view. In my reading, they have just produced a particular strictification, and have essentially reproven a version of the coherence theorem.
I mean that in turn to justify string diagrams in non-strict monoidal categories, they are implicitly treating the construction as landing in coloured pros, and not in strict monoidal categories, because in the category of coloured pros the "string diagrams" are colour-preserving functors, hence the wires are only allowed to be labelled with the objects of the original monoidal category.
Amar Hadzihasanovic (Mar 27 2024 at 15:36):If they actually were considering the strictification, then the valid string diagrams could also have wires labelled by lists of objects.
Amar Hadzihasanovic (Mar 27 2024 at 15:38):So it's like they're doing the correct construction of a representable pro, then adding a bunch of what is "garbage" for their stated purposes, and then ignoring the "garbage" they have just added.
Aaron David Fairbanks (Mar 27 2024 at 16:19):By the way, a completely analogous thing works for bicategories too, and I would guess there are analogous things that work for many other kinds of compositional structures. Theorem 2.3 in @Mike Shulman's paper A practical type theory for symmetric monoidal categories is the analogous theorem for symmetric monoidal categories (that they are equivalent to representable colored proPs), and this is the only place I've seen one of these results explicitly stated.
Mike Shulman (Mar 27 2024 at 21:59):I was away for a few days and didn't manage to read every word that was said recently, so my apologies if this was already said. But perhaps part of the confusion about pros is that one of the simplest definitions of a pro is as a strict monoidal category whose objects are a free monoid. So in that sense, on passing from an ordinary monoidal category to the equivalent pro one is "strictifying". Now one generally speaks of the "objects of the pro" as being not the objects of the strict monoidal category that it "is", but rather the generators of the free monoid of objects, and in that sense the set of objects is preserved when passing from a monoidal category to a pro. But I think there's also a sense in which the content of this equivalence is the same as the content of the strictification theorem.
Mike Shulman (Mar 27 2024 at 22:01):Also:
Dylan Braithwaite said:
Indeed, this paper proves (in theorem 5.7) that when you quotient monoidal functors by natural isomorphism, the strictification adjunction becomes an equivalence.
I don't think I believe that. The proof ends by claiming that since is a strict equivalence of categories, and are isomorphic in . But I don't think that follows; Par can be a strict monoidal functor that is an equivalence of categories without having an inverse equivalence that is also a strict monoidal functor, which is what would be required for the conclusion.
Aaron David Fairbanks (Mar 27 2024 at 22:59):Evan Patterson said:
I haven't followed this whole thread, so maybe I'm missing some context, but are you really claiming that people haven't proposed combinatorial descriptions? Here are a few:
And these are just some involving my colleage David Spivak (and in one case also me). More people have worked on this stuff and proposed other approaches.
Neat papers and diagrams. I think the people in this thread were interested to see combinatorial models of non-symmetric monoidal categories in particular, but it looks like the ones linked are symmetric. My understanding is the operad of wiring diagrams in the second paper could be described as "the operad for traced props (on a fixed color set)" and the operad of wiring diagrams in the third paper could be described as "the operad for props (on a fixed color set)". Is that right?
Evan Patterson (Mar 27 2024 at 23:01):That's right. All these papers are about the symmetric case. Sorry for missing the point!
Nathanael Arkor (Mar 27 2024 at 23:49):I think the people in this thread were interested to see combinatorial models of non-symmetric monoidal categories in particular
That isn't my impression. String diagrams for symmetric monoidal categories are more complicated than those for nonsymmetric monoidal categories, so it seems to me that that's even better.
Evan Patterson (Mar 27 2024 at 23:53):I think that string diagrams for SMCs are more useful than those for non-symmetric monoidal categories, just because the former seem to show up much more frequently in applications. But it's interesting that it seems easier to define graph-like combinatorial diagrams in the symmetric case, even though the structure is more complicated algebraically.
Mike Shulman (Mar 28 2024 at 03:18):Nathanael Arkor said:
I think the people in this thread were interested to see combinatorial models of non-symmetric monoidal categories in particular
That isn't my impression. String diagrams for symmetric monoidal categories are more complicated than those for nonsymmetric monoidal categories, so it seems to me that that's even better.
I would say that string diagrams for symmetric monoidal categories are simpler than those for nonsymmetric monoidal categories, because you don't have to worry about embedding them in a plane but they can just be abstract graphs or manifolds. That was my point a while ago: I think the combinatorial definitions of nonsymmetric string diagrams are more complicated and further from intuition than the topological ones that can literally talk about "embedding in a plane".
dusko (Mar 28 2024 at 09:16):that is a very nice observation, mike shulman. i sensed that difference but didn't quite manage to articulate it, and probably didn't even understand it.
but it is an interesting phenomenon objectively. the most natural version of string diagrams, the genuine poincare dual of the cell diagrams, the string diagrams for 2 categories, are not the most natural ones to manipulate. some things are easier to solve without them than with them. the string diagrams for the symmetric monoidal case are much easier, and i think almost always make things easier.
maybe the genuinely geometric string diagrams require chasing in a different medium? maybe with the help of some future intelligent interfaces, we will be able to chase string diagrams (face diagrams: 0-cells are the faces) in space.
Amar Hadzihasanovic (Mar 28 2024 at 10:00):I don't disagree about the primacy of “topological intuition”, but I guess I do disagree with what sort of mathematical object more closely adheres to the cognitive process behind “topological intuition”. As I tried to suggest, when I look at a string diagram and form a judgement about whether that diagram is a “embedded into a plane”, I believe that my brain is filtering out all the “point-set topological” stuff. I am not looking at what an edge is doing in any particular point, I am simply cataloguing elements of the picture as 0-dimensional, 1-dimensional, or 2-dimensional; and then I am going through a sequence of discrete checks, of the form “Are these two adjacent edges bounding a single region of space”? (Not so explicitly formed, but that is their essential content). So all the data that my brain is actually taking into account is
and that is exactly the information which would be stored into a combinatorial description of a planar string diagram.
Amar Hadzihasanovic (Mar 28 2024 at 10:09):I find that there's a certain amount of "begging the question" in these claims that an enormous equivalence class of continuous embeddings into gets to be "closer to intuition"; as if, this "gets" to be identified with a nice little picture in your head; whereas when you say "combinatorial description", you think of some table, or some Hasse diagram, or something dry and unreadable like that. But then the former is "closer to intuition" only because you are declaring it to be somehow equivalent to your intuition.
Joshua Meyers (Mar 28 2024 at 11:51):ok so can you give or cite a definition of a combinatorial description of a planar string diagram?
Nathaniel Virgo (Mar 28 2024 at 12:03):(I think people think different things about what's close to intuition because people develop their intuitions in completely different ways and have completely different things in their heads.)
Mike Shulman (Mar 28 2024 at 14:29):Yeah, we had this argument several times already in this thread and didn't get anywhere. I believe that my brain is not thinking about any of the extra data you have to impose on a planar diagram to make it combinatorial, and in partircular not thinking about any "2-dimensional" aspects of the picture, just about the fact that it is drawn on paper. There's no sense in which I'm thinking about an "enormous equivalence class", just about a single representative of it. And I'm surprised that you and others claim to find it complicated to intuit the connection between physical space and , which has been a staple of mathematical intuition and modeling for centuries. (Yes, of course, philosophers argue about it, but philosophers argue about everything.)
Joshua Meyers (Mar 28 2024 at 14:44):Well none of the proponents of a combinatorial definition of planar string diagram have yet actually exhibited one, they have just advocated for it in theory. I want to see how you would actually do it before I evaluate the approach.
Amar Hadzihasanovic (Mar 28 2024 at 14:49):Reasoning about geometry synthetically in terms of points, lines, faces and their incidence relation predates by a couple of millennia, so I don't think it should be difficult to believe that one's "topological intuition" can be structured along the former ideas rather than the latter.
Joshua Meyers (Mar 28 2024 at 14:50):Yeah it's not difficult to believe, I just want to see how it works in practice.
Amar Hadzihasanovic (Mar 28 2024 at 14:51):@Joshua Meyers I have linked a paper of mine that uses combinatorial planar string diagrams. This was not deemed satisfactory because the definition is "just" a special instance of a general higher-dimensional definition, and I was invited to write down its specialisation to 2 dimensions. Since there seems to be a lot of demand, I guess I should do it, after I am finished with other priorities.
Peva Blanchard (Mar 28 2024 at 14:55):This discussion reminds me of Daniel Kahneman's book "Thinking fast and slow". From what I remember, I quite liked the idea that "intuition" is the accumulation of practice, and the result of a long process that make a thing easy/fast/effortless to recall.
I guess we invoke "visual intuition" because, most of us (although not everyone) have a lot of visual experience. And it could be seen as bad faith the fact that someone would refuse this common (although not universal) source of experience. Of course, mathematical practice (e.g. algebraic manipulations, proving things, but also traditions and schools.) is (obviously) another great source of mathematical experience, thus mathematical intuition.
In short, I guess we cannot judge abstractly that "X is more intuitive than Y": it's more about practicing together.
ps: Daniel Kahneman died yesterday. RIP.
Mike Shulman (Mar 28 2024 at 15:34):Suppose we write a computer program in which the user can draw string diagrams (which many people have done). I think the most natural way of interacting with it is be like a vector graphics program: I can drop a node here and a node there, and then connect them with either a hand-drawn curve or perhaps a spline. Nowhere do I think about regions or orderings or any other combinatorial data. Of course this is a discretized version of , but I think it's much closer to that model than to any combinatorial one.
Nathanael Arkor (Mar 28 2024 at 15:46):For what it's worth, I think string diagrams, as people often use them, are far too flexible. People draw curved lines when straight lines will do (and correspond directly to the duals of the pasting diagrams), and this obscures the combinatorial perspective.
Amar Hadzihasanovic (Mar 28 2024 at 15:48):I think it's telling that you are saying a vector graphics program: that is, one in which "lines" and "nodes" will be stored as objects of a different class, with lines having endpoints that are associated to nodes.
By contrast, using a bitmap graphics program, where a line is literally a "continuous sequence of points" would be a nightmare!
I think the first is much closer to what I think of as combinatorial, and the second to "point-set" topological.
Nathanael Arkor (Mar 28 2024 at 15:48):I think string diagrams for monoidal categories should only involve curved lines in the presence of duals, for instance.
Joshua Meyers (Mar 28 2024 at 15:49):You often need curved lines to go around things and prevent collisions. Perhaps in many cases this could be avoided by judiciously moving the nodes around but it isn't necessarily a trivial computational problem to move the nodes around in such a way that all lines can be straight
Mike Shulman (Mar 28 2024 at 15:49):@Nathanael Arkor That seems to me like you are noticing a mismatch between how people use string diagrams and your preferred combinatorial formalization. I would say that means you should choose a different formalization, rather than complain that people should use them differently! (-:
Nathanael Arkor (Mar 28 2024 at 15:50):Joshua Meyers said:
You often need curved lines to go around things and prevent collisions. Perhaps in many cases this could be avoided by judiciously moving the nodes around but it isn't necessarily a trivial computational problem to move the nodes around in such a way that all lines can be straight
You need to be more careful about nodes, yes, e.g. allowing them to be wide to accommodate multiple inputs/outputs, but it's very simple to do in practice.
Joshua Meyers (Mar 28 2024 at 15:51):Allowing nodes to be wide won't help with having to go around them!
Nathanael Arkor (Mar 28 2024 at 15:51):Mike Shulman said:
Nathanael Arkor That seems to me like you are noticing a mismatch between how people use string diagrams and your preferred combinatorial formalization. I would say that means you should choose a different formalization, rather than complain that people should use them differently! (-:
Perhaps that really is the pertinent point, you're right.
Mike Shulman (Mar 28 2024 at 15:52):@Amar Hadzihasanovic, note that even in a vector graphics program the position of a node in the plane is a pair of numbers, a spline is specified by numbers indicating things like its starting and ending angles and its control points, and there is nothing representing regions or orderings. If you call that "combinatorial" then okay, but it seems to me like you do need something Joyal-Street-like to show how to interpret them.
Mike Shulman (Mar 28 2024 at 15:53):If you want to argue that Joyal and Street should have worked in algebraic geometry rather than differential geometry, I'll listen to that argument!
Mike Shulman (Mar 28 2024 at 15:53):But it's still geometry, not what I would call combinatorial.
Nathanael Arkor (Mar 28 2024 at 15:53):Nathanael Arkor said:
Mike Shulman said:
Nathanael Arkor That seems to me like you are noticing a mismatch between how people use string diagrams and your preferred combinatorial formalization. I would say that means you should choose a different formalization, rather than complain that people should use them differently! (-:
Perhaps that really is the pertinent point, you're right.
Although I think there are good reasons to use string diagrams in the way I would advocate, not just for reasons of formalisation. But perhaps that is a separate discussion.
Nathanael Arkor (Mar 28 2024 at 15:56):On the other hand, I belive using string diagrams in this way addresses the formalisation problem, without introducing any problems in practice :)
Joshua Meyers (Mar 28 2024 at 15:57):https://ncatlab.org/nlab/show/combinatorial+map seems relevant
Mike Shulman (Mar 28 2024 at 15:59):In the analogy to the interpretation of type-theoretic syntax, I would say that the combinatorial approaches are like intrinsically-well-typed inductive-inductive syntax; vector graphics are like untyped abstract syntax trees; and bitmap graphics are like strings of symbols. Parsing and lexing strings of symbols into ASTs is nontrivial but largely a solved problem, and similarly for passing from bitmaps to vectors. And interpreting well-typed syntax into a model is straightforward, but well-typed syntax is not what we write in practice. The interesting gap is between vector graphics or ASTs and well-typed syntax or semantics.
Joshua Meyers (Mar 28 2024 at 16:01):FWIW even though I agree with Mike that geometry is just as valid a foundation as algebra, and need not be reduced to algebra, I still would like to see a combinatorial (algebraic) definition of string diagram because it would give insight into the general form of a morphism in a presentation of a pro
Jean-Baptiste Vienney (Mar 28 2024 at 16:20):Something like in this paper? String Diagram Rewrite Theory II: Rewriting with Symmetric Monoidal Structure
Joshua Meyers (Mar 28 2024 at 16:21):We were more thinking about the not-necessarily-symmetric monoidal case
Jean-Baptiste Vienney (Mar 28 2024 at 16:21):Oh ok
Amar Hadzihasanovic (Mar 28 2024 at 16:31):@Mike Shulman my understanding of "combinatorial" is, essentially, that the primitives are nodes, edges, and faces -- as "atomic" elements that have different type -- together with their (possibly oriented) incidence relations. For me this does not imply intrinsic well-typedness.
You may say that in the monoidal case you do not need to have explicit faces, but you do in the general 2-categorical case, and I don't see a reason to treat them separately.
Amar Hadzihasanovic (Mar 28 2024 at 16:38):I think this is in line with how you interact with the diagrams in the hypothetical vector graphics program. You click on a node, it selects the node. You click on any point of an edge, it selects the entire edge. You click on a face, it selects the face, you can change its colour etc. You tweak their appearance/position, but the program modifies all the incident elements in order to keep the incidence relation stable.
Mike Shulman (Mar 28 2024 at 16:38):No, I don't click on a "face". There are no "faces".
Mike Shulman (Mar 28 2024 at 16:38):All there are are nodes and edges.
Nathanael Arkor (Mar 28 2024 at 16:39):Mike Shulman said:
but well-typed syntax is not what we write in practice
I would have said that well-typed syntax is precisely what we write (e.g. in a paper). In a programming language, input is inherently just textual (at least in mainstream programming languages), so one must technically write strings of symbols instead, but if there was a convenient input method for well-typed syntax, I would view that as wholly preferable.
Mike Shulman (Mar 28 2024 at 16:39):Sorry, I should have said intrinsically well-typed syntax is not what we write. Even in a paper, the reader has to do the typechecking step.
Mike Shulman (Mar 28 2024 at 16:40):Amar Hadzihasanovic said:
You may say that in the monoidal case you do not need to have explicit faces, but you do in the general 2-categorical case, and I don't see a reason to treat them separately.
I do. Namely, the monoidal case is simpler, because you don't have to think about faces! (-:
Nathanael Arkor (Mar 28 2024 at 16:47):I think one of my takeaways from this discussion is that it would be useful to have more precise terminology to refer to the different perspectives on string diagrams (and graphical syntaxes more generally), just as for the different perpectives on type theory (and term syntaxes more generally).
Dylan Braithwaite (Mar 28 2024 at 16:50):Joshua Meyers said:
We were more thinking about the not-necessarily-symmetric monoidal case
@Malin Altenmüller mentioned earlier in the thread her work on DPO rewriting for surface embedded graphs which I believe is intended to build towards a model for rewriting with planar string diagrams.
Doesn't this more-or-less give a combinatorial definition of the sort you're looking for?
Amar Hadzihasanovic (Mar 28 2024 at 16:55):828e6bce-cab5-4c07-9f80-2e91feba8826.png
@Mike Shulman This to me is as clearly "4 regions of the plane" as it is "2 intersecting lines". You are trying to suggest that it is possible for you to look at lines on paper (or the screen) in a way that neatly separates them from the regions of the plane that they bound. I simply do not think that this is how perception works!
Amar Hadzihasanovic (Mar 28 2024 at 16:57):There's plenty of optical illusions which make use precisely of the fact that "negative space" is as concrete to our senses as, well, its opposite :)
John Baez (Mar 28 2024 at 16:59):Nathanael Arkor said:
For what it's worth, I think string diagrams, as people often use them, are far too flexible. People draw curved lines when straight lines will do (and correspond directly to the duals of the pasting diagrams), and this obscures the combinatorial perspective.
For most people I know, the main point of string diagrams is not "the combinatorial perspective" - they are using these diagrams to think about algebraic structures like monads, quantum groups and such, and well-chosen curves can make it clearer what's going on algebraically.
Somewhere @Niles Johnson posted a series of pictures where he started with a poorly drawn (but technically correct) string diagrams and kept improving it.
Joshua Meyers (Mar 28 2024 at 17:00):Dylan Braithwaite said:
Joshua Meyers said:
We were more thinking about the not-necessarily-symmetric monoidal case
Malin Altenmüller mentioned earlier in the thread her work on DPO rewriting for surface embedded graphs which I believe is intended to build towards a model for rewriting with planar string diagrams.
Doesn't this more-or-less give a combinatorial definition of the sort you're looking for?
Yes this looks promising, I'll look at it later
Amar Hadzihasanovic (Mar 28 2024 at 17:00):You may not conceptualise "planarity" as "avoiding creating new faces", and instead conceptualise it as "avoiding intersecting lines", but I don't believe it is possible to separate the two dual perspectives
Joshua Meyers (Mar 28 2024 at 17:02):Amar Hadzihasanovic said:
You may not conceptualise "planarity" as "avoiding creating new faces", and instead conceptualise it as "avoiding intersecting lines", but I don't believe it is possible to separate the two dual perspectives
Drawing a new edge between two nodes creates exactly one new face, but it does not violate planarity unless it intersects a pre-existing edge, in which case it would create more than one new face.
Amar Hadzihasanovic (Mar 28 2024 at 17:04):But even if there were no faces, which is the case for symmetric monoidal diagrams, I still think that if you can only interact with edges "as a whole", and not with some subsets of their points, that's combinatorial and not point-set topological!
Amar Hadzihasanovic (Mar 28 2024 at 17:05):Joshua Meyers said:
Amar Hadzihasanovic said:
You may not conceptualise "planarity" as "avoiding creating new faces", and instead conceptualise it as "avoiding intersecting lines", but I don't believe it is possible to separate the two dual perspectives
Drawing a new edge between two nodes creates exactly one new face, but it does not violate planarity unless it intersects a pre-existing edge, in which case it would create more than one new face.
I'm talking of planarity of the embedding of some fixed graph, no talk of adding/removing edges.
Joshua Meyers (Mar 28 2024 at 17:06):then "creating new faces" doesn't make sense as there are no faces at all before you embed the graph
Amar Hadzihasanovic (Mar 28 2024 at 17:08):Creating new faces besides the ones you want to create -- is this better?
Amar Hadzihasanovic (Mar 28 2024 at 17:10):I'm imagining this in the context of our hypothetical diagram-drawing program.
Amar Hadzihasanovic (Mar 28 2024 at 17:12):Oh sorry I see, I should have added the specification "besides the intended ones" in the original sentence.
Amar Hadzihasanovic (Mar 28 2024 at 17:13):(After all you can also plausibly "intersect lines" if you want to create a new node at the intersection :) )
Joshua Meyers (Mar 28 2024 at 17:13):it's also hard to say which faces are intended since there are often many non-equivalent planar embeddings of the same graph, which would result in different faces
Amar Hadzihasanovic (Mar 28 2024 at 17:16):Well, if anything this is another argument against planar string diagrams being a planar embedding of some disembodied graph. Actually you only picture the diagram in your mind as already embedded with all its faces.
Joshua Meyers (Mar 28 2024 at 17:17):right, it's either a graph equipped with a planar embedding, or it's a graph equipped with some yet-to-be-elucidated combinatorial structure (perhaps the one in the paper @Dylan Braithwaite linked to, I didn't look at it yet)
Amar Hadzihasanovic (Mar 28 2024 at 17:19):My point is that the 2d faces are intrinsically part of the structure of a planar string diagram.
Mike Shulman (Mar 28 2024 at 17:19):Amar Hadzihasanovic said:
You may not conceptualise "planarity" as "avoiding creating new faces", and instead conceptualise it as "avoiding intersecting lines", but I don't believe it is possible to separate the two dual perspectives
I do. Avoiding intersecting lines is as simple as asking whether two functions have disjoint images. Asking anything about "faces" involves the Jordan curve theorem.
Amar Hadzihasanovic (Mar 28 2024 at 17:19):It is not "a graph + something"... it's a 2d object
Mike Shulman (Mar 28 2024 at 17:20):Amar Hadzihasanovic said:
But even if there were no faces, which is the case for symmetric monoidal diagrams, I still think that if you can only interact with edges "as a whole", and not with some subsets of their points, that's combinatorial and not point-set topological!
If you want to call that "combinatorial" that's fine with me, but as I said, that means that some "combinatorial" definitions require some Joyal-Street-like argument to interpret.
Amar Hadzihasanovic (Mar 28 2024 at 17:25):Mike Shulman said:
Amar Hadzihasanovic said:
You may not conceptualise "planarity" as "avoiding creating new faces", and instead conceptualise it as "avoiding intersecting lines", but I don't believe it is possible to separate the two dual perspectives
I do. Avoiding intersecting lines is as simple as asking whether two functions $[a,b] \to \mathbb{R}^2$ have disjoint images. Asking anything about "faces" involves the Jordan curve theorem.
Euclid understood faces in 300BC. Next thing you are going to tell me that Pythagoras' theorem involves understanding sine and cosine functions.
Joshua Meyers (Mar 28 2024 at 17:28):I love Euclid but it does not meet modern standards of rigor. E.g. in Book 1 Prop 1 he constructs an equilateral triangle on a line segment AB by first drawing a circle with center A and radius AB and a circle with center B and radius BA, then he says "let C be the intersection of the two circles". Well how do we know the circles intersect???? He is clearly missing some stuff that would be needed today to discuss planarity
Evan Patterson (Mar 28 2024 at 17:34):Nathanael Arkor said:
I think one of my takeaways from this discussion is that it would be useful to have more precise terminology to refer to the different perspectives on string diagrams (and graphical syntaxes more generally), just as for the different perpectives on type theory (and term syntaxes more generally).
It doesn't seem to be standard, even in the ACT community, but the terminology that I picked up from David Spivak is
Mike Shulman (Mar 28 2024 at 17:49):Amar Hadzihasanovic said:
Euclid understood faces in 300BC. Next thing you are going to tell me that Pythagoras' theorem involves understanding sine and cosine functions.
Yes, and one can argue about whether Euclid understood faces as well as he thought he did. But that wasn't the question -- you said you don't believe it is possible to separate the dual perspectives, and I was arguing that it is possible, because as an example, in the context of modern point-set topology, one perspective is easy and the other is highly nontrivial.
Amar Hadzihasanovic (Mar 28 2024 at 18:09):I meant it is not possible to separate them in our perception of the string diagram as a physical object; I think we perceive simultaneously the lines and the regions that they bound, with no chance of isolating the ones from the others. As in the cartesian plane example: the 4 quadrants are as immediately perceived as the 2 axes.
I think this is relevant to the question of what is "close to intuition". The "embedded graph" creates a separation between a disembodied graph and its embedding into a plane that I do not think exists: when we approach drawing a string diagram, I'd say we picture it already with its placement in the plane, faces and all. We don't first think about a floating node with dangling edges, and only then about "how I should place this node and its edges on the page".
Amar Hadzihasanovic (Mar 28 2024 at 18:14):Which is why I advocate that a combinatorial planar string diagram should be, directly, a 2d object, made of nodes, edges, and faces.
Anyway, even though there's a lot of disagreement, I should say that I am thankful for this discussion, because it's giving me a lot of questions that I will need to address if I write this note/paper on "combinatorial string diagrams".
Amar Hadzihasanovic (Mar 28 2024 at 18:17):(And also that, while here I am playing the "combinatorics advocate", as I tried to say at the beginning of the discussion I am not on the "string diagrams are REALLY combinatorial" side -- more on the "the combinatorial side is really sort of inextricable from the topological side, and both are equally useful")
Joshua Meyers (Mar 29 2024 at 02:52):Dylan Braithwaite said:
Joshua Meyers said:
We were more thinking about the not-necessarily-symmetric monoidal case
Malin Altenmüller mentioned earlier in the thread her work on DPO rewriting for surface embedded graphs which I believe is intended to build towards a model for rewriting with planar string diagrams.
Doesn't this more-or-less give a combinatorial definition of the sort you're looking for?
BTW I skimmed this paper and it is definitely in the right direction! However it does not culminate in a combinatorial model of planar string diagrams, but leaves it for future work, perhaps that @Amar Hadzihasanovic will do.
dusko (Mar 30 2024 at 10:53):i am probably late to the train of this conversation but i'll say what i have been thinking. it's easy to ignore :)
the conversation seems to have been whether combinatorial or topological view of string diagrams was more intuitive. but a different angle could be: math is not there to comply with our intuitions, but to expand them. if i intuitively understand a puzzle, i can solve it in my head. i need the physical puzzle to twiddle with it and move it because all those moves don't fit into my intuition. math is like that physical puzzle. it helps you solve things that you couldn't solve by intuition. sometimes you solve a puzzle and still don't know what exactly you've done. archimedes really needed the sand to draw his circles. if he could do it in his head, he wouldn't have been so annoyed with the soldiers and wouldn't have gotten killed. and of all people von neumann said: "you don't understand math. you get used to it."
to prove unintuitive things, people drew lots of pictures, then translated them into equations so they wrote lots of equations. the theory of invariants ran equations from page to page to page. diagram chasing packs lots of equations into a picture. you can manipulate your equations without drowning in a flood of letters. so cell diagrams help us capture things that are beyond our intuitions. cell diagrams reduce sequences of equations to "discrete homotopies". then you add 2-cells and they aren't even discrete anymore...
but we don't chase string diagrams. we write sequences of equations between string diagrams. so that looks like a step back. what might be good about that? well, for monoidal categories string diagrams give us more insightful pictures of the "arrows" that we would otherwise chase. they liberate us from ever having to chase around the middle-two-interchange square since both ways around it are the same string diagram, just read in different ways. so they save us a step or two in every chase. so we revert to equations because we saved a couple?
on a better look, well-designed equational steps with string diagrams are geometric transformations with significant invariants. the adjunction equations just transform a boundary: "yanking" of the string, or twisting it in a different way. the frobenius law is a geometric transformation similar to the kempe move from his "proof" of 4-color theorem: you take the H and put it on the side. (though we usually look at two different Hs, more like N and И. but it is still the kempe move.)
i think we write the string diagram transformations as equations because the medium we use them does not support chasing string diagrams --- and NOT because string diagrams do not support chasing. eg, if you fix the outer faces of the frobenius law as sheets and draw the two sides of the equation on two foils glued along this shared external sheet, then the law is again a "discrete homotopy" step, albeit with a dimension more. OR you can add a 3-cell, and it is not discrete anymore.
if people set their minds to it (and if they don't drown in melted ice) i am sure someone will come up with an interface for chasing string diagrams.
Aaron David Fairbanks (Mar 30 2024 at 13:00):dusko said:
if people set their minds to it (and if they don't drown in melted ice) i am sure someone will come up with an interface for chasing string diagrams.
If I understand you correctly, homotopy.io is an example of this.
Niles Johnson (Mar 30 2024 at 19:47):John Baez said:
Somewhere Niles Johnson posted a series of pictures where he started with a poorly drawn (but technically correct) string diagrams and kept improving it.
Ha ha, did I?! That sounds like something I would do, since I've often found them more confusing than they are clarifying. Maybe that happened back before Twitter imploded, when Donald and I were trying to compare string diagrams with pasting diagrams in our 2-categories book.
Probably the only nontrivial contribution I could make to this discussion is to concur that many people want to use string diagrams to convey some fact or calculation, and sometimes they are the best way to do that. (And, maybe sometimes not, but that's off-topic here.)
John Baez (Mar 30 2024 at 20:48):Hmm, I thought you did it somewhere else. But maybe it was someone else. I think it was in a discussion of monads and their algebras. The first string diagram had straight lines, and then whoever it was started curving them and explaining how this made the meaning clearer.
Niles Johnson (Mar 30 2024 at 21:02):Hmmm, no I think that must have been someone else.
Nathanael Arkor (Mar 30 2024 at 21:12):John Baez said:
Hmm, I thought you did it somewhere else. But maybe it was someone else. I think it was in a discussion of monads and their algebras. The first string diagram had straight lines, and then whoever it was started curving them and explaining how this made the meaning clearer.
I would be interested to see that.
Samuel Steakley (Mar 30 2024 at 21:13):John Baez said:
Hmm, I thought you did it somewhere else. But maybe it was someone else. I think it was in a discussion of monads and their algebras. The first string diagram had straight lines, and then whoever it was started curving them and explaining how this made the meaning clearer.
Sounds like some material from Ralf Hinze and @Dan Marsden 's book "Introducing String Diagrams."
John Baez (Mar 30 2024 at 22:04):Right, it was @Dan Marsden! Here is an example.
Nathanael Arkor (Mar 31 2024 at 06:15):Dan doesn't actually say that the different versions convey information better/worse (or how they do, if they do). He just says:
there's a lot of scope for artistic expression.
Samuel Steakley (Mar 31 2024 at 07:24):Ralf and Dan make some stronger statements about better/worse design in Introducing String Diagrams (e.g. page 43).
Dan Marsden (Mar 31 2024 at 08:56):I've alway been interested in this point about drawing the diagrams to improve human intuition, which is why I manually lay out the tikz for each of my diagrams. An early remark in freely available work is in my preprint https://arxiv.org/pdf/1401.7220.pdf, remark 4.19 on artistic values, in that case relating to distributive law axioms. (The diagrams are the opposite way up to my later work with Ralf).
John Baez (Mar 31 2024 at 17:44):Nathanael Arkor said:
Dan doesn't actually say that the different versions convey information better/worse (or how they do, if they do). He just says:
there's a lot of scope for artistic expression.
Somewhere he did say that, I'm pretty sure. What I just found seems like a very abbreviated version of what he actually said somewhere.
John Baez (Mar 31 2024 at 17:56):In remark 4.19 he shows a diagram that he says is worse than some other one, but I seem to be remembering something else.
Joshua Meyers (Apr 25 2024 at 16:30):Aaron David Fairbanks said:
Joshua Meyers said:
whoa I'd love to see a kind of string diagram that works natively in a general weak monoidal category where I don't have to always ask myself why it's okay to assume that a weak monoidal category is really strict...
String diagrams do work natively in a weak monoidal category. This is maybe not so well-known. I don't know of a paper that spells this out completely, but Amar Hadzihasanovic and I have both considered writing something.
The kind of compositional structure that string diagrams most naturally describe is a "(colored) pro" -- it's like a multicategory, except the arrows can have multiple outputs as well as multiple inputs. Pros are essentially algebraic (just like categories or multicategories). I could spell out an essentially algebraic definition if someone wanted.
(A pro can equivalently be characterized as a strict monoidal category whose underlying monoid of objects is free. But let's prefer to think of a pro as a basic gadget in its own right. The reason being, we'll actually define monoidal categories in terms of pros. It's not a circular definition; you can define a pro without referring to monoidal categories.)
A pro is called "representable" if every list of objects (or equivalently, every pair of objects as well as the empty list) is isomorphic to a single object.
Theorem: The category of (weak) monoidal categories and (strong) monoidal functors is equivalent to the category of representable pros (in which the maps are just homomorphisms of pros, given by the essentially algebraic definition). Among other things, this theorem tells you that string diagrams work natively in a weak monoidal category.
(I think Amar Hadzihasanovic also posted this same thing recently somewhere else on this Zulip, but it seems relevant here also and I want to spread the word wherever possible.)
You might look at this and be unimpressed, because you already knew that every monoidal category is equivalent to a strict one (and a pro is supposedly just some special kind of strict monoidal category). What's interesting is that "representable pro" is a good definition of "monoidal category". It's another way of presenting the same information as the usual definition. (Whenever I want to think about monoidal categories and monoidal functors I am secretly thinking about representable pros, because it's so much easier.) On the other hand, "strict monoidal category" is not a good definition of "monoidal category"; the category of monoidal categories is not equivalent to the category of strict monoidal categories and strict functors.
You can also see String diagrams for non-strict monoidal categories. I don't think they talk about pros, but I think it is basically the same story.
Can you please explain how to use "representable pro" as a good definition of "monoidal category", such that you can secretly think about representable pros instead whenever you have to think about monoidal categories?
Joshua Meyers (Apr 25 2024 at 20:05):I get the general idea but I would like to see the details
Aaron David Fairbanks (Apr 26 2024 at 01:57):Hi, sure. I gave a talk about this earlier in the year. The fastest way for me to put together an explanation right now is to just share my script and slides from that talk.
https://docs.google.com/document/d/1o791NNK6xcIc_6Y8gbdWLxk64n2RE86rjRJBqqDaXJ4/edit?usp=sharing
But we'll see how effective this is. It's probably still not enough detail. Feel free to ask me to elaborate on anything specifically.
Joshua Meyers (Apr 26 2024 at 14:57):I read through this, very nice. My first thought is that the particular choice of isomorphisms should be included as part of the structure of a representable pro --- otherwise you risk using different isomorphisms different times and not having them cancel as is required for many of the arguments. That said, it is surprising to me that there don't seem to be any coherence conditions required of the choice of isomorphisms, or any requirement that they be preserved by maps of representable pros.
Amar Hadzihasanovic (Apr 26 2024 at 15:08):The choice of representing isomorphisms is unique up to a unique equivalence, so I think that the proper way to approach this is to impose a choice if one wants an equivalence of categories, but a choice is not actually needed if one wants a biequivalence of 2-categories...
Amar Hadzihasanovic (Apr 26 2024 at 15:09):Maps of representable pros respecting a given choice would correspond to strict monoidal functors.
Joshua Meyers (Apr 26 2024 at 15:12):My point is that this argument doesn't work without imposing a choice. "tensoring cancels with untensoring" fails if you use two different tensoring morphisms
image.png
Amar Hadzihasanovic (Apr 26 2024 at 15:14):Ah, sorry, yes: the "untensoring" morphisms do have to be the inverses of the "tensoring" ones.
Aaron David Fairbanks (Apr 26 2024 at 15:14):It's true that the direct translation process goes between representable pros + chosen isomorphisms on one hand and monoidal categories on the other hand. But also, monoidal functors between monoidal categories correspond to maps between their underlying pros not respecting the chosen isomorphisms.
Aaron David Fairbanks (Apr 26 2024 at 15:17):So the category of monoidal categories is equivalent to the category of representable pros without chosen tensor isomorphisms. (Or, if you prefer, it's the category of representable pros with chosen tensor isomorphisms but with maps not respecting them. These are equivalent categories.)
Mike Shulman (Apr 26 2024 at 15:39):Even more precisely, strong monoidal functors correspond to pro-maps not respecting the chosen isomorphisms, while strict monoidal functors correspond to pro-maps that do respect the chosen isomorphisms.
Nathaniel Virgo (Apr 27 2024 at 01:03):Aaron David Fairbanks said:
Hi, sure. I gave a talk about this earlier in the year. The fastest way for me to put together an explanation right now is to just share my script and slides from that talk.
https://docs.google.com/document/d/1o791NNK6xcIc_6Y8gbdWLxk64n2RE86rjRJBqqDaXJ4/edit?usp=sharing
But we'll see how effective this is. It's probably still not enough detail. Feel free to ask me to elaborate on anything specifically.
Is the double category story at the end written down anywhere?
Aaron David Fairbanks (Apr 27 2024 at 01:22):No. @Mike Shulman and I have an unfinished paper about this. It was also back in this Zulip thread from a long time ago: https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-questions/topic/representable.20props.20and.20pros/near/301511384
Aaron David Fairbanks (Apr 27 2024 at 01:29):I am going to have more free time soon, so I'll try to finish some of these projects.
Josh Chen (Aug 12 2024 at 11:49):Nathanael Arkor said:
Cole Comfort said:
I think that the exposition of string diagrams for non-strict monoidal/symmetric monoidal categories in the literature is quite lacking.
I admit I am still a little perplexed by even the term "string diagrams for non-strict monoidal categories", because my impression was that the entire point of string diagrams was that they could be used to reason about arbitrary monoidal categories. The authors of "String diagrams for non-strict monoidal categories" seem to agree with this. However, they claim it is still useful to be explicit about the non-strictness for examples, but I did not find their examples supported this claim. An alternative proof of the coherence theorem is one application, but it seems to me that, after one has proven the coherence theorem that way, one is justified in never using the more explicit notion of string diagram again. What am I missing?
FWIW, I found this thread precisely because I was looking for string diagram formalisms in non-strictly associative settings. In my thesis I'm doing a lot of reasoning on equalities between morphisms in wild categories, which in many cases can be reasoned about as though they were bicategories, except that they crucially don't satisfy the same coherence/strictification result. It would still be nice to have some graphical formalism that eases the equational bureaucracy..
John Baez (Aug 12 2024 at 14:06):What are "wild categories"?
Josh Chen (Aug 12 2024 at 14:52):They're most immediately understood in a HoTT setting, where they're defined just like what the HoTT book precategories, except where precategories have sets of morphisms, wild categories have arbitrary morphism types .
Losing the set truncatedness condition means no longer behaves as expected of a 1-category nor a nicely coherent -category, is some "wild", or precoherent, version of an -cat.
Josh Chen (Aug 12 2024 at 15:00):Classically, I think they roughly correspond to -restricted simplicial spaces (i.e. ) with some appropriately restricted Segal condition, or maybe some kind of "wild enrichment" in Batanin-Leinster weak -groupoids... I'm investigating them as a building block/stepping stone to do "enough" -category theory in book HoTT.