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.
Fabio Zanasi (Apr 11 2023 at 16:27):I'm working on something involving closed monoidal categories, and I wondered if anybody has a pointer on the construction of a free symmetric closed monoidal category (SCMC) starting from a collection of generating objects and morphisms.
Traditionally, SCMCs are described as SMCs where the tensor has a right adjoint. However, I believe it should be doable to describe this data equivalently by saying that there are eval_{A,B} morphisms for each objects A,B, and Lambda(f) morphisms for each morphism f, satisfying certain equations. I've started working this out myself (in fact, I've used something along these lines fairly recently, in a FSCD2022 paper on rewriting in SCMCs, but I'd like to understand it more systematically). However, I have the impression it should be written somewhere already. Any hint?
Matteo Capucci (he/him) (Apr 11 2023 at 16:31):Sorry for the very dumb comment but can't you use eval and to recover the units and counits of the tensor-hom adjunction? then you're back at the problem of presenting a monoidal category
Mike Shulman (Apr 11 2023 at 16:31):Are you thinking of a linear type theory, something like section 2.10 of mikeshulman.github.io/catlog/catlog.pdf?
Cole Comfort (Apr 11 2023 at 16:36):I think what you want is contained in the paper, "Graphical presentations of symmetric monoidal closed theories"
https://hal.science/hal-00333750/file/smcc.pdf
Fabio Zanasi (Apr 11 2023 at 22:56):Mike Shulman said:
Are you thinking of a linear type theory, something like section 2.10 of mikeshulman.github.io/catlog/catlog.pdf?
Mmm I'm thinking of something way more basic than this. Just a presentation by generators and relations.
Fabio Zanasi (Apr 11 2023 at 23:01):Matteo Capucci (he/him) said:
Sorry for the very dumb comment but can't you use eval and to recover the units and counits of the tensor-hom adjunction? then you're back at the problem of presenting a monoidal category
Basically yes, that's the route I pursued. But I was wondering whether there was an existing reference for this style of presentation, perhaps also operating some simplifcation with respect to a plain translation of the unit/counit conditions.
The question is related to using string diagrams to reason about free SCMCs. Note for the case of SMCs we can confine ourselves to generating objects as wire labels, but this does not seem possible for SCMCs, because arbitrary objects are not just lists of generators but more complex entities (they mix $\otimes$ with $\multimap$).
Fabio Zanasi (Apr 11 2023 at 23:04):Cole Comfort said:
I think what you want is contained in the paper, "Graphical presentations of symmetric monoidal closed theories"
This seems very much relevant, thanks. I'm going to study it in more detail.
Cole Comfort (Apr 12 2023 at 12:26):Fabio Zanasi said:
Matteo Capucci (he/him) said:
Sorry for the very dumb comment but can't you use eval and to recover the units and counits of the tensor-hom adjunction? then you're back at the problem of presenting a monoidal category
Basically yes, that's the route I pursued. But I was wondering whether there was an existing reference for this style of presentation, perhaps also operating some simplifcation with respect to a plain translation of the unit/counit conditions.
The question is related to using string diagrams to reason about free SCMCs. Note for the case of SMCs we can confine ourselves to generating objects as wire labels, but this does not seem possible for SCMCs, because arbitrary objects are not just lists of generators but more complex entities (they mix $\otimes$ with $\multimap$).
@Mike Shulman proved that closed symmetric monoidal categories fully faithfully embed in *-autonomous categories:
https://arxiv.org/pdf/2004.08487.pdf (https://www.youtube.com/watch?v=5CjSu5hLtcw)
So you can regard the object as . This may not be a completely satisfying to you, but this perspective is conceptually useful for me.
Robin Piedeleu (Apr 13 2023 at 08:34):I was also going to mention Mike Shulman's work. I think it implies that you can use string diagrams for compact closed categories for smccs too, but not all diagrams you can draw are allowed in that context. An alternative---which seems closer in spirit to what you had in mind---could be to use local constraints like the bubbles and clasp of the Rosetta Stone paper. Not sure a formal account of that has been fully worked out anywhere, though.
Cole Comfort (Apr 13 2023 at 09:43):Robin Piedeleu said:
I was also going to mention Mike Shulman's work. I think it implies that you can use string diagrams for compact closed categories for smccs too, but not all diagrams you can draw are allowed in that context.
I wonder if there is a formal way to state this.
An alternative---which seems closer in spirit to what you had in mind---could be to use local constraints like the bubbles and clasp of the Rosetta Stone paper. Not sure a formal account of that has been fully worked out anywhere, though.
Isn't the bubble and clasp notation formalized by this conservativity result of symmetric monoidal closed categories? The clasp is a way to enforce that the proof net has the correct type to be in the image of the embedding. Perhaps I am missing some nuance?
Also, Hinze points out that another way to view this clasp and bubble thing is in terms of a right Kan extension, which you might find interesting:
https://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf
Mike Shulman (Apr 13 2023 at 15:48):What my work says directly is that you can use string diagrams for -autonomous categories for smccs too. The string diagrams for -autonomous categories look like a subset of the ones for compact closed categories, but I don't know of anywhere that this is made precise. Category-theoretically, I think the question is whether any -autonomous category can be embedded faithfully (certainly not fully) in a compact closed category. I have asked this question before and no one seems to know the answer. I don't even know of any technology that could help establish it.
Mike Shulman (Apr 13 2023 at 15:50):I don't immediately see a relationship between the bubble and clasp notation and my embedding theorem. My embedding is full, so there is no condition required on the string diagrams themselves: any -autonomous string diagram whose domain and codomain are in the image of the embedding is a valid "closed symmetric monoidal string diagram".
Fabio Zanasi (Apr 14 2023 at 14:43):Thank you all, I'll look more closely at Mike's work. Robin, answering your question on the clasp notation for string diagrams in monoidal closed categories, it is formalised in my CSL'23 paper, and also used in my FSCD'22 paper. I don't claim it to be totally novel, but while doing those works we could not find it worked out systematically anywhere, so we did it ourselves.
However note the clasp (which we call 'bubble') is syntactic sugar for one of the functors in the adjunction situation. So it's not by itself an answer to my question about a presentation by generators and relations.
Mike Shulman (Apr 14 2023 at 15:51):@Fabio Zanasi, can you give a link to those papers?
Fabio Zanasi (Apr 14 2023 at 19:32):@Mike Shulman there you go: https://drops.dagstuhl.de/opus/volltexte/2023/17467/pdf/LIPIcs-CSL-2023-6.pdf
Fabio Zanasi (Apr 14 2023 at 19:32):We aimed at a very specific application (automatic differentiation) for which we needed higher-order string diagrams
Fabio Zanasi (Apr 14 2023 at 19:33):BTW Dan Ghica and I have a longer, more systematic account of these 'hierarchical string diagrams' in preparation, I'll share when ready.
Robin Piedeleu (Apr 16 2023 at 20:22):Fabio Zanasi said:
Thank you all, I'll look more closely at Mike's work. Robin, answering your question on the clasp notation for string diagrams in monoidal closed categories, it is formalised in my CSL'23 paper, and also used in my FSCD'22 paper. I don't claim it to be totally novel, but while doing those works we could not find it worked out systematically anywhere, so we did it ourselves.
However note the clasp (which we call 'bubble') is syntactic sugar for one of the functors in the adjunction situation. So it's not by itself an answer to my question about a presentation by generators and relations.
I thought the 'bubble' in these hierarchical string diagrams were different from the 'bubble and clasp' notation of the Rosetta stone paper: as far as I understand, for hierarchical diagrams, the bubbles are an explicit notation for the exponentiation functor (in the style of functorial boxes, I assume?), whereas the bubbles and clasps are syntactic markers used to constrain where you can apply the yanking rule to diagrams (that, in a compact closed category, you can apply freely, but that is restricted in a merely closed monoidal category). Thus, in the former, you can box a diagram with two wires at the bottom and one at the top into a bubble, to obtain one of type with one wire at the bottom for and one at the top for . For the latter, as far as I understand, you turn the same diagram into one with two wires at the top--one for and one for --joined by a clasp to indicate that, together, they represent the object . As @Cole Comfort wrote, the 'bubble and clasp' notation seems more closely related to @Mike Shulman 's result (which could be understood to formalise the idea that you can remove these bubble and clasps as long as the diagram you deal with is in the image of the embedding of smccs into -autonomous ones? I would need a bit more time to convince myself that's the case). Am I totally off here?
Mike Shulman (Apr 17 2023 at 20:48):I don't know about hierarchical diagrams yet, but that does seem to me an accurate description of bubble-and-clasp, and not too far off in its relation to my result (depending on what exactly "in the image of the embedding" means).