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: Para construction and symmetric monoidal categories


view this post on Zulip Nathaniel Virgo (Nov 25 2023 at 08:15):

Suppose I have a monoidal category M\mathcal{M} acting on a category C\mathcal{C}. Then I can apply the Para construction, as described in Towards Foundations of Categorical Cybernetics. This gives me a bicategory Para(C)\mathbf{Para}(\mathcal{C}) where the objects are obejcts of C\mathcal{C}, 1-cells are morphisms of C\mathcal{C} parametrised by objects of M\mathcal{M}, and 2-cells are re-parametrisations. (It can also be made into a double category.)

Now suppose that M\mathcal{M} is a symmetric monoidal category. (But C\mathcal{C} is still just a category.) It seems like the symmetry of M\mathcal{M} ought to impose some extra structure on Para(C)\mathbf{Para}(\mathcal{C}), because a morphism parametrised by MNM\otimes N is canonically isomorphic to one parametrised by NMN\otimes M.

But if someone gives me a morphism in Para(C)\mathbf{Para}(\mathcal{C}) I don't seem to have any way to 'know' that it's parametrised by MNM\otimes N in order to apply the swap to it. So it's not obvious how to express this purely in terms of the bicategory Para(C)\mathbf{Para}(\mathcal{C}), but it seems like there should be a way. Does anyone know how to do it?

view this post on Zulip John Baez (Nov 25 2023 at 10:56):

This reminds of a related issue: on the nLab article it says:

Again, it is folklore that this bicategory is symmetric monoidal when ⊙ is a symmetric monoidal action, meaning 𝒞 is monoidal, ℳ is symmetric and ⊙ is a symmetric monoidal functor.

"This bicategory" is, I believe, exactly the one you're talking about and calling Para(C)\mathbf{Para}(\mathcal{C}). (The nLab calls it Para()\mathbf{Para}(\odot).)

view this post on Zulip John Baez (Nov 25 2023 at 11:01):

I had thought the only problem was nobody has yet had the energy to write down a proof that the necessary coherence laws hold, to show that this bicategory is symmetric monoidal under these assumptions.

I'd been wanting to pressure someone to do it, or maybe do it myself. I would try constructing a symmetric monoidal double category first, and extracting a symmetric monoidal bicategory from that using @Mike Shulman's machinery.

view this post on Zulip John Baez (Nov 25 2023 at 11:05):

But you seem to be saying there's some "in principle" reason it's hard:

view this post on Zulip John Baez (Nov 25 2023 at 11:05):

Nathaniel Virgo said:

But if someone gives me a morphism in Para(C)\mathbf{Para}(\mathcal{C}) I don't seem to have any way to 'know' that it's parametrised by MNM\otimes N in order to apply the swap to it. So it's not obvious how to express this purely in terms of the bicategory Para(C)\mathbf{Para}(\mathcal{C}), but it seems like there should be a way. Does anyone know how to do it?

view this post on Zulip John Baez (Nov 25 2023 at 11:11):

It's true that an individual morphism in Para(C)\mathbf{Para}(\mathcal{C}) is parametrized by some object and this object can't 'know' that it's the tensor product MNM \otimes N of two other objects. But when you're constructing the symmetry for a monoidal category (or bicategory, or double category) you don't just have a single morphism that you're trying to 'swap': you have two! So here you start with a morphism parametrized by MM and one parametrized by NN; you have those objects in hand, and you can form their tensor product and the swap SM,N:MNNMS_{M,N} : M \otimes N \to N \otimes M.

view this post on Zulip Nathaniel Virgo (Nov 25 2023 at 11:18):

(I guess it should be called Para()\mathbf{Para}(\odot) really. The paper I linked calls it Para(C)\mathbf{Para}_\bullet(\mathcal{C}) -- I was just being lazy in not giving a name to the action.)

I was wondering if we can say when M\mathcal{M} is symmetric monoidal but we don't assume a monoidal structure on C\mathcal{C}.

The thing nlab says definitely seems related, and I can see why it ought to be true (at least if we also assume C\mathcal{C} is symmetric monoidal - I don't know what a symmetric monoidal functor is otherwise). Without the monoidal structure on C\mathcal{C} I think we won't end up with a symmetric monoidal bicategory but maybe there is still something we can say.

view this post on Zulip Dylan Braithwaite (Nov 25 2023 at 11:23):

One way to keep track of the parameterising objects in Para is to instead view it as a [[locally graded category]] . But maybe this is a bit of a blunt approach and there's some way to characterise the 2-cells arising from symmetries with some kind of universal property.

I think a way to get your hands on the parameterising object would be to ask if a morphism factors through some universal morphism CMCC \to M \bullet C (which would just be the identity on MCM \bullet C in the underlying category)

view this post on Zulip John Baez (Nov 25 2023 at 12:23):

Nathaniel Virgo said:

(I guess it should be called Para()\mathbf{Para}(\odot) really. The paper I linked calls it Para(C)\mathbf{Para}_\bullet(\mathcal{C}) -- I was just being lazy in not giving a name to the action.)

I was wondering what we can say when M\mathcal{M} is symmetric monoidal but we don't assume a monoidal structure on C\mathcal{C}.

Oh. I would never try that unless I had an example to guide me - in other words, some reason to feel sure it should work.

view this post on Zulip Nathaniel Virgo (Nov 25 2023 at 13:08):

It might be that I have an "XY problem" here, I'm not sure. What I really want to do is to say that an endomorphism in Para()\mathbf{Para}(\odot) is "independent of the order of its parameters". By independent of the order of paramters I mean that the swap (in C\mathcal{C}) forms an isomorphism (in Para()\mathbf{Para}(\odot)) f;ff;ff;f\cong f;f. If we're just working in a monoidal category rather than an actegory it means that

image.png

That's fine, but it's a bit weird, because the swap isn't special in Para()\mathbf{Para}(\odot) - it happens to be the swap in C\mathcal{C}, but in Para()\mathbf{Para}(\odot) it's just a 2-cell without any obvious (to me) defining property. So I was trying to figure out if there's a way to pick out the swap given only the data of Para()\mathbf{Para}(\odot), or at least to get a more principled understanding of what role the swap from C\mathcal{C} plays in Para()\mathbf{Para}(\odot). Maybe it's a weird thing to try and do, I don't know.

view this post on Zulip Philip Saville (Nov 25 2023 at 18:30):

I'm not sure how enlightening it is, but I can confirm that -- at least when you're looking at the Para construction of a symmetric monoidal category C\mathbb{C} on itself -- the swap in C\mathbb{C} does determine the swap of a symmetric monoidal bicategory structure on Para(C)\mathrm{Para}(\mathbb{C}). Every isomorphism in C\mathbb{C} lifts to an equivalence in Para(C)\mathrm{Para} (\mathbb{C}) with parameter given by the unit, and every strong natural transformation lifts to a pseudonatural transformation. The braiding for the symmetric structure is then the lifting of the braiding through these two constructions -- Hugo Paquet and I sketched this here but ran out of time to write up the details in full. (The proof is not as difficult as it looks at first sight, because coherence of monoidal categories gives you the axioms for free.) I'm pretty sure all this falls out of Mike Shulman's double categorical framework too, though I never got round to checking for sure.

I am interested in knowing if there's a nicer / more universal way of saying parameters can be reordered, though, because for graded monads it would say something like "the effects can be combined in either order", which is neat.

view this post on Zulip Dylan Braithwaite (Nov 25 2023 at 19:57):

You can view a monoidal action ()(\bullet) as a pseudofunctor from the delooping of a monoidal category to Cat\mathbf{Cat}. Then Para()\mathbf{Para}(\bullet) can be seen as the "2-grothendieck construction" of this indexed category.

I bet you could work out a version of the monoidal Grothendieck construction for 2-indexed symmetric monoidal categories such that pseudofunctors ():BMSymMonCat(\bullet) : \mathbb B \mathcal M \to \mathbf{SymMonCat} give rise to Para()\mathbf{Para}(\bullet) as a symmetric monoidal bicategory.

view this post on Zulip John Baez (Nov 25 2023 at 21:04):

That's a nice way to think about what's going on here, Dylan. Thanks!

Hey, @Joe Moeller - here's something cool for you to do!

view this post on Zulip John Baez (Nov 25 2023 at 21:06):

I think it would be technically (and also conceptually) helpful to get double categories into the game. Does someone have a double category version of the Grothendieck construction worked out yet?

view this post on Zulip Mike Shulman (Nov 25 2023 at 21:13):

I think there's a double-categorical Grothendieck construction in https://arxiv.org/abs/2205.15240.

view this post on Zulip Jean-Baptiste Vienney (Nov 25 2023 at 21:29):

You also have these slides by Dorette Pronk on the matters in this paper:
Double Grothendieck: double fibrations and double colimits: Part one, Part two

view this post on Zulip Morgan Rogers (he/him) (Nov 25 2023 at 23:40):

I should ping @Nicolas Blanco regarding Grothendieck constructions for double categories

view this post on Zulip Nathaniel Virgo (Nov 26 2023 at 01:10):

I think there's a weaker version of the statement on nlab, where you can end up with a monoidal structure on Para()\mathbf{Para}(\odot) that is not symmetric. To get this you need something stronger than a monoidal action but weaker than a symmetric monoidal action.

(This is pretty tangential to my original question, which I'm still interested in, but I'm interested in this as well.)

To see why that should be true I'll describe a graphical calculus for actegories, which I think is folklore. It's helpful for intuition, though I guess somebody still has to do all the coherence proofs to show it works.

At first let's not assume a monoidal structure on C\mathcal{C}. So a string diagram in C\mathcal{C} will always be one-dimensional, with exactly one wire coming in and out of each morphism. But M\mathcal{M} is monoidal, so a string diagram in M\mathcal{M} looks like a string diagram in any monoidal category.

Then, for example, for A,B,CMA,B,C\in \mathcal{M} and XCX\in \mathcal{C}, let's draw ABCXA\otimes B\otimes C \odot X as

image.png

which is an object in C\mathcal{C}. The laws for an action say that it doesn't matter how you parenthesise this expression, and it also doesn't matter whether you interpret the diagram as ABCA\otimes B\otimes C acting on XX or ABA\otimes B acting on CXC\odot X etc. So this diagram is unambiguous up to canonical isomorphisms.

Then since the action is functorial and all the structure maps are natural we can draw boxes on these wires as well, and slide them past each other in the same way as for a monoidal category.

Then the Para construction looks the same as it does for monoidal categories - a 1-cell in Para()\mathbf{Para}(\odot) is something that looks like

image.png

and a 2-cell is a morphism in C\mathcal{C} obeying an equation like

image.png

view this post on Zulip Nathaniel Virgo (Nov 26 2023 at 01:11):

Now let's assume C\mathcal{C} is monoidal with monoidal product \oplus, and let's assume the action is monoidal.

I don't actually know the definition of a monoidal action (is it written down somewhere?) but I'm guessing it means that diagrams like this are also unambiguous up to canonical isomorphisms:

image.png

For example we can interpret it as (AB)(XY)(A\otimes B)\odot(X\oplus Y) or as A((BX)Y)A\otimes ((B\odot X)\oplus Y) and there will be a canonical isomorphism between them, built up from the various bits of structure.

It should also let us draw the wires "in the wrong order", like

image.png

which can be parsed as (AX)(BY)(A\odot X)\oplus(B\odot Y) or A(X(BY))A\odot(X\oplus(B\odot Y)), and these should be isomorphic as well.

If we only have that then I don't think we'll get a monoidal bicategory structure on Para()\mathbf{Para}(\odot). But I think we can get one if we add another bit of structure: a natural family of isomorphisms (AB)(XY)(AX)(BY)(A\otimes B)\odot(X\oplus Y) \cong (A\odot X)\oplus(B\odot Y), which we can write like this:

image.png

Maybe this also has to obey some coherence laws, I'm not sure. But note that we're not yet assuming M\mathcal{M} or C\mathcal{C} are symmetric monoidal, so we're only allowed to swap black wires with blue wires, not black with black or blue with blue.

view this post on Zulip Nathaniel Virgo (Nov 26 2023 at 01:11):

If we have that then we should be able to define a monoidal structure on Para()\mathbf{Para}(\odot) that looks like this:

image.png

Note that we have to swap a black and a blue wire to draw this, which is why we need that extra bit of structure. Modulo the fact that I've handwaved all the coherence stuff, I think this should have all the properties needed to be a monoidal structure on Para()\mathbf{Para}(\odot).

If, in addition, we assume that C\mathcal{C} and M\mathcal{M} are symmetric monoidal, and that the extra structure preserves the swaps, i.e.

image.png

Then we can write things like

image.png

and I'm guessing that lets you define a symmetry on Para()\mathbf{Para}(\odot). (But I'm less sure about that than the rest of what I said, because I'm not familiar with symmetric monoidal bicategories.)

view this post on Zulip Nathaniel Virgo (Nov 26 2023 at 05:17):

for more on the above see this thread from ages ago. The swap I describe above is exactly the thing that lets you cross wires in the double category diagrams in that old thread.

view this post on Zulip John Baez (Nov 26 2023 at 09:53):

Nathaniel Virgo said:

I don't actually know the definition of a monoidal action (is it written down somewhere?)

I haven't seen it; I just know what it must be. Say the monoidal category MM acts on a category CC and write mcCm \circ c \in C for the action of mMm \in M on cCc \in C. Then we need an "associator"

αm,m,c:(mm)cm(mc) \alpha_{m,m',c} : (m \otimes m') \odot c \xrightarrow{\sim} m \odot (m' \odot c)

and "left unitor"

λc:Icc \lambda_{c} : I \odot c \xrightarrow{\sim} c

obeying a version of the usual pentagon identity (containing a mix of the associator in MM and the associator I just introduced) and the left unitor identity (containing the associator I just introduced, the unitor in MM and the associator I just introduced).

view this post on Zulip John Baez (Nov 26 2023 at 09:56):

In short, you can read off the definition of actegory from the definition of monoidal category, much as you can read off the definition of monoid action from the definition of monoid.

view this post on Zulip Dylan Braithwaite (Nov 26 2023 at 10:19):

This is the definition of an action of a monoidal category on a category, but I think Nathaniel meant an action that is compatible with a monoidal structure on the other category too. i.e. a 'monoidal actegory'

Matteo and Bruno's preprint on actegories has several candidate definitions for this

43d4ac15-90d3-474b-aa4a-097222eda2aa.png

view this post on Zulip John Baez (Nov 26 2023 at 10:31):

Oh, whoops. There should be one of these that corresponds to a pseudofunctor from the delooping of the monoidal category MM to the 2-category MonCat\mathbf{MonCat}. To me that would seem to be the "right" definition.

Of course you get to decide whether morphisms in MonCat\mathbf{MonCat} are lax monoidal functors or strong monoidal functors... I'd say that strict monoidal functors are not useful unless one can prove some sort of strictification theorem.

view this post on Zulip John Baez (Nov 26 2023 at 10:37):

If you used lax monoidal functors, it seems that the Para construction (= 2-Grothendieck construction) would give a lax monoidal category - one where the associator is not invertible.

view this post on Zulip Nathaniel Virgo (Nov 26 2023 at 11:10):

Oh, that's funny - my guess isn't on the list Dylan posted. So then I'll spell my guess out in a bit more detail. I don't know how to talk/think about it in terms of MonCat\mathbf{MonCat} so I'll do it the long way.

I was thinking of the case where neither M\mathcal{M} nor C\mathcal{C} has a braiding. What I imagined was what John said above, plus an associator on the other side

βm,c,c:(mc)cm(cc)\beta_{m,c,c'} : (m\odot c)\oplus c \xrightarrow{\sim} m\odot(c\oplus c)

and right unitor

ρm:mICm\cancel{\rho_m : m\odot I_\mathcal{C} \xrightarrow{\sim} m}

with a "right unitor equation" and two additional pentagon diagrams - one that mixes up β\beta with the associator of C\mathcal{C} and another one that mixes up α\alpha and β\beta, like so:

image.png

I think that should give us what I wanted above, something that lets us interpret diagrams containing black and blue wires as objects in C\mathcal{C} in a coherent way.

view this post on Zulip Dylan Braithwaite (Nov 26 2023 at 11:23):

I don't think the right unitor type-checks. The domain is in C\mathcal{C} and the codomain is in M\mathcal{M}

view this post on Zulip Dylan Braithwaite (Nov 26 2023 at 11:25):

Other than that I think this is equivalent to asking that C\mathcal{C} is a (M,C)(\mathcal M, \mathcal C) bimodule

view this post on Zulip Nathaniel Virgo (Nov 26 2023 at 11:32):

You're right. Maybe it doesn't need the right unitor actually. So now I should go and figure out what a bimodule is.

view this post on Zulip Nathaniel Virgo (Nov 26 2023 at 11:34):

(Though if that's not what the statement on nlab was about then most of what I said today was irrelevant - I apologise for that.)

view this post on Zulip Dylan Braithwaite (Nov 26 2023 at 11:45):

Yeah bimodule is a pretty overloaded term sorry. What I'm talking about is called a biactegory in the above paper, but I prefer bimodule because biactegory is so easy to misread as bicategory. It's a category with a compatible left and right action, analogous to what a bimodule would be for rings.

If an M\mathcal M-actegory is a "2-presheaf" BMCat\mathbb B\mathcal M \to \mathbf{Cat} then an (M,N)(\mathcal M, \mathcal N)-bimodule is a "2-profunctor" BM×(BN)opCat\mathbb B\mathcal M \times (\mathbb B \mathcal N)^\text{op} \to \mathbf{Cat}

view this post on Zulip Dylan Braithwaite (Nov 26 2023 at 11:59):

But actually I think when you ask that one side is just C\mathcal C with its monoidal product (ie your notion of monoidal actegory), these things are equivalent to monoidal functors.

You have isomorphisms
mcm(ic)(mi)cm \odot c \cong m \odot (i \otimes c) \cong (m \odot i) \otimes c so the action is completely determined by the functor ()i:MC(-)\odot i : \mathcal M \to \mathcal C. And conversely any monoidal functor FF gives an action mc=F(m)cm \bullet c = F(m) \otimes c

view this post on Zulip Nathaniel Virgo (Nov 26 2023 at 12:13):

I was just worrying about that. The string diagrams sort of feel like just embedding M\mathcal{M} into C\mathcal{C}, so it sort of makes sense that it's just the same as a monoidal functor MC\mathcal{M}\to\mathcal{C}.

view this post on Zulip Matteo Capucci (he/him) (Nov 26 2023 at 14:19):

John Baez said:

I had thought the only problem was nobody has yet had the energy to write down a proof that the necessary coherence laws hold, to show that this bicategory is symmetric monoidal under these assumptions.

I'd been wanting to pressure someone to do it, or maybe do it myself. I would try constructing a symmetric monoidal double category first, and extracting a symmetric monoidal bicategory from that using Mike Shulman's machinery.

This are indeed the problem and the solution. In particular David Jaz Myers came up with a clever construction which solves many problems of Para, including this one. So me and him are writing a paper right now.
One of the key innovations is studying Para in arbitrary 2-categories with strict 2-limits, such as MonCat\bf MonCat. Para instantiated in MonCat\bf MonCat yields a pseudocategory object (i.e. a [[double category]] in the modern, weak, sense) in MonCat\bf MonCat itself, hence a monoidal double category. From the actegories paper (which exists partly to answer the very question Nathaniel asked), we know the data of an actegory in MonCat\bf MonCat corresponds to a monoidal actegory, i.e. the compatible action of a braided monoidal category on a monoidal category (see Table 1, which Dylan posted above, from the paper). So in the end we get that para for a monoidal actegory yields a monoidal double category. Add symmetric to everything and you get a symmetric monoidal double category.

view this post on Zulip Matteo Capucci (he/him) (Nov 26 2023 at 14:21):

In general, Section 5 in the actegories paper is devoted to studying the compatibility of monoidal and actegorical structure. We define monoidal, braided monoidal and symmetric monoidal actegories there.

view this post on Zulip Nathaniel Virgo (Nov 26 2023 at 14:33):

Does the paper say anything specific about my original question, which is "Suppose M\mathcal{M} is symmetric monoidal and we don't assume a monoidal structure on C\mathcal{C}. Then does Para()\mathbf{Para}(\odot) have any special structure compared to the case where M\mathcal{M} is not symmetric, and if so how can we characterise it"? I got a bit sidetracked by thinking about monoidal structure on C\mathcal{C}, but that was what I was really trying to ask.

view this post on Zulip John Baez (Nov 26 2023 at 15:01):

Matteo Capucci (he/him) said:

This are indeed the problem and the solution. In particular David Jaz Myers came up with a clever construction which solves many problems of Para, including this one. So me and him are writing a paper right now.

"He and I".

One of the key innovations is studying Para in arbitrary 2-categories with strict 2-limits, such as MonCat\bf MonCat. Para instantiated in MonCat\bf MonCat yields a pseudocategory object (i.e. a [[double category]] in the modern, weak, sense) in MonCat\bf MonCat itself, hence a monoidal double category. From the actegories paper (which exists partly to answer the very question Nathaniel asked), we know the data of an actegory in MonCat\bf MonCat corresponds to a monoidal actegory, i.e. the compatible action of a braided monoidal category on a monoidal category (see Table 1, which Dylan posted above, from the paper). So in the end we get that para for a monoidal actegory yields a monoidal double category. Add symmetric to everything and you get a symmetric monoidal double category.

Great, I'm glad you're doing all this! This is mathematics that will be useful for centuries, if civilization survives. There's a certain special satisfaction to be had from doing something historically inevitable but good, and doing a good job of it.

view this post on Zulip Matteo Capucci (he/him) (Nov 26 2023 at 15:15):

Nathaniel Virgo said:

Does the paper say anything specific about my original question, which is "Suppose M\mathcal{M} is symmetric monoidal and we don't assume a monoidal structure on C\mathcal{C}. Then does Para()\mathbf{Para}(\odot) have any special structure compared to the case where M\mathcal{M} is not symmetric, and if so how can we characterise it"? I got a bit sidetracked by thinking about monoidal structure on C\mathcal{C}, but that was what I was really trying to ask.

Ah, sorry, I didn't notice you actually asked something else! :laughing: No, I don't really have anything good to say on the top off my head.

view this post on Zulip Matteo Capucci (he/him) (Nov 26 2023 at 15:16):

John Baez said:

"He and I".

Damn wokes and their pronouns! :P (thanks, I learn with corrections like these)

view this post on Zulip Matteo Capucci (he/him) (Nov 26 2023 at 15:17):

John Baez said:

Great, I'm glad you're doing all this! This is mathematics that will be useful for centuries, if civilization survives. There's a certain special satisfaction to be had from doing something historically inevitable but good, and doing a good job of it.

I sure hope it does!

In the meantime, I made an nLab page about monoidal actegories

view this post on Zulip Jules Hedges (Nov 27 2023 at 10:42):

John and me definitely disagree about prescriptive vs descriptive grammar

I missed a pretty interesting thread here! Very happy to see things worked out... the theorem that decent symmetric monoidal actions are the same as strong monoidal functors is one of my favourites, I sometimes call it the "golden theorem". It puts a hard limit on how weird and exotic things can get when you're studying optics and such

view this post on Zulip Bruno Gavranović (Nov 27 2023 at 10:48):

Jules Hedges said:

It puts a hard limit on how weird and exotic things can get when you're studying optics and such

That is, of course, if you're restricting yourself to strong monoidal functors and non-lax actegories.
The Optic/Para machinery can be generalised to the setting of lax actegories (one way to see this is that lax actegories embed into locally graded ones that Dylan mentioned), and it's not clear to me whether an analogue of a such theorem exists then.

view this post on Zulip Matteo Capucci (he/him) (Nov 27 2023 at 10:57):

Jules Hedges said:

John and me definitely disagree about prescriptive vs descriptive grammar

I missed a pretty interesting thread here! Very happy to see things worked out... the theorem that decent symmetric monoidal actions are the same as strong monoidal functors is one of my favourites, I sometimes call it the "golden theorem". It puts a hard limit on how weird and exotic things can get when you're studying optics and such

It used to be the magic lemma :grinning_face_with_smiling_eyes: golden theorem feels like a promotion!

view this post on Zulip Matteo Capucci (he/him) (Nov 27 2023 at 11:00):

It really is the categorification of a very well-known fact in commutative algebra, that a module structure is the same as a linear map from the acting ring. To me the most interesting result are the ones for monoidal and braided actions. Proving them was a lot of fun! (credit for the idea goes to @Eigil Rischel )

view this post on Zulip Jules Hedges (Nov 27 2023 at 11:00):

Close enough

(Just remembered what I mixed this up with... this was what my general topology lecturer called the result that epsilon-delta-continuous functions between metric spaces are characterised by pulling back opens to opens, ie. the thing that motivates topological spaces)

view this post on Zulip Matteo Capucci (he/him) (Nov 27 2023 at 11:05):

Bruno Gavranović said:

Jules Hedges said:

It puts a hard limit on how weird and exotic things can get when you're studying optics and such

That is, of course, if you're restricting yourself to strong monoidal functors and non-lax actegories.
The Optic/Para machinery can be generalised to the setting of lax actegories (one way to see this is that lax actegories embed into locally graded ones that Dylan mentioned), and it's not clear to me whether an analogue of a such theorem exists then.

I believe so. Up to choosing the directions right, a lax actegory is a graded monad. Graded monads are classified by lax monoidal functors into [C,C][C, C]. And it seems to me that the interaction with the braiding doesn't actually change from the strong case (there are no 'lax braided functors'). So I feel confident to conjecture that the classification theorems extend to the lax case. Of course the devil is in the details...