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: theory: category theory

Topic: modules over rig categories


view this post on Zulip Morgan Rogers (he/him) (Jul 10 2023 at 15:54):

Has anyone considered actions of (symmetric) rig categories on monoidal categories? I have seen that the theoretical development of rig categories takes a lot of work, but with that in one's pocket it should be sensible to consider modules for these; ie "actions on monoidal categories". Has anyone considered this in any detail?

view this post on Zulip Damiano Mazza (Jul 11 2023 at 06:13):

About ten years ago, Paul-André Melliès developed the theory of these things to some extent. He had a draft called Parametric monads and enriched adjunctions, which I am no longer able to find on his web page. Instead, now there's a (published) paper called The parametric continuation monad. Funnily enough, I do not recognize anything in it of the stuff that I remember from the draft :big_smile:

This kind of actions turned out to be useful in the semantics of so-called "graded coeffects" in programming languages, which correspond, on the logical side, to a graded version of the exponential modality of linear logic. We wrote up a brief, superficial categorical account of these models in this paper. Later, Michele Pagani and our mutual colleague Flavien Breuvart studied concrete models based on the relational semantics of linear logic, which are however a bit "decategorified" in the sense that the rig category becomes a preordered rig. Flavien kept developing these things in various directions, he certainly knows more than me about them!

view this post on Zulip Morgan Rogers (he/him) (Jul 11 2023 at 07:41):

I spoke with Flavien about some related things yesterday. It's very curious to me that you present these as "exponential" actions, when if one writes the monoidal product as \oplus the same axioms are explicitly linear!

view this post on Zulip John Baez (Jul 11 2023 at 10:46):

Morgan Rogers (he/him) said:

Has anyone considered actions of (symmetric) rig categories on monoidal categories? I have seen that the theoretical development of rig categories takes a lot of work, but with that in one's pocket it should be sensible to consider modules for these; ie "actions on monoidal categories". Has anyone considered this in any detail?

If so, I haven't seen it! Chris Grossack asked me the same question yesterday, not by coincidence, and my big counter-question was: why do you folks want to think about rig categories instead of just the class of them where the "addition" is given by coproducts or more general colimits? Those seem more manageable, and they seem to come up a lot in practice.

Here are a couple of papers worth knowing, even though they're about these more specialized kinds of rig categories, and they don't seem to say a lot about module categories:

https://arxiv.org/abs/1410.1716

Here Martin Brandenburg studies "cocomplete tensor categories", which are symmetric monoidal categories with all colimits which commute with the tensor product in each variable.

https://arxiv.org/abs/1105.3104

Here Chirvasitu and Johnson-Freyd study "2-rings", which are locally presentable monoidal categories for which the monoidal structure distributes over colimits. So, they're dropping the "symmetric" assumption and strengthening "has all colimits" to "locally presentable" (which is a really smart idea, since it gives you extra leverage without ruling out really interesting examples).

view this post on Zulip Morgan Rogers (he/him) (Jul 11 2023 at 11:08):

John Baez said:

If so, I haven't seen it! Chris Grossack asked me the same question yesterday, not by coincidence, and my big counter-question was: why do you folks want to think about rig categories instead of just the class of them where the "addition" is given by coproducts or more general colimits? Those seem more manageable, and they seem to come up a lot in practice.

Ha, that's easy, it's because an important class of examples for me are those coming from rigs or ordered rigs where + has no reason to coincide with coproduct. The coproduct examples are important, of course, but for our purposes the universal property of the coproduct doesn't see any use.

Thanks for the references. Surprisingly or not, Brandenburg uses several of the free constructions which have arisen in this work, although our applications are in computer science rather than algebraic geometry (not that these things are independent).

view this post on Zulip John Baez (Jul 11 2023 at 11:20):

Cool. It would be great to have a book on categorified rig theory that starts with general rig categories and then specializes to various important cases. In every case I know, the free guy on one generator is quite interesting. For example Todd Joe and I study symmetric monoidal Cauchy complete k-linear categories and show the free guy is a category where objects are finite direct sums of representations of permutation groups. We then marched ahead and wrote a 53-page paper on this. :upside_down:

view this post on Zulip John Baez (Jul 11 2023 at 11:23):

For the case you're considering, the free symmetric rig category on no generators is the groupoid of finite sets... but it would be good to study the free one on one generator too.

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

But the whole theory of modules should also be incredibly interesting.

view this post on Zulip Damiano Mazza (Jul 11 2023 at 13:05):

Morgan Rogers (he/him) said:

It's very curious to me that you present these as "exponential" actions, when if one writes the monoidal product as \oplus the same axioms are explicitly linear!

The name "exponential" comes from "exponential modality" of linear logic. As I mentioned above, we see an action of a symmetric rig category (R,,)(\mathcal R,\oplus,\odot) on a symmetric monoidal category (C,)(\mathcal C,\otimes)

!():R×CC!(-) : \mathcal R\times\mathcal C\to\mathcal C

as a graded version of the exponential modality of linear logic. To stress that, we write !xA!_xA for !(x,A)\mathop !(x,A). The axioms are such that when R\mathcal R is the trivial rig category (one object), this degenerates to a model of the exponential modality in the usual sense. The name "exponential" makes sense because of structural morphisms like

!xyA!xA!yA!_{x\oplus y}A\to \mathop{!}_x A\otimes\mathop{!}_y A

which are part of the action structure and which remind of elementary laws like ax+y=axaya^{x+y}=a^xa^y for the numerical exponential operation. If I understand correctly, you are suggesting to denote by \oplus what I am denoting by \otimes, in which case the above morphism looks indeed like linearity. However, in the context of linear logic, the rig category acts on the multiplicative structure (traditionally denoted by \otimes), not on the additive structure (i.e., coproducts in C\mathcal C, which are traditionally denoted by \oplus in linear logic).

view this post on Zulip Morgan Rogers (he/him) (Jul 11 2023 at 13:23):

That makes sense, and makes it even more interesting that the linear one is the one we use. Our operations/interpretations of the components of linear logic are happening at different categorical levels!

view this post on Zulip Jean-Baptiste Vienney (Jul 11 2023 at 15:14):

All that is very interesting to me. Lately, we introduced graded differential linear logic JS Lemay and me and when I did the talk at MFPS one month ago or so, one guy asked me how we could find something more general than a semi-ring for the coefficients. I didn’t know about these exponential actions. It looks like we could probably add differentiation to this.

view this post on Zulip Damiano Mazza (Jul 11 2023 at 15:35):

Morgan Rogers (he/him) said:

Our operations/interpretations of the components of linear logic are happening at different categorical levels!

I'm curious to know how you are using these actions then! You'll tell me about it next time we meet in our office :big_smile: