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: parallel dimensions


view this post on Zulip Sam Tenka (Apr 06 2020 at 22:15):

String diagrams are great! For example, they are really helpful when doing tensor computations in linear algebra. One often uses one of the page's dimensions to denote arrow composition and another to denote tensor (in other words, one often works with Vect equipped with tensor as its the monoidal operation). But there are times when direct sum is useful, too. Are there standard notations for working with two monoidal operations at once? This is not a math question so much as a psychological question about eyeball ergonomics.

view this post on Zulip John Baez (Apr 06 2020 at 22:18):

Many people have struggled with this, but basically they all give up.

view this post on Zulip Jules Hedges (Apr 06 2020 at 22:30):

Wait, really? Me and @Antonin Delpeuch are working on this recently. It's not quite straightforward but it doesn't seem that difficult. I can't describe the surface diagrams in words though

view this post on Zulip Jules Hedges (Apr 06 2020 at 22:31):

Certainly I've been informally using surface diagrams for 2 interacting monoidal products in game theory, on the assumption that probably nothing will go wrong

view this post on Zulip Jules Hedges (Apr 06 2020 at 22:32):

(I'll come back to this tomorrow, going to sleep now)

view this post on Zulip Nathanael Arkor (Apr 06 2020 at 22:33):

there's a recent StackExchange question on this topic: https://math.stackexchange.com/questions/3583052/string-diagrams-when-you-have-two-monoidal-products

view this post on Zulip Fabrizio Genovese (Apr 06 2020 at 22:36):

This is an ongoing topic of research. I think the last people looking into it atm are @Jules Hedges and @Antonin Delpeuch

view this post on Zulip Fabrizio Genovese (Apr 06 2020 at 22:37):

In general there are also different flavors of this depending on how the monoidal structure interact, e.g. if they distribute over each other

view this post on Zulip Fabrizio Genovese (Apr 06 2020 at 22:38):

but the general agreement is that a graphical calculus should be some flavour of surface diagrams. What is really hard to pind down is what kind of topological moves are allowed or not, e.g. can surfaces cross each other?

view this post on Zulip John Baez (Apr 06 2020 at 22:39):

Jules Hedges said:

Wait, really? Me and Antonin Delpeuch are working on this recently. It's not quite straightforward but it doesn't seem that difficult. I can't describe the surface diagrams in words though

I don't think it's difficult in principle; it's just enough of a pain in the butt to draw and read these diagrams that they never seem to catch on as a practical tool. For example, in quantum mechanics we have \otimes and \oplus, but you don't see many (any?) people using string or surface diagrams involving both these monoidal structures.

view this post on Zulip Jules Hedges (Apr 06 2020 at 22:44):

Top secret spoiler alert: Antonin has made a web tool for typesetting these kind of surface diagrams in Javascript. It looks pretty good, he's not ready to announce it yet though

view this post on Zulip Fabrizio Genovese (Apr 06 2020 at 23:29):

Well, at least wrt the stuff we were doing in Ox tho ⊕ had a marginal role wrt tensor, which was basically the only parallel operation we were interested in

view this post on Zulip Fabrizio Genovese (Apr 06 2020 at 23:31):

Also, there were people like Jamie Vicary using surface diagrams with applications in quantum logic, if I'm not wrong

view this post on Zulip John Baez (Apr 07 2020 at 01:58):

Yes, Jamie and @Mike Stay used some surface diagrams in quantum theory and cryptography... not for \otimes and \oplus though.

view this post on Zulip Jules Hedges (Apr 07 2020 at 09:31):

Here's one I made earlier. This is a picture of a game (as in game theory), specifically the market entry game. Here the usual sequential and parallel dimensions are actual temporally sequential and parallel composition. The parallel sheets are indeed parallel universes, in the sense that in any given play of the game only one of them "runs". The monoidal product corresponding to that I call "external choice", terminology I took from game semantics
(https://categorytheory.zulipchat.com/user_uploads/21317/cDtZvobjgPu84Hl06cLA70c-/EHKBjrnXYAEfqLb.jpg)

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 13:41):

Don't you need to tear the paper sometimes? I'm imagining writing something like
image.png

both sides to be interpreted as something like A(C+D) = AC + AD

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:43):

I think this is one of the design choices! In the approach me and Antonin are taking we don't allow the left hand diagram, which means we're using a sort of normal form representation where we always fully distribute the 2 monoidal structures. That causes some different headaches, but simplifies the topology

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:44):

The specific headache that our approach causes is that \otimes is no longer simply disjoint union of diagrams - you need to do a whole rewriting step

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:46):

Jules Hedges said:

The specific headache that our approach causes is that \otimes is no longer simply disjoint union of diagrams - you need to do a whole rewriting step

OMG T_T

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 13:47):

Or I guess (just idle doodling) the left-hand diagram should actually look like this. Then if you take a vertical cross section it also looks like a string diagram - it seems more like it would have a sensible interpretation that way.

image.png

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:47):

Yes

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:48):

Now you're making me question whether our decision was the right one.....

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:49):

Nathaniel Virgo said:

Or I guess (just idle doodling) the left-hand diagram should actually look like this. Then if you take a vertical cross section it also looks like a string diagram - it seems more like it would have a sensible interpretation that way.

image.png

Yes, this seems right to me as well

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:49):

When you draw it like that, it's easy to see that it's isotopic to the other representation: move the AA wire down to the seam where it becomes critical, then it splits into 2 wires

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:50):

Jules Hedges said:

When you draw it like that, it's easy to see that it's isotopic to the other representation: move the AA wire down to the seam where it becomes critical, then it splits into 2 wires

That's interesting, intuitively I'd have said that you can choose if the wire has to slid on one branch or on the other

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:51):

This comes from the specific type of distributivity you have, I guess. Probably you get your thing from a linearly distributive category

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:52):

Yes, my category is way more well behaved because it's freely generated

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:52):

Read parallel sheets as "or". If you have an A and either a B or a C, then you either have an A and a B, or you have an A and a C

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:52):

so we just allow all the possible branchings

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:53):

Jules Hedges said:

Read parallel sheets as "or". If you have an A and either a B or a C, then you either have an A and a B, or you have an A and a C

Yes, clearly it works with this interpretaton, but I really don't like what happens at the graphical level then

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:53):

You shouldn't have this kind of discontiuities if the graphical calculus is right. Are you sure 3 dimensions are enough?

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:54):

3 dimensions is all that the gods gave us to work with in our universe, have to make the best of them

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:54):

What I mean is

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:55):

maybe this stuff really lives in somethig bigger, you are dealing with a projection, and that's where the weird stuff comes from

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:57):

Me and Antonin are working with distributive monoidal categories, where one of the monoidal structures is cocartesian. So it's just like string diagrams for a cocartesian monoidal category, where you can merge 2 wires and you can push any generating morphism across the critical point, which moves between 1 copy and 2 copies

view this post on Zulip Jules Hedges (Apr 07 2020 at 13:58):

Same thing but 1 dimension higher. (I think that there's some justification going on that makes that formal, that this is just something in the category of something, but we didn't figure that out yet)

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:59):

I see what you are doing now. then the diagram above is a bit misleading tho. You want the border between A and D + C to be explicitly drawn, I guess

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 13:59):

That border really is a morphism, no?

view this post on Zulip Jules Hedges (Apr 07 2020 at 14:04):

Yes. It's a "special" morphism in the same sense as a monoid. I think it's unambiguous to just represent it as a border, same as a monoid is unambiguous with 2 joining wires

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 14:05):

Yes, that is correct. Also this means that you diagrams are read bottom up and that surfaces can be forked downwards and not upwards, right?

view this post on Zulip Jules Hedges (Apr 07 2020 at 14:06):

Ah yes, we now have twice as many dimensions to have flame wars about

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 14:07):

xD

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 14:27):

One context where this makes sense to me: let's say we're in Cat, and we have functors F:CD×EF:C\to D\times E and G:D×ECG:D\times E \to C, and we also have a natural transformation η:idCF;G\eta:\mathrm{id}_C\Rightarrow F;G. Then we might draw it as image.png

One can imagine this getting a lot more complicated if you have lots of functors between lots of Cartesian product categories, and lots of natural transformations between them.

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 14:29):

(more on string diagrams for Cat: https://arxiv.org/pdf/1401.7220.pdf)

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 14:29):

Wait, isn't the type of G:CD×EG: C \to D \times E as well?

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 14:30):

Sorry, it should have been D×ECD\times E \to C

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 14:30):

I'm reading the diagram left to right and top to bottom

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 14:30):

Oh, you are reading bottom up, yes

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 14:31):

Yes, in this situation it makes sense indeed, but in the setting above you'd probably draw this as a box

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 14:31):

If a boundary denotes a structural morphism, then you can only splt in one way, since coproducts have a diagonal monoid but not a diagonal comonoid

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 14:32):

In the general setting of surface diagrams this -- and many other weird things such as the ones you can do with homotopy.io -- make sense, yes

view this post on Zulip Jules Hedges (Apr 07 2020 at 14:36):

@Nathaniel Virgo Did you really pick all this up since my lectures in January? That's amazingly fast...

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 14:36):

@Jules Hedges yep :)

view this post on Zulip Jules Hedges (Apr 07 2020 at 14:37):

Nice... I've been slowly picking this up for years...

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 14:37):

@Fabrizio Genovese I'm not sure what you mean exactly (I am pretty new to this and mostly just playing around) but the right-hand boundary of my surface diagram is a string diagram image.png

you need the extra dimension to express the natural transformation

view this post on Zulip Jules Hedges (Apr 07 2020 at 14:44):

While I'm thinking about it, let me invite @Antonin Delpeuch to this stream and also poke @Cole Comfort

view this post on Zulip Simon Burton (Apr 07 2020 at 14:49):

This is from Reutter, David J., and Jamie Vicary. "Shaded tangles for the design and verification of quantum circuits." Monoidal.png
They bring in the direct sum via the 2cells. Not sure if this is at all related to what the original question was...
https://royalsocietypublishing.org/doi/full/10.1098/rspa.2018.0338

view this post on Zulip Jules Hedges (Apr 07 2020 at 14:55):

A meta-problem I believe we have is that most of the literature on surface diagrams is brain-meltingly difficult. I think there's a gap in the market for a "user's guide to surface diagrams"

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 14:55):

+1!

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 14:56):

One question for this thread is, how does Cat with its product relate to (for example) Vect with tensor product and direct sum as two monoidal products, as in Sam's question? That might tell us how surface diagrams for Vect-with-two-monoidal-operators "should" look.

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 15:02):

On the topic of gaps in the market, I'd really like to see an introduction to category theory that uses graphical reasoning from the start, e.g. for functors and natural transformations, not just for monoidal categories. It seems like it's massively underutilised as a way of making the basics easy to grasp.

view this post on Zulip Simon Burton (Apr 07 2020 at 15:13):

There's "Category Theory Using String Diagrams" by Dan Marsden. I think it's good, but I got totally lost at section 5.1 where he starts using boxes to notate (the action of) functors.

view this post on Zulip Amar Hadzihasanovic (Apr 07 2020 at 15:22):

Nathaniel Virgo said:

On the topic of gaps in the market, I'd really like to see an introduction to category theory that uses graphical reasoning from the start, e.g. for functors and natural transformations, not just for monoidal categories. It seems like it's massively underutilised as a way of making the basics easy to grasp.

Last year I tried teaching a course doing exactly that, which forced me to do lots of nonconventional choices (eg introduce an “elementary” definition of bicategories very early on). Here's the lecture notes.

view this post on Zulip Amar Hadzihasanovic (Apr 07 2020 at 15:24):

This is still all done maths-style with rigorous definitions. I guess one could try to introduce the graphical calculus “informally” by example, instead.

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 15:25):

Wow, great, I will definitely check these out!

view this post on Zulip Amar Hadzihasanovic (Apr 07 2020 at 15:25):

Anyway I would like one day to expand this into a more comprehensive book!

view this post on Zulip Jules Hedges (Apr 07 2020 at 15:36):

Cool!!

view this post on Zulip Antonin Delpeuch (Apr 07 2020 at 15:39):

Nice! (I hope the book will be open access!)

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 15:44):

Nathaniel Virgo said:

Fabrizio Genovese I'm not sure what you mean exactly (I am pretty new to this and mostly just playing around) but the right-hand boundary of my surface diagram is a string diagram image.png

you need the extra dimension to express the natural transformation

What I mean is this: In 1-dimensional string diagrams you have morphisms drawn as boxes. everything that is not a box is a structural morphism, e.g. an identity (wire), a symmetry (swap), etc

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 15:45):

If you have more structure, e.g. your product is cartesian, then you also have a diagonal in the structure, that is, a comonoid, which you still want to denote with some special notation

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 15:46):

In the example about bimonoidal categories we split surfaces top -> bottom. This actually denotes the application of the structural morphism corresponding to the coproduct monoid

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 15:46):

As you do with structural morphisms in other graphical settings, you don't draw anything specific. You just draw a boundary and merge the surfaces bottom top and it's implied you are applying the coproduct monoid there

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 15:48):

But you cannot do the opposite, because the coproduct monoidal structure does not come together a comonoid. So if you split in the other direction (bottom to top) you have to actually decorate the boundary with something saying what this split amounts to

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 15:49):

actually I don't think you can do it at all in the bimonoidal case, but maybe I'm mistaken

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 16:05):

Oh I see. But this is just a question of graphical style, isn't it? If we're doing normal string diagrams we draw boxes around the morphisms because they're convenient to write labels on, but conceptually we can still think of them as points if we want to. Once we extend those points into lines it gets harder to draw boxes around them, so I just wrote "F" and "G" next to the lines instead. (This is exactly the style Marsden uses in 2D, I just replaced a line connecting two 2d regions with a line connecting three regions.)

In the bimonoidal example I drew I guess we can interpret the dashed line as the structural morphism, so maybe that's a reasonable convention to adopt: dashed line means coproduct monoid, solid lines mean other morphisms.

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 16:09):

(But I'm kind of unsure - I'm not really familiar with the definitions for bimonoidal categories and I'm really just drawing pictures here. It seems like Cat + cartesian product should be quite similar to a bimonoidal category to me, though.)

view this post on Zulip Jules Hedges (Apr 07 2020 at 16:10):

I get your intuition, also can't figured out where it comes from. Cat\mathbf{Cat} in this guise is a monoidal bicategory, I wonder whether monoidal bicategories are like bimonoidal categories?

view this post on Zulip Antonin Delpeuch (Apr 07 2020 at 16:16):

I feel like it is not possible to make sense of an arbitrary composition of such structural morphisms to interpret it as an object in a free bimonoidal category. For me that is where this syntax fails. If you only represent straight sheets (so, objects normalized as sums of products), you avoid this problem.

view this post on Zulip Fabrizio Genovese (Apr 07 2020 at 16:19):

Nathaniel Virgo said:

Oh I see. But this is just a question of graphical style, isn't it? If we're doing normal string diagrams we draw boxes around the morphisms because they're convenient to write labels on, but conceptually we can still think of them as points if we want to. Once we extend those points into lines it gets harder to draw boxes around them, so I just wrote "F" and "G" next to the lines instead. (This is exactly the style Marsden uses in 2D, I just replaced a line connecting two 2d regions with a line connecting three regions.)

In the bimonoidal example I drew I guess we can interpret the dashed line as the structural morphism, so maybe that's a reasonable convention to adopt: dashed line means coproduct monoid, solid lines mean other morphisms.

Yes, it is just a matter of style indeed. In this case we may say that an undecorated boundary is structural. Still I feel I'd make a lot of confusion that way :frown:

view this post on Zulip Joe Moeller (Apr 07 2020 at 16:33):

I was recently wondering if you could develop some calculational set of rules for using ordinary 2d string diagrams when you have two monoidal structures AND you know some relationship between them, eg distribution. Then could you record some data about the "inactive" monoidal structure in labels on the strings, then apply the distributions rules somehow that switches which monoidal structure is "active".

view this post on Zulip Joe Moeller (Apr 07 2020 at 16:34):

If it works out nicely, I could imagine doing calculations where you switch back and forth a few times depending on what the next step in the calculation requires.

view this post on Zulip Sam Tenka (Apr 07 2020 at 16:34):

Joe Moeller said:

I was recently wondering if you could develop some calculational set of rules for using ordinary 2d string diagrams when you have two monoidal structures AND you know some relationship between them, eg distribution. Then could you record some data about the "inactive" monoidal structure in labels on the strings, then apply the distributions rules somehow that switches which monoidal structure is "active".

Cool! This reminds me of https://arxiv.org/abs/1706.00526 (page 44), by @Evan Patterson

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 17:10):

Jules Hedges said:

I get your intuition, also can't figured out where it comes from. Cat\mathbf{Cat} in this guise is a monoidal bicategory, I wonder whether monoidal bicategories are like bimonoidal categories?

Maybe it works like this:

A monoidal category is basically a bicategory with only one object. The objects of the monoidal category are the 1-cells of the bicategory, and the 2-cells become the morphisms. That’s why the string diagrams for a monoidal category look like monochrome versions of the ones for a bicategory - there's only one object, so the regions between the wires are all the same colour.

In the same sense, is a bimonoidal category a monoidal bicategory with only one object?

view this post on Zulip John Baez (Apr 07 2020 at 17:30):

A monoidal bicategory with one object is usually called a "braided monoidal category". But you can think of a braided monoidal category as having two monoidal structures, a vertical and a horizontal one, related by an interchange law.

One beautiful way to see these two monoidal structures is to use this fact: a braided monoidal category is a monoidal category in the 2-category of monoidal categories - just like a commutative monoid is a monoid in the category of monoids. I think this was proved by Joyal and Street in their paper "Braided tensor categories".

view this post on Zulip Nathaniel Virgo (Apr 07 2020 at 21:18):

Oh of course, one object means A×AA\times A is the same as AA, so the extra dimension goes away. So that's not the right analogy, but it still feels like surface diagrams for bimonoidal categories should be like monochrome versions of diagrams for monoidal bicategories. I'll have to think about it some more.

(Or rather the distinct sheets go away but the extra dimension stays relevant for the strings - it'd be interesting to understand that properly one day.)

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 14:35):

Continuing this thought process, I think I have a fairly straightforward way to make diagrams for bimonoidal categories, which I think should work. This is all informal still, but maybe concrete enough to be potentially useful.

The trick is to notice that my Cat diagram can be seen as a smooth transformation from a string diagram on the left to another string diagram on the right, with just a 'local' discontinuity at the natural transformation.
image.png

So my idea is that to make nice sheet diagrams for a bimonoidal category, we need to make nice string-like diagrams for the objects. Then we make the sheet diagram by adding an extra dimension, where the morphisms appear as local discontinuities.

view this post on Zulip Oscar Cunningham (Apr 08 2020 at 14:37):

Do we know how to solve the decategorified problem of making diagrams for rings?

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 14:37):

For a general category with two monoidal operations, it seems like a reasonable way to do this would be to draw the objects as points on wires, with one monoidal operation being sequential composition (putting two dots next to each other on the same wire) and the other being parallel composition (putting two wires next to each other)

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 14:39):

E.g. if we happen to have in our category that (AB)C(AC)(BC)(A\oplus B)\otimes C \cong (A\otimes C)\oplus(B\otimes C), then we might write it like this

image.png

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 14:40):

To make that into a surface diagram we just make a smooth transition from one of those to the other, adding a discontinuity to represent the isomorphism where it's needed. (I've drawn the diagram top-down to avoid any need for mental rotation)

image.png

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 14:42):

My idea is that any morphism should be representable like this, either as a point on a wire, or at a junction between wires, which may or may not also be a junction between sheets.

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 14:42):

@Oscar Cunningham I don't know - does what I described above do that, or is there a problem with it that I've missed?

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 14:45):

Of course we have to choose which monoidal operation is parallel and which is sequential composition. If we did it the other way round, the above diagrams would look like this (but I think this way is a bit more awkward.) image.png

(The dotted line is just to help the eye - the 'C' wire splits in two at the same point where the tube bifurcates into two legs.)

view this post on Zulip Oscar Cunningham (Apr 08 2020 at 14:47):

I think that would work for rings too

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 15:11):

Note that if we're in, e.g., Vect, we can still do things like "bending the wires around" to represent unit and counit. If we chose tensor product as sequential composition then this corresponds to bending a wire around while staying in the same sheet, but if the tensor product is parallel composition then it corresponds to bending the whole sheet around. Does anyone have an example of something interesting to draw that involves both products?

view this post on Zulip Joe Moeller (Apr 08 2020 at 15:35):

I think in the pictures above you don't have room for composition anymore. The problem is really representing three operations in a 2d diagram.

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 15:46):

Here's a morphism f:ABCDf:A\oplus B \to C\otimes D being composed with idC(g:DEF)\mathrm{id}_C\otimes (g:D\to E\oplus F). image.png

The idea is to use one dimension each for \otimes (left-right), \oplus (front-back) and composition (up-down).

view this post on Zulip Joe Moeller (Apr 08 2020 at 16:05):

Sorry, I hadn't seen that yet. Yes, moving up to 3d seems necessary.

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 16:10):

It seems kind of a cool principle to me actually - the process to get from string diagrams to these 3D sheet diagrams is the same as the process to get from one-dimensional equations to string diagrams. It would totally make sense to consider morphisms between these diagrams, if only we could draw or perceive the 4D diagrams that would result. (Well we could animate them. But 5D is right out.)

view this post on Zulip Joe Moeller (Apr 08 2020 at 16:16):

It is incredibly natural, but it's also impractical. There's a discussion going on in #learning: show and tell about how hard it is to create surface diagrams, as I'm sure you know. And as you point out, going higher is simply not feasible.

view this post on Zulip Nathaniel Virgo (Apr 08 2020 at 16:46):

I don't think the lack of practicality is a show-stopping issue for me at this point.

view this post on Zulip Sam Tenka (Apr 09 2020 at 16:42):

Nathaniel Virgo said:

To make that into a surface diagram we just make a smooth transition from one of those to the other, adding a discontinuity to represent the isomorphism where it's needed. (I've drawn the diagram top-down to avoid any need for mental rotation)

image.png

This is so beautiful.

view this post on Zulip Cole Comfort (May 04 2020 at 16:20):

Sorry to necro the thread, but I think if you use 3d diagrams (full proof surfaces), instead of 2.5d (proof sheets) to represent morphisms in a bimonoidal category, then I think you run into some problems, unless the 3rd dimension is properly constrained. If we are allowed to tear sheets apart like in https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-basic.20questions/topic/parallel.20dimensions/near/193188862 , then things go horribly wrong.