Category Theory
Zulip Server
Archive

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.


Stream: learning: questions

Topic: products and coproducts with string diagrams


view this post on Zulip Bernd Losert (Jan 27 2023 at 19:02):

How do you draw products and coproducts with string diagrams? Is there a good reference that I can consult?

view this post on Zulip Jules Hedges (Jan 27 2023 at 19:16):

A common thing is to use the fact (attributed to Fox) that a monoidal product is cartesian iff every object is a commutative comonoid + all morphisms are comonoid homomorphisms, and dually a monoidal product is cocartesian iff every object is a commutative monoid + all morphisms are monoid homomorphisms. (There's a tiny bit more to it than that, but that's close enough.) That's a very easy way to get string diagrams, it's written in Selinger's "survey of graphical languages for monoidal categories"

view this post on Zulip Bernd Losert (Jan 28 2023 at 11:35):

Thanks. Hopefully that paper has an example of what I'm looking for.

view this post on Zulip Antonin Delpeuch (Jan 28 2023 at 20:20):

If you want to draw both products and coproducts in the same string diagram, it is likely you need string diagrams for a [[rig category]] (or more precisely a [[distributive category]])… We made "sheet diagrams" for that: https://arxiv.org/abs/2010.13361

view this post on Zulip Ralph Sarkis (Jan 28 2023 at 22:14):

Also, see tape diagrams.

view this post on Zulip Cole Comfort (Jan 30 2023 at 18:27):

Ralph Sarkis said:

Also, see tape diagrams.

I would argue that these two things are actually the same, just using two depictions of the projection of the same three dimensional structure, where in the case of tape diagrams, the degeneracies at the branching are not drawn.

view this post on Zulip Cole Comfort (Jan 30 2023 at 18:28):

The rules in the tape diagrams paper express the same isotopy that is described in our paper. Again, minus the degeneracies at the branching points, which one should be careful about so as not to make moves which disrespect the isotopy

view this post on Zulip Cole Comfort (Jan 30 2023 at 18:32):

It seems that there is some confusion about our paper on sheet diagrams, because the normalization procedure which we describe is is used to prove completeness, but not every diagram has to be normalized when using it. The normalization rules correspond to moves respecting a certain isotopy, so they can of course be inverted; all that you need to know is that such a normal form actually exists.

view this post on Zulip Cole Comfort (Jan 30 2023 at 18:42):

Of course in the tape diagrams paper they do much more things than prove completeness, and it is actually for a more specific kind of bimonoidal category. But aside from that they are the same axioms as far as I can tell.

view this post on Zulip Cole Comfort (Jan 30 2023 at 18:52):

It is analagous to how in a a logic, you can eliminate cut, but you don't have to do it, you just have to be able to. And in multiplicative linear logic this cut elimination corresponds to the normalization of proof nets in some sense, to wrap it back around to string diagrams.

view this post on Zulip Antonin Delpeuch (Jan 31 2023 at 15:13):

@Cole Comfort are you saying that the requirements to have biproducts to make tape diagrams is not actually essential, and that the syntax could be generalized for arbitrary rig categories? I haven't dived in the paper enough to really be able to tell ^^

view this post on Zulip Cole Comfort (Jan 31 2023 at 15:18):

Antonin Delpeuch said:

Cole Comfort are you saying that the requirements to have biproducts to make tape diagrams is not actually essential, and that the syntax could be generalized for arbitrary rig categories? I haven't dived in the paper enough to really be able to tell ^^

I believe that the extra axioms for biproducts and duals are independent from the rig category axioms. For example, the adjoints and diagonal maps don't exist in general, but if you drop them, then you seem to get exactly the same thing as sheet diagrams.

view this post on Zulip Cole Comfort (Jan 31 2023 at 15:19):

Also, just because this is the case doesn't mean that the proof strategies of either paper could easily be refined/generalized to prove completeness in the more refined/generalized case.