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.
How do you draw products and coproducts with string diagrams? Is there a good reference that I can consult?
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"
Thanks. Hopefully that paper has an example of what I'm looking for.
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
Also, see tape diagrams.
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.
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
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.
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.
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.
@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 ^^
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.
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.