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

Topic: are commutative monoidal categories monadic over Petri nets?

John Baez (Feb 14 2021 at 17:36):

Jade Master said:

John Baez Fabrizio Genovese know that we understand the operational semantics a bit better I think we might be able to understand the Montanari-Meseguer style morphisms a bit better. They seem like some sort of Kleisli morphisms for some sort of semantics. Is that what you're getting at?

That is exactly what I was getting at. There's a nice pure math question here, which is whether $\mathsf{CMC}$ is monadic over $\mathsf{Petri}$. You can do something similar to a Kleisli category whenever you have an adjunction; we don't really need the adjunction to be monadic. But we should get a bunch of nice formal properties if it is monadic.

Fabrizio Genovese (Feb 14 2021 at 17:37):

John Baez said:

Jade Master said:

John Baez Fabrizio Genovese know that we understand the operational semantics a bit better I think we might be able to understand the Montanari-Meseguer style morphisms a bit better. They seem like some sort of Kleisli morphisms for some sort of semantics. Is that what you're getting at?

That is exactly what I was getting at. There's a nice pure math question here, which is whether $\mathsf{CMC}$ is monadic over $\mathsf{Petri}$. You can do something similar to a Kleisli category whenever you have an adjunction; we don't really need the adjunction to be monadic. But we should get a bunch of nice formal properties if it is monadic.

I don't know if Petri is monadic over CMC, but I bet PreNet is monadic over (S)MC.

John Baez (Feb 14 2021 at 18:11):

Fabrizio Genovese said:

John Baez said:

That is exactly what I was getting at. There's a nice pure math question here, which is whether $\mathsf{CMC}$ is monadic over $\mathsf{Petri}$. You can do something similar to a Kleisli category whenever you have an adjunction; we don't really need the adjunction to be monadic. But we should get a bunch of nice formal properties if it is monadic.

I don't know if Petri is monadic over CMC, but I bet PreNet is monadic over (S)MC.

Btw, I think you're saying it backwards: if $L: C \to D$ is a left adjoint we say $D$ is monadic over $C$ if certain conditions hold.

John Baez (Feb 14 2021 at 18:44):

The category of gadgets with more structure is "over" the category of gadgets with less structure... forgetfulness goes down.

Fabrizio Genovese (Feb 14 2021 at 21:19):

John Baez said:

Fabrizio Genovese said:

John Baez said:

That is exactly what I was getting at. There's a nice pure math question here, which is whether $\mathsf{CMC}$ is monadic over $\mathsf{Petri}$. You can do something similar to a Kleisli category whenever you have an adjunction; we don't really need the adjunction to be monadic. But we should get a bunch of nice formal properties if it is monadic.

I don't know if Petri is monadic over CMC, but I bet PreNet is monadic over (S)MC.

Btw, I think you're saying it backwards: if $L: C \to D$ is a left adjoint we say $D$ is monadic over $C$ if certain conditions hold.

Yeah, I always forget which way these things go :smile:

John Baez (Feb 14 2021 at 21:31):

I mix up left and right all the time. I find over and under easier to remember. The sun casts shadows down, and the shadow of an object is an example of a forgetful functor.

Morgan Rogers (he/him) (Feb 15 2021 at 09:53):

Jade Master said:

Morgan Rogers (he/him) Yes that is the question. I am currently guessing that it's not monadic but I'm not sure.

It's not too difficult to find out, as long as we know what the functors do and how to calculate some coequalizers in the respective categories. I imagine the latter is the more difficult part, but since there are plenty of experts here, it should be an accessible problem!

Morgan Rogers (he/him) (Feb 15 2021 at 10:13):

It might even be true in the full generality of your paper on Q-nets, but let's not get ahead of ourselves. The description of this adjunction for Petri nets is covered in Section 4 of that paper, and is split into two parts (going via the category of graphs on commutative monoids). It's not unreasonable to hope that the individual parts of the right adjoint will be monadic, and hopefully will satisfy the conditions of the crude monadicity theorem, which is compositional.

Morgan Rogers (he/him) (Feb 15 2021 at 15:23):

I'll start this, since I'm interested enough.
From Definition 4.3, the forgetful functor $A^{\bullet}: \mathbf{Graph}(\mathsf{CMon}) \to \mathsf{Petri}$ sends a graph of commutative monoids
$Q = s,t:E \rightrightarrows V$ to $A^{\bullet}Q = \overline{s}, \overline{t}: \overline{E} \rightrightarrows \mathbb{N}[RV]$,
where $RV$ is the underlying set of the monoid $V$, and
$\overline{E} = \{(e, x, y) \in RE \times \mathbb{N}[RV] \times \mathbb{N}[RV] \mid R\epsilon_V (x) = s(e) \text{ and } R\epsilon_V (y) = t(e)\}$,
for $\epsilon_V: \mathbb{N}[RV] \to V$ the counit of the free-forgetful adjunction between the category of commutative monoids and the category of Sets. $\overline{s}, \overline{t}$ are the second and third projections respectively. There's a description of what happens on morphisms too, but it's more or less the only thing possible once you have the definition of what happens to objects.
As Jade says, this definition is non-trivial! Fortunately, we only have to understand what happens to certain coequalizers.

Morgan Rogers (he/him) (Feb 15 2021 at 15:28):

What does a coequaliser of graphs of commutative monoids look like? Let $P:= q,r: D \rightrightarrows U$ be another such graph. A homomorphism $P \to Q$ consists of a pair of monoid homomorphisms $(f:D \to E, h: U \to V)$ which commute with the structure maps, so $hq = sf$ and $hr = tf$. Let $(g,k)$ be another such. What's the coequalizer of $(f,h)$ and $(g,k)$?

Morgan Rogers (he/him) (Feb 15 2021 at 15:39):

It helps to know what a coequalizer of monoid homomorphisms is (commutativity is preserved for free). The coequalizer of $f$ and $g$, for example, is the quotient $F$ of $E$ by the congruence generated by the span $(f,g)$. Write $W$ for the quotient of $V$ by the congruence generated by $h$ and $k$. We can check that the structure maps $s$ and $t$ descend along this quotient thanks to commuting with the structure maps, so we get $u,v : F \rightrightarrows W$ as the coequalizer of the graphs. Easier than I feared!
Let's call the quotient maps $m:E \twoheadrightarrow F$ and $n:V \twoheadrightarrow W$.

Morgan Rogers (he/him) (Feb 15 2021 at 15:51):

Okay, so now to transfer the diagram of coequalizers (which i haven't actually shown you, but I hope you can picture) along the forgetful functor. We have
$\overline{D} = \{(d, z, w) \in RD \times \mathbb{N}[RU] \times \mathbb{N}[RU] \mid R\epsilon_U (z) = q(d) \text{ and } R\epsilon_U (w) = r(d)\}$,
so $(f,h)$ becomes the mapping $(\overline{f}:\overline{D} \to \overline{E}, \mathbb{N}[Rh]: \mathbb{N}[RU] \to \mathbb{N}[RV])$,
where $\overline{f}(d,z,w) = (Rf(d),\mathbb{N}Rh, \mathbb{N}Rh)$, and similarly for $(g,k)$ and $(m,n)$. Now we need to compare the image of $(m,n)$ with the coequalizer in the category of Petri nets!

Morgan Rogers (he/him) (Feb 15 2021 at 16:04):

I still have letters left, so let's recall what maps of Petri nets look like, from Definition 2.3 of Jade's paper. Let $a,b: A \rightrightarrows \mathbb{N}[B]$ and $a',b': A' \rightrightarrows \mathbb{N}[B']$ be Petri nets. Then a morphism from the former to the latter is $(o:A \to A',p:B \to B')$ such that $a'o = \mathbb{N}[p]a$ and $b'o = \mathbb{N}[p]b$. The coequalizer of a pair of such things is computed by taking the coequalizers in $\mathbf{Set}$, thanks to the fact that the free commutative monoid functor preserves colimits, and letting the maps $a',b'$ descend along the resulting quotient maps.

Morgan Rogers (he/him) (Feb 15 2021 at 16:32):

So comparing $A^\bullet (m,n)$ with the coequalizer of $A^\bullet (f,h)$ and $A^\bullet (g,k)$, we note that $n$ is the coequalizer in the category of monoids, whereas the second component of the coequalizer of $A^\bullet (f,h)$ and $A^\bullet (g,k)$ is (generated by) the coequalizer of $h$ and $k$ as maps of Sets. These are different in general: consider the two canonical maps $\mathbb{N} \rightrightarrows \mathbb{N} \times \mathbb{N}$; their coequalizer in the category of commutative monoids is the trivial monoid, but as maps of sets the coequalizer just collapses all of the elements of the form $(0,n)$ and $(n,0)$ together without touching anything else. So (if I'm not already confused) we can't expect $A^\bullet$ to preserve all coequalizers.

Morgan Rogers (he/him) (Feb 15 2021 at 16:39):

But we know that the coequalizers of pairs which are split by the forgetful functor $R$ are preserved, since commutative monoids are monadic over Set, so the second component of the coequalizer will be preserved in that case. To hope for a compositional monadicity to hold, we need to check reflexive coequalizers. After a quick search, the monad induced by any finitary algebraic theory satisfies the conditions of the crude monadicity theorem, so we're sorted for the second component!

Morgan Rogers (he/him) (Feb 15 2021 at 16:55):

The final question, for this part at least, is whether $\overline{m}: \overline{E} \to \overline{F}$ is the coequalizer of $\overline{f}$ and $\overline{g}$ when these have a mutual splitting. By the same argument as above, since $R$ preserves reflexive coequalizers, the first component of $\overline{m}$ is right. The other components are obtained by pulling back the image of the coequalizer of $h$ and $k$, so thanks to the fact that coequalizers are stable under pullback in Set, those are right too.

Morgan Rogers (he/him) (Feb 15 2021 at 16:57):

In other words...
$A^{\bullet}: \mathbf{Graph}(\mathsf{CMon}) \to \mathsf{Petri}$ is monadic, and satisfies the conditions of the crude monadicity theorem.
Now we just need to do this work again for the functor $B^{\bullet}: \mathsf{CMC} \to \mathbf{Graph}(\mathsf{CMon})$ :grinning_face_with_smiling_eyes:

Morgan Rogers (he/him) (Feb 15 2021 at 17:01):

This should be a straightforward lifting of the proof that categories are monadic over graphs, but there's a little extra work to do to check that it satisfies the crude monadicity theorem too.

Morgan Rogers (he/him) (Feb 15 2021 at 17:06):

@Jade Master if you want to turn the above sketch into a short paper with me in the not too distant future, lmk. :innocent:
I'm sure some of the pieces could be condensed, and indeed that it could be extended to Q-nets, since the main useful fact was that the category of algebras for a finitary algebraic theory is (crudely) monadic, and this is enough because coequalizers are essentially computed componentwise.

John Baez (Feb 15 2021 at 17:26):

Hurrah!

Jade Master (Feb 15 2021 at 17:28):

@Morgan Rogers (he/him) wow :astonished: you did it. I'd love to help write that up, but first I need to spend a bit more time understanding it.

John Baez (Feb 15 2021 at 17:29):

He did half of it.

Jade Master (Feb 15 2021 at 17:32):

True. He did the hard part though :)

John Baez (Feb 15 2021 at 17:32):

It was hard to follow because it involved a blizzard of notation and I was too lazy to draw any pictures myself, but the key I guess is the crude monadicity theorem. Somehow I associate that theorem with @Todd Trimble because he tends to whip it out when needed, and I'm really bad at these monadicity theorems so I always think "gee, I wish I could do that".

Morgan Rogers (he/him) (Feb 15 2021 at 17:32):

And finding any mistakes I've made along the way, of course! In case I wasn't clear before, the reason I'm focussed on using the crude monadicity theorem, which provides a necessary but not sufficient condition for monadicity, is that unlike the precise monadicity theorem, the conditions in this result are compositional, so we can check it separately on the two forgetful functors and conclude that the result holds for the composite.
John beat me to it :joy:

Jade Master (Feb 15 2021 at 17:33):

I'm guessing that the second part of the adjunction follows from some more abstract considerations, like Morgan said.

Morgan Rogers (he/him) (Feb 15 2021 at 17:34):

John Baez said:

It was hard to follow because it involved a blizzard of notation and I was too lazy to draw any pictures myself

Yes, I still haven't found an efficient enough way of drawing diagrams to avoid employing a "you should draw the diagrams yourself to work out what I'm saying" comment.

John Baez (Feb 15 2021 at 17:35):

I hadn't even known the crude monadicity theorem is compositional, but that's really important. After all, the result you're talking about is vaguely, vaguely in the same realm as these facts:

1. Cat is monadic over ReflexiveGraph,
2. ReflexiveGraph is monadic over Set,
3. Cat is not monadic over Set.

John Baez (Feb 15 2021 at 17:35):

Which of 1. or 2. fail the hypotheses of the crude monadicity theorem?

Morgan Rogers (he/him) (Feb 15 2021 at 17:36):

That's an important obstacle. I'm pretty sure it's 1 which fails, unfortunately.

Morgan Rogers (he/him) (Feb 15 2021 at 17:37):

Essentially because monadicity comes down to coequalizers, and those aren't well-behaved in Cat :grimacing:

Morgan Rogers (he/him) (Feb 15 2021 at 17:37):

So perhaps I haven't done the hard part after all :upside_down:

Jade Master (Feb 15 2021 at 17:46):

I will spend some more time thinking about this later today :)

Todd Trimble (Feb 16 2021 at 00:45):

Morgan Rogers (he/him) said:

That's an important obstacle. I'm pretty sure it's 1 which fails, unfortunately.

Yes, exactly right: the forgetful functor from categories to reflexive graphs does not preserve reflexive coequalizers. In fact, there's a sort of interesting ideal-like theorem: if $U_1: A \to B$ satisfies the crude monadicity hypotheses and $U_2: B \to C$ is any monadic functor, then $U_2 \circ U_1$ is monadic. See Barr-Wells, page 121 of 302 of the pdf. Unfortunately, they don't give the proof.

John Baez (Feb 16 2021 at 01:45):

Cool! Much better even than "compositionality".

John Baez (Feb 16 2021 at 01:46):

I assume the crudely monadic functors only work on the right side like that, or you would have told us the other side of the story.

Fawzi Hreiki (Feb 16 2021 at 01:54):

Yeah if it worked the other way, categories would be monadic over sets (which they aren't)

John Baez (Feb 16 2021 at 01:59):

Oh, duh - Todd almost said that.

John Baez (Feb 16 2021 at 02:00):

So to help me remember this: if you're going to forget things, it's good to do the crudely monadic forgetting first.

Fawzi Hreiki (Feb 16 2021 at 02:17):

There’s also the ‘vulgar monadicity conditions’

Fawzi Hreiki (Feb 16 2021 at 02:18):

There’s an exercise in Mac Lane about composing the three in some appropriate order

Todd Trimble (Feb 16 2021 at 02:39):

Yes, that's on the page I referred to.

John Baez (Feb 16 2021 at 03:03):

It's in Barr and Wells. I looked it up and added a little (but nothing vulgar) to the nLab article.

Jade Master (Feb 16 2021 at 03:25):

Morgan Rogers (he/him) said:

It helps to know what a coequalizer of monoid homomorphisms is (commutativity is preserved for free). The coequalizer of $f$ and $g$, for example, is the quotient $F$ of $E$ by the congruence generated by the span $(f,g)$. Write $W$ for the quotient of $V$ by the congruence generated by $h$ and $k$. We can check that the structure maps $s$ and $t$ descend along this quotient thanks to commuting with the structure maps, so we get $u,v : F \rightrightarrows W$ as the coequalizer of the graphs. Easier than I feared!
Let's call the quotient maps $m:E \twoheadrightarrow F$ and $n:V \twoheadrightarrow W$.

This part makes sense to me. Grph(CMon) is a presheaf category so coequalizers should be computed pointwise.

Jade Master (Feb 16 2021 at 03:33):

Okay thanks Morgan, I read through everything and it is making sense to me.

Jade Master (Feb 16 2021 at 03:38):

The one part I'm not familiar with is that pullbacks are stable under coequalizers in Set. What exactly does that mean? If you take the pullback of some coequalizers then that is the same as taking the pullback of each component in the diagram of the coequalizers and then coequalizing at the end?

Jade Master (Feb 16 2021 at 03:44):

I guess that does make sense intuitively in Set. Okay great. To be honest I am kind of surprised that this is looking monadic, I thought the funny business with the right adjoint $\mathsf{Grph(CMon)} \to \mathsf{Petri}$ would surely mess things up....or that morphisms of Petri nets coming just from functions on sets wouldn't be expressive enough.

Jade Master (Feb 16 2021 at 03:55):

Another question is, why do we want this adjunction to be monadic in the first place again? We can definitely always form the Kleisli category for the monad UF... I'm pretty sure that regardless of whether U is monadic then the adjunction into the Kleisli category is initial in the category of adjunctions which compose to the monad UF. If U is monadic then pair (U,F) is actually terminal in that category of adjunctions. What does this get us though?

John Baez (Feb 16 2021 at 06:12):

I just thought it was a cool math question to ask whether commutative monoidal categories are monadic over Petri. You don't need this to define the "pseudo-Kleisli category" where an object is a Petri net and a morphism from $P$ to $Q$ is a morphism of commutative monoidal categories $FP \to FQ$, where $F: \mathsf{Petri} \to \mathsf{CMC}$.

The importance of this "pseudo-Kleisli category" is clear from all the examples we've talked about. It's worth studying. It should have some better properties if it's actually a Kleisli category. But I don't know any!

Nathaniel Virgo (Feb 16 2021 at 07:06):

Can I ask a really basic question: I'm wondering what the functor $U$ does, explicitly. It has to take a commutative monoidal category and turn it into a Petri net, but how does it do that exactly? Does it just send every object to a species, and every morphism to a reaction with a single reactant and a single product? (I'm trying to imagine what the proposed monad would be like, only so I can follow the conversation.)

John Baez (Feb 16 2021 at 07:15):

I'll let Jade give you the details of $U$, but I'll tell you a story about it.

We made an obvious-looking guess about the functor $U: \mathsf{CMC} \to \mathsf{Petri}$- I believe it's exactly the guess you made. We proved it was a functor. We constructed a natural-looking isomorphism

$\mathrm{hom}_{\mathsf{CMC}}(F P , C) \cong \mathrm{hom}_{\mathsf{Petri}}(P, U C)$

for every Petri net $P$ and every commutative monoidal category $C$. So we were happy!

But then we tried to check it was natural in the technical sense and we couldn't! We got stuck... until Michael Shulman showed us that a quite different $U$ was the one we needed.

This is the first time where I was trying to prove something was an adjunction and I got stuck at this particular step, right at the end. It was an interesting lesson.

Morgan Rogers (he/him) (Feb 16 2021 at 09:53):

Nathaniel Virgo said:

Can I ask a really basic question: I'm wondering what the functor $U$ does, explicitly. It has to take a commutative monoidal category and turn it into a Petri net, but how does it do that exactly? Does it just send every object to a species, and every morphism to a reaction with a single reactant and a single product? (I'm trying to imagine what the proposed monad would be like, only so I can follow the conversation.)

$U$ consists of the forgetful functor to the category of graphs of commutative monoids, and then the more complicated construction of a Petri net from a graph that I wrote out above.

Morgan Rogers (he/him) (Feb 16 2021 at 10:08):

Jade Master said:

Another question is, why do we want this adjunction to be monadic in the first place again?

There are several reasons we might want to know 'how monadic' the forgetful functor is. The first is to get some free results about the structure of the category of commutative monoidal categories or Petri nets (I don't know enough about either category to point to something currently unknown that would be made more accessible, but there we go).
The second is that if the adjunction is monadic, or even premonadic (counit is a regular epimorphism for every object) then the Kleisli category embeds full and faithfully into it, so you can treat the Kleisli morphisms as commutative monoidal category functors. Speaking of which, @John Baez, that should clarify the distinction between the Kleisli category for the adjunction and the category you describe, which is the full subcategory of the category of commutative monoidal categories on the free objects (coming from the Kleisli category via the canonical comparison functor).

Morgan Rogers (he/him) (Feb 16 2021 at 10:13):

If it turns out not to be monadic, then it might also be interesting to work out what the category of algebras actually is, since that's yet another category which will encode some interesting information about Petri nets.

Jade Master (Feb 16 2021 at 13:49):

John Baez said:

I just thought it was a cool math question to ask whether commutative monoidal categories are monadic over Petri. You don't need this to define the "pseudo-Kleisli category" where an object is a Petri net and a morphism from $P$ to $Q$ is a morphism of commutative monoidal categories $FP \to FQ$, where $F: \mathsf{Petri} \to \mathsf{CMC}$.

The importance of this "pseudo-Kleisli category" is clear from all the examples we've talked about. It's worth studying. It should have some better properties if it's actually a Kleisli category. But I don't know any!

The Kleisli category exists for any monad, so I don't think there's any reason to use pseudo here.

Jade Master (Feb 16 2021 at 13:55):

Nathaniel Virgo said:

Can I ask a really basic question: I'm wondering what the functor $U$ does, explicitly. It has to take a commutative monoidal category and turn it into a Petri net, but how does it do that exactly? Does it just send every object to a species, and every morphism to a reaction with a single reactant and a single product? (I'm trying to imagine what the proposed monad would be like, only so I can follow the conversation.)

It was said above by Morgan, but just to say it a bit more informally: for a commutative monidal category $C$, $U(C)$ has places given by Ob C and transitions given by tuples $(f,x,y)$ where f is a morphism in C, and x and y are elements of $\mathbb{N}[Ob C]$ which collapse via the counit of the monad $\mathbb{N}$ to the source and target of f.

Morgan Rogers (he/him) (Feb 16 2021 at 13:57):

Jade Master said:

John Baez said:

The importance of this "pseudo-Kleisli category" is clear from all the examples we've talked about.

The Kleisli category exists for any monad, so I don't think there's any reason to use pseudo here.

But what John's describing isn't the Kleisli category, since it involves maps of commutative monoidal categories. Unless we show that $U$ is at least premonadic, in which case the actual Kleisli category coincides with this one.

Jade Master (Feb 16 2021 at 13:59):

Morgan Rogers (he/him) said:

Jade Master said:

Another question is, why do we want this adjunction to be monadic in the first place again?

There are several reasons we might want to know 'how monadic' the forgetful functor is. The first is to get some free results about the structure of the category of commutative monoidal categories or Petri nets (I don't know enough about either category to point to something currently unknown that would be made more accessible, but there we go).
The second is that if the adjunction is monadic, or even premonadic (counit is a regular epimorphism for every object) then the Kleisli category embeds full and faithfully into it, so you can treat the Kleisli morphisms as commutative monoidal category functors. Speaking of which, John Baez, that should clarify the distinction between the Kleisli category for the adjunction and the category you describe, which is the full subcategory of the category of commutative monoidal categories on the free objects (coming from the Kleisli category via the canonical comparison functor).

Most niceness of CMC already follows from being the category of algebras for a Lawvere theory in Cat. You can get completeness and cocompleteness this way...and probably more stuff. I think that personally I'm more likely to find the full-subcategory result to be more useful, there may be lots of nice properties which are preserved by the full inclusion.

Jade Master (Feb 16 2021 at 14:02):

Morgan Rogers (he/him) said:

Jade Master said:

John Baez said:

The importance of this "pseudo-Kleisli category" is clear from all the examples we've talked about.

The Kleisli category exists for any monad, so I don't think there's any reason to use pseudo here.

But what John's describing isn't the Kleisli category, since it involves maps of commutative monoidal categories. Unless we show that $U$ is at least premonadic, in which case the actual Kleisli category coincides with this one.

Oh I see. that makes sense now. The full inclusion means that you can use maps of CMCs to describe the Kleisli category...otherwise you would need to use maps of Petri nets.

Morgan Rogers (he/him) (Feb 16 2021 at 14:04):

Fancy working out the counit of the adjunction? :sweat_smile: If not, I'll get around to it. And we should certainly check that the adjunction isn't monadic sooner or later, if that's the current intuition about the situation.

Jade Master (Feb 16 2021 at 14:13):

Hm let me see. The counit has type $\epsilon: F U (C) \to C$. The objects of FUC are $\mathbb{N}(Ob C)$ and the objects of $C$ are just $Ob C$ so the the object component must be the counit of $\mathbb{N}$. The morphisms of FU(C) are free sequences and sums of triples (f,x,y) as described above, and because the counit should be symmetric monoidal, it suffices to define it on generators. So I'm going to guess that (f,x,y) just maps to the morphism f.

Jade Master (Feb 16 2021 at 14:13):

And the rest of the functor is the unique commutative monoidal functorial extension.

Jade Master (Feb 16 2021 at 14:14):

My intuition was that it's not Monadic but your work has started to convince me that it is :)

Morgan Rogers (he/him) (Feb 16 2021 at 14:21):

Jade Master said:

Hm let me see. The counit has type $\epsilon: F U (C) \to C$. The objects of FUC are $\mathbb{N}(Ob C)$ and the objects of $C$ are just $Ob C$ so the the object component must be the counit of $\mathbb{N}$. The morphisms of FU(C) are free sequences and sums of triples (f,x,y) as described above, and because the counit should be symmetric monoidal, it suffices to define it on generators. So I'm going to guess that (f,x,y) just maps to the morphism f.

This is simpler than I feared! fyi we're aiming to use the result:
premonadic.png
which is an exercise from Monoidal Topology: A Categorical Approach to Order, Metric and Topology (edited by Dirk Hofmann, Gavin J. Seal, Walter Tholen)

Morgan Rogers (he/him) (Feb 16 2021 at 14:21):

Sorry for low quality, I just took a screenshot. There's probably a comparable result or exercise in TTT.

Daniele Palombi (Feb 16 2021 at 15:52):

Great! I asked around about this like a thousand of times (the main victims being @fosco and @Fabrizio Genovese )
Maybe i should start posting questions here...

John Baez (Feb 16 2021 at 17:29):

Jade Master said:

John Baez said:

I just thought it was a cool math question to ask whether commutative monoidal categories are monadic over Petri. You don't need this to define the "pseudo-Kleisli category" where an object is a Petri net and a morphism from $P$ to $Q$ is a morphism of commutative monoidal categories $FP \to FQ$, where $F: \mathsf{Petri} \to \mathsf{CMC}$.

The importance of this "pseudo-Kleisli category" is clear from all the examples we've talked about. It's worth studying. It should have some better properties if it's actually a Kleisli category. But I don't know any!

The Kleisli category exists for any monad, so I don't think there's any reason to use pseudo here.

Sure there is! The "pseudo-Kleisli category", where

• an object is a Petri net and a morphism from $P$ to $Q$ is a morphism of commutative monoidal categories $FP \to FQ$, where $F: \mathsf{Petri} \to \mathsf{CMC}$

is equivalent to the "Kleisli category", where

• an object is a free algebra of the monad $UF : \mathsf{Petri} \to \mathsf{Petri}$ and a morphism is a morphism of algebras

iff the forgetful functor $U: \mathsf{CMC} \to \mathsf{Petri}$ is monadic. So it's an interesting pure math question whether $U$ is monadic.

John Baez (Feb 16 2021 at 17:31):

The pseudo-Kleisli category is important regardless of whether it's equivalent to the Kleisli category! We've seen already that it has lots of applications.

But it might be helpful to prove these categories are equivalent, by proving $U$ is monadic. Until we know they're equivalent, we need different names for them.

John Baez (Feb 16 2021 at 17:35):

I'm not claiming this question is good for anything. It's just an obvious question that's sitting there waiting to be answered - like "is every even number > 4 a sum of two primes?", though probably a lot easier.

John Baez (Feb 16 2021 at 18:48):

(As usual I respond to the first thing I see and then later read that people have already sorted it out. But I think some people like seeing everything written out carefully.)

John Baez (Feb 16 2021 at 18:53):

@Morgan Rogers (he/him) wrote:

There are several reasons we might want to know 'how monadic' the forgetful functor is. The first is to get some free results about the structure of the category of commutative monoidal categories or Petri nets (I don't know enough about either category to point to something currently unknown that would be made more accessible, but there we go).

We already know we have an adjunction between $\mathsf{Petri}$ and $\mathsf{CMC}$, and we know both categories are complete and cocomplete. We know some things about $\mathsf{CMC}$ just because it's the category of commutative monoid objects in the cartesian 1-category $\mathsf{Cat}$. What are some more things we'd learn from knowing the adjunction between them is monadic? I'm really not very knowledgeable about this, so anything would be interesting.

the counit is a regular epimorphism for every object...

That's one!

Mike Shulman (Feb 16 2021 at 19:36):

Is "pseudo-Kleisli category" a common term? It's a bit misleading to those of us who are used to associating "pseudo" with "up to isomorphism"; if I understand correctly this is just the bijective-on-objects / fully-faithful factorization of the free CMC functor.

Mike Shulman (Feb 16 2021 at 19:38):

John Baez said:

1. Cat is monadic over ReflexiveGraph,
2. ReflexiveGraph is monadic over Set,
3. Cat is not monadic over Set.

Sorry if this is a dumb question, but why is ReflexiveGraph monadic over Set? Do you mean a reflexive graph in the sense of a set of vertices, a set of edges with sources and targets, and a specified loop at each vertex? The "set of vertices" functor from that category to Set isn't even conservative, so it can't be monadic. Are you thinking of a different forgetful functor, like the "set of edges"?

John Baez (Feb 16 2021 at 19:44):

Mike Shulman said:

Is "pseudo-Kleisli category" a common term? It's a bit misleading to those of us who are used to associating "pseudo" with "up to isomorphism...

No, I just made it up on the spur of the moment. Don't get too worked up over it, I'm not going to publish a paper with this. I could say "Kleisloid category" if you prefer.

John Baez (Feb 16 2021 at 19:45):

if I understand correctly this is just the bijective-on-objects / fully-faithful factorization of the free CMC functor.

Yeah.

Morgan Rogers (he/him) (Feb 16 2021 at 20:29):

Mike Shulman said:

John Baez said:

1. Cat is monadic over ReflexiveGraph,
2. ReflexiveGraph is monadic over Set,
3. Cat is not monadic over Set.

Sorry if this is a dumb question, but why is ReflexiveGraph monadic over Set? Do you mean a reflexive graph in the sense of a set of vertices, a set of edges with sources and targets, and a specified loop at each vertex? The "set of vertices" functor from that category to Set isn't even conservative, so it can't be monadic. Are you thinking of a different forgetful functor, like the "set of edges"?

Indeed, the set of edges functor is the one making this monadic, cf nLab. The category of reflexive graphs is equivalent to the category of $M$-sets for $M$ a certain monoid with three elements, and that equivalence turns the "edges" functor into the usual $M$-sets forgetful functors. A consequence of this is that the same functor is comonadic!

Fawzi Hreiki (Feb 16 2021 at 20:33):

I think the forgetful functor from reflexive graphs to graphs satisfies the crude monadicity conditions so that's another way of seeing this.

Fawzi Hreiki (Feb 16 2021 at 20:34):

(Since the edges functor from graphs to sets satisfies those conditions too and so we can compose)

John Baez (Feb 16 2021 at 20:38):

Indeed, the set of edges functor is the one making this monadic...

By the way, this is connected to Ehresmann's idea of describing a category purely in terms of morphisms, not objects, and naming categories after their morphisms, not their objects. I guess instead of Vect he'd say something like Lin.

Fawzi Hreiki (Feb 16 2021 at 20:41):

Its a nice fact that you can define a category as a set of edges with domain and codomain maps and composition, but no one really thinks that way in practice.

Fawzi Hreiki (Feb 16 2021 at 20:42):

But yeah the reason 'morally' why this edges functor is monadic is that a directed graph, even though it seems a priori two-sorted, is actually determined by just the edges.

Mike Shulman (Feb 17 2021 at 02:35):

Thanks! Is it obvious, then, that the composite "set of arrows" functor from Cat to Set is not monadic?

Todd Trimble (Feb 17 2021 at 03:19):

You might not like this, but there is no monadic functor from Cat to Set because Cat is not a regular category.

Mike Shulman (Feb 17 2021 at 03:39):

Haha, no, I like that fine.

Mike Shulman (Feb 17 2021 at 03:39):

That's interesting -- I never thought about it quite like that before, but maybe it helps to explain why I never liked the single-sorted definition of category much.