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: deprecated: our papers

Topic: Cornering Optics

Chad Nester (May 03 2022 at 07:03):

@Guillaume Boisseau, @Mario Román and I have put up a preprint on arXiv.

The paper shows how optics (like lenses) in a monoidal category arise as part of the free cornering of that category (the double category obtained by freely adding companion and conjoint structure). This gives us nice string diagrams for optics, and is conceptually simpler than the usual approach via coends. There's also a bit about comb diagrams at the end if that's your thing.

Chad Nester (May 03 2022 at 07:04):

I don't consider myself much of an optics person, but I think it's pretty interesting :)

Matteo Capucci (he/him) (May 03 2022 at 07:40):

Very interesting! I gave it a quick look now and I love the part about combs, it seems indeed quite an handy description

Matteo Capucci (he/him) (May 03 2022 at 07:41):

Are the corner diagrams you draw like those in https://arxiv.org/abs/1612.02762?

Matteo Capucci (he/him) (May 03 2022 at 07:41):

Also, does the free cornering arise in some 'elementary' way?

Chad Nester (May 03 2022 at 07:42):

Yes. We use the main result of that paper to prove our main result!

Matteo Capucci (he/him) (May 03 2022 at 07:42):

Chad Nester said:

Yes. We use the main result of that paper to prove our main result!

Ha, see, I didn't read carefully enough :laughing:

Chad Nester (May 03 2022 at 07:43):

The free cornering is constructed inductively from the monoidal category in question. There are only a few axioms. Is this "elementary"?

Chad Nester (May 03 2022 at 07:44):

I mean, I think it's pretty simple but I don't know what you're looking for.

Matteo Capucci (he/him) (May 03 2022 at 07:45):

I think all this shenanigan has links with MSP preferred definition of optics as 'para and copara kissing' (the pullback definition in our 'Fibre optics' preprint), since para and copara can be represented profitably in the quintet construction applied to a monoidal actegory.

Matteo Capucci (he/him) (May 03 2022 at 07:46):

Chad Nester said:

The free cornering is constructed inductively from the monoidal category in question. There are only a few axioms. Is this "elementary"?

Yeah, that 'elementary' is quite vague/patronizing? Sorry. I meant, is it some 'natural' construction having, say, some universal property? Is it something you can extend to bicategories for instance?

Matteo Capucci (he/him) (May 03 2022 at 07:47):

I don't think I'm conveying this well

Chad Nester (May 03 2022 at 07:50):

I do think it's the single-object bicategory case of the "free proarrow equipment on a bicategory", but haven't checked. Is there a reference for that construction anywhere?

Chad Nester (May 03 2022 at 07:51):

It is certainly an initial object, but this is because it is constructed inductively.

Nathanael Arkor (May 03 2022 at 11:02):

Chad Nester said:

I do think it's the single-object bicategory case of the "free proarrow equipment on a bicategory", but haven't checked. Is there a reference for that construction anywhere?

Not in general, but there are special cases in the literature, such as when the bicategory is locally discrete or has a single object.

John Baez (May 03 2022 at 16:04):

That's cool! I've never gotten into optics but I like double categories, so the concept of the "free cornering" of a category is interesting to me. I've never thought about it before. Is it new? It's something like the free fibrant double category on a category.

John Baez (May 03 2022 at 16:06):

Hmm, I just read more comments here. Are you saying this concept was introduced by David Jaz Myers?

John Baez (May 03 2022 at 16:06):

By the way "fibrant double category" is another name for "proarrow equipment", and there are probably other names for it too... oh yeah, "framed bicategory".

John Baez (May 03 2022 at 16:09):

Somebody should try to work out the free fibrant double category on a general bicategory. That sounds like a useful thing. @Christian Williams might like it for his work on logic.

Chad Nester (May 03 2022 at 17:32):

@John Baez The relevant concept is that of a proarrow equipment (known by many names!). The "free cornering" of a monoidal category is the double category (with one object) that you get by adding companion and conjoint structure to it (that is, by making it into a proarrow equipment). The idea with the name is that you do this by adding corner cells and asking that they satisfy the relevant yanking equations. David Jaz Myers has a paper about these string diagrams, and in particular argues that they are sound in the same way that string diagrams for monoidal categories are. We use that result.

John Baez (May 03 2022 at 17:33):

When I asked if "this concept was introduced by..." I meant the concept of "free cornering of a category", not "proarrow equipment". I should know better by now than to use pronouns. They are so tricky.

Chad Nester (May 03 2022 at 17:34):

Ah okay. I think I get to claim credit for this, from this paper.

Chad Nester (May 03 2022 at 17:36):

Also from last year's ACT my paper on "Situated Transition Systems" uses it (still forthcoming, but on arXiv).

John Baez (May 03 2022 at 17:37):

Okay, cool. Ideally someone someday would show there's something like a forgetful functor from proarrow equipments to categories (or bicategories) and something like a left adjoint to that. Did you do that?

(I say "something like" because one has to choose precisely how to treat this would-be adjunction: using categories, 2-categories, bicategories, etc.)

Nathanael Arkor (May 03 2022 at 17:37):

Chad Nester said:

Ah okay. I think I get to claim credit for this, from this paper.

Presumably there's some overlap with Autonomization of monoidal categories and Freely adjoining monoidal duals?

Chad Nester (May 03 2022 at 17:37):

Nathanael Arkor said:

Chad Nester said:

Ah okay. I think I get to claim credit for this, from this paper.

Presumably there's some overlap with Autonomization of monoidal categories and Freely adjoining monoidal duals?

I don't know. I'll take a look though.

Chad Nester (May 03 2022 at 17:39):

John Baez said:

Okay, cool. Ideally someone someday would show there's something like a forgetful functor from proarrow equipments to categories (or bicategories) and something like a left adjoint to that. Did you do that?

(I say "something like" because one has to choose precisely how to treat this would-be adjunction: using categories, 2-categories, bicategories, etc.)

I haven't done this, no. I do agree that it would be good to do.

Nathanael Arkor (May 03 2022 at 17:40):

In the latter paper, for instance, they describe how to freely adjoin duals to every object of a monoidal category, and show this gives a fully faithful embedding, which proves that it is exactly the free proarrow equipment on a one-object bicategory.

Nathanael Arkor (May 03 2022 at 17:41):

In the former paper, infinite chains of duals are adjoined, rather than just a single right dual, though I think similar ideas are applied.

Chad Nester (May 03 2022 at 17:48):

For the former paper (Autonomization of Monoidal Categories), I guess it's similar in that we also freely add the components necessary to have duals and impose equations on them, but we never end up with an autonomous category in the general case.

Chad Nester (May 03 2022 at 17:52):

I think I'm going to have to spend some time with the latter paper (Freely Adjoining Monoidal Duals), but I'd guess they end up with something like the horizontal cells of the free cornering (in our terminology).

Chad Nester (May 03 2022 at 17:53):

Thanks for that reference!

John Baez (May 03 2022 at 17:58):

Chad Nester said:

I think it's reasonable to use the word "free" anyway, but would be open to a better name.

I'm not opposed to it! It probably is free in the sense of applying some sort of left adjoint process. If you call it free, it'll motivate someone to investigate this.

Chad Nester (May 03 2022 at 17:59):

I deleted that comment because I thought it was too defensive, but great!

Nathaniel Virgo (May 04 2022 at 01:50):

I just read through this thread's paper. It's really nice. (And kudos for using hand-drawn diagrams.)

I'm curious why, in the definition of a free cornering, you don't impose equations like $I^\circ = I^\bullet = I$ or $(A\otimes B)^\circ = B^\circ \otimes A^\circ$ and $(A\otimes B)^\bullet = A^\bullet \otimes B^\bullet$? Plus some equations for the corners like

image.png

and their upside-down versions.

It seems like if you had some equations along those lines then you wouldn't need the definition of $\bullet\circ$-alternating, because every vertical object could be expressed in that form. You'd also have that the diagrams for $(A\otimes B)^\bullet$ and $A^\bullet \otimes B^\bullet$ would be the same (for example), which seems like a nice property to have. Or does this not work / is something like that secretly there already?

Bryce Clarke (May 04 2022 at 06:08):

This is a really cool paper; I read the whole thing when I saw it on the arXiv yesterday!

Bryce Clarke (May 04 2022 at 06:11):

Something I'm wondering is if the fully faithful inclusion of "double categories with companions and conjoints" into just double categories has a left adjoint? Or is the freeness of the corning construction specifically related to monoidal categories?

Tom Hirschowitz (May 04 2022 at 06:51):

Chad Nester said:

Ah okay. I think I get to claim credit for this, from this paper.

Love the slug analogy!

Matteo Capucci (he/him) (May 04 2022 at 07:21):

John Baez said:

By the way "fibrant double category" is another name for "proarrow equipment", and there are probably other names for it too... oh yeah, "framed bicategory".

lmao this is Babel-level terminology hell

Chad Nester (May 04 2022 at 13:13):

Nathaniel Virgo said:

I just read through this thread's paper. It's really nice. (And kudos for using hand-drawn diagrams.)

I'm curious why, in the definition of a free cornering, you don't impose equations like $I^\circ = I^\bullet = I$ or $(A\otimes B)^\circ = B^\circ \otimes A^\circ$ and $(A\otimes B)^\bullet = A^\bullet \otimes B^\bullet$? Plus some equations for the corners like

image.png

and their upside-down versions.

It seems like if you had some equations along those lines then you wouldn't need the definition of $\bullet\circ$-alternating, because every vertical object could be expressed in that form. You'd also have that the diagrams for $(A\otimes B)^\bullet$ and $A^\bullet \otimes B^\bullet$ would be the same (for example), which seems like a nice property to have. Or does this not work / is something like that secretly there already?

Thanks!

What you suggest is certainly possible, although it turns out that the things you want to equate are isomorphic in the category of horizontal cells anyway -- see Lemma 3 here. I think fewer axioms are better, and so since it doesn't really get us anything I prefer not to make the identifications.

Moreover I think the category of horizontal cells is pretty interesting, so I'm hesitant to collapse any of the structure there before I feel like I really understand it (which I do not). Also sometimes it's convenient to be able to talk about $A^\circ \otimes B^\circ$ and $(A \otimes B)^\circ$ separately.

It may well turn out that for certain applications collapsing that structure as you suggest is exactly what you want!

Chad Nester (May 04 2022 at 13:18):

You can indeed make every object alternate in the appropriate way (up to isomorphism) by stricking in copies of $I^\circ$ and $I^\bullet$ though. We haven't really explored this so I don't know if there's anything interesting to say or not.

Chad Nester (May 04 2022 at 13:20):

Bryce Clarke said:

Something I'm wondering is if the fully faithful inclusion of "double categories with companions and conjoints" into just double categories has a left adjoint? Or is the freeness of the corning construction specifically related to monoidal categories?

I'd like to know this too.

Chad Nester (May 04 2022 at 13:21):

Bryce Clarke said:

This is a really cool paper; I read the whole thing when I saw it on the arXiv yesterday!

I think at some point one of my coauthors saw on twitter that you were thinking about double categories and lenses. We figured we should probably write up our results as soon as possible to avoid being scooped! I'm happy you like the paper :)

Chad Nester (May 04 2022 at 13:24):

Matteo Capucci (he/him) said:

John Baez said:

By the way "fibrant double category" is another name for "proarrow equipment", and there are probably other names for it too... oh yeah, "framed bicategory".

lmao this is Babel-level terminology hell

The names I know for this thing are: proarrow equipment, framed bicategory, fibrant double category, companion and conjoint structure, and connection structure.

Chad Nester (May 04 2022 at 13:24):

Since it's not going to make the problem worse than it is, I really think we should call them "cornered double categories", or maybe "double categories with corner structure".

Chad Nester (May 04 2022 at 13:25):

With my favourite existing accepted terminology being the companion and conjoint one.

Nathanael Arkor (May 04 2022 at 13:28):

Bryce Clarke said:

Something I'm wondering is if the fully faithful inclusion of "double categories with companions and conjoints" into just double categories has a left adjoint? Or is the freeness of the corning construction specifically related to monoidal categories?

I'm certain this is true, and if I remember correctly, it's even alluded to in one of the Dawson–Paré–Pronk papers on double categories (though they don't prove it). The idea is that freely adjoining companions and conjoints to a double category should be a "completion" in a sense in which adjoining adjoints to a bicategory is not, despite both giving "free proarrow equipment" constructions, and so this is a particularly nice context in which to consider the construction.

Nathanael Arkor (May 04 2022 at 13:31):

(By "completion", I suspect that the resulting 2-adjunction is lax idempotent, or something like that.)

Mike Shulman (May 04 2022 at 14:58):

I don't see immediately how that could be true. Both adjoints in a bicategory and companions/conjoints in a double category are unique up to unique isomorphism, and preserved by all functors, so I don't know what would be different.

Nathanael Arkor (May 04 2022 at 15:11):

Mike Shulman said:

I don't see immediately how that could be true. Both adjoints in a bicategory and companions/conjoints in a double category are unique up to unique isomorphism, and preserved by all functors, so I don't know what would be different.

I mean in the sense that having all companions and conjoints is a property of a double category, whereas "being a proarrow equipment" is not a property of a bicategory. So one could very well adjoin all companions and conjoints that don't already exist to a double category, whereas one could not do something similar for bicategories: you need the extra structure of an F-category.

Mike Shulman (May 04 2022 at 15:16):

Ah, I thought you were talking about just "adding adjoints to a bicategory" qua bicategory, which is different from making a bicategory into a proarrow equipment.

Mike Shulman (May 04 2022 at 15:22):

Chad Nester said:

The names I know for this thing are: proarrow equipment, framed bicategory, fibrant double category, companion and conjoint structure, and connection structure.

I don't think a connection structure is quite the same; IIRC that just refers to companions, not conjoints. If you have both it would be a "connection and co-connection structure".

The terminology "framed bicategory" is my fault, and I would prefer to deprecate it. Nowadays I generally say "equipment".

Nathanael Arkor (May 04 2022 at 15:22):

Yes, sorry, I should have been a bit more careful in my phrasing: what I meant is the free proarrow equipment construction is given by freely adjoining a right adjoint to each 1-cell of a bicategory, but to even talk about what it means to be a 1-cell in the original bicategory, you need to move to a setting where you can distinguish some of the 1-cells in the bicategory (e.g. F-categories or double categories).

Nathanael Arkor (May 04 2022 at 15:25):

Bryce Clarke said:

Something I'm wondering is if the fully faithful inclusion of "double categories with companions and conjoints" into just double categories has a left adjoint? Or is the freeness of the corning construction specifically related to monoidal categories?

I presume the existence of a left adjoint follows from an AFT, but you really want to know that the construction is locally fully faithful, which is the hard part (and probably requires figuring out exactly what the construction looks like).

Chad Nester (May 04 2022 at 15:28):

Mike Shulman said:

Chad Nester said:

The names I know for this thing are: proarrow equipment, framed bicategory, fibrant double category, companion and conjoint structure, and connection structure.

I don't think a connection structure is quite the same; IIRC that just refers to companions, not conjoints. If you have both it would be a "connection and co-connection structure".

Hmm, okay. Thanks.

John Baez (May 04 2022 at 15:59):

Chad Nester said:

Since it's not going to make the problem worse than it is, I really think we should call them "cornered double categories", or maybe "double categories with corner structure".

Yes: the solution to a concept having too many names is always to introduce another name.

Martti Karvonen (May 04 2022 at 16:36):

Relevant xkcd