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: A topos of Petri nets?

Jade Master (Apr 27 2020 at 07:54):

Let $\mathsf{Petri}$ be the category where

• objects are Petri nets i.e.. pairs of functions $s,t : T \to \mathbb{N}[S]$ where $\mathbb{N}[S]$ is the free commutative monoid on $S$ and,
• a morphism from a Petri net $P$ to a Petri net $P'$ is a pair of functions $(f : T \to T', g : S \to S')$ commuting with the source and target maps of $P$ and $P'$.
  I'm trying to prove/disprove that $\mathsf{Petri}$ is a topos. I know that $\mathsf{Petri}$ is cocomplete. This is because it can be constructed as the comma category $( 1_\mathsf{Set} \downarrow \mathbb{N}[-] \times \mathbb{N}[-] )$ where $\mathbb{N}[-] \times \mathbb{N}[-]$ is the functor which sends a set $X$ to the cartesian product $\mathbb{N}[X] \times \mathbb{N}[X]$. Cocompleteness follows from the proposition in section four of this nLab article .

Jade Master (Apr 27 2020 at 08:06):

If it's not a topos maybe there is a way to tweak the morphisms so that it becomes one.

Thomas Read (Apr 27 2020 at 08:29):

I think there's a subobject classifier, analogous to the one for the category of directed graphs.

That is, we have two places $A$ (places mapping to this will be in the corresponding subobject) and $B$ (places mapping to this will not be in the corresponding subobject). And for every $n, m \in \mathbb{N}$ we have a transition from $n$ tokens at $A$ to $m$ tokens at $A$ (transitions mapping to these will be in the subobject). And for every $n, m, k, l \in \mathbb{N}$ we have a transition from $n$ tokens at $A$ and $m$ tokens at $B$ to $l$ tokens at $A$ and $k$ tokens at $B$ (transitions mapping to these will not be in the subobject).

Thomas Read (Apr 27 2020 at 08:34):

(I'm assuming that a subobject of a Petri net is a subset of the places, along with a subset of the transitions which only involve the chosen places)

Jade Master (Apr 27 2020 at 08:45):

A subobject is a pair of subsets like you mentioned except that the inclusion of transitions must preserve the source and target on the nose. If a place is in the source of a transition in your subobject, then those places must also be in your subobject and the arcs connecting them. A similar statement is true for the outputs of transitions in your subobject.

Jade Master (Apr 27 2020 at 08:50):

Your subobject classifier seems like it's right to me though. I'll have to think on it a bit.

Morgan Rogers (he/him) (Apr 27 2020 at 09:33):

I don't think it has a terminal object. The collection of nets with $S$ and $T$ both singletons is jointly terminal, but none of them admits a morphism from all of the objects.

Thomas Read (Apr 27 2020 at 09:36):

I think the net with one place $A$, and a transition from $n$ tokens at $A$ to $m$ tokens at $A$ for every $n, m \in \mathbb{N}$ is terminal?

Fabrizio Genovese (Apr 27 2020 at 09:36):

Morgan Rogers said:

I don't think it has a terminal object. The collection of nets with $S$ and $T$ both singletons is jointly terminal, but none of them admits a morphism from all of the objects.

I think you are right

Fabrizio Genovese (Apr 27 2020 at 09:37):

Thomas Read said:

I think the net with one place $A$, and a transition from $n$ tokens at $A$ to $m$ tokens at $A$ for every $n, m \in \mathbb{N}$ is terminal?

What is "for all" in the context of PT nets? m and n must be fixed

Thomas Read (Apr 27 2020 at 09:38):

As in $T \cong \mathbb{N}^2$. For each pair $(n, m)$ we add a separate transition going from $n$ tokens to $m$ tokens.

Fabrizio Genovese (Apr 27 2020 at 09:39):

Oh, in that way!

Fabrizio Genovese (Apr 27 2020 at 09:39):

I'm trying to find a reason why this doesn't work, but intuitively it seems it should

Morgan Rogers (he/him) (Apr 27 2020 at 09:40):

I went away for 5 minutes and came up with T a singleton, S the empty set, but that doesn't sound like what you're suggesting?

Fabrizio Genovese (Apr 27 2020 at 09:41):

So for each transition you send all its inputs to the first place, all its outputs to the second place, then you sum all the arities of the arcs, you get m and n and there is exactly one transition from the place to the left to the place to the right that takes m tokens on the left and gives n tokens on the right

Fabrizio Genovese (Apr 27 2020 at 09:41):

The singleton gets sent to the transition having 0 inputs and 0 outputs

Fabrizio Genovese (Apr 27 2020 at 09:42):

there is exactly one of such transition in the net @Thomas Read proposed

Morgan Rogers (he/him) (Apr 27 2020 at 09:42):

I don't know what transitions are in terms of $s$ and $t$...

Thomas Read (Apr 27 2020 at 09:42):

$T$ is transitions, $S$ is places

Fabrizio Genovese (Apr 27 2020 at 09:42):

transitions are the Ts, places are the Ss :D

Fabrizio Genovese (Apr 27 2020 at 09:43):

But anyway, since Graph is a topos I don't find too hard to believe Petri nets are too

Thomas Read (Apr 27 2020 at 09:43):

$s$ and $t$ takes a transition and tells you the "source" and "target"

Fabrizio Genovese (Apr 27 2020 at 09:43):

(an elementary one, obviously)

Morgan Rogers (he/him) (Apr 27 2020 at 09:44):

So this is the Petri net that sends $(m,n)$ to $m$, $n$ respectively?

Fabrizio Genovese (Apr 27 2020 at 09:44):

Yes

Fabrizio Genovese (Apr 27 2020 at 09:44):

The interesting question is "what does the internal logic tell you about this? And what about the geometric interpretation?"

Morgan Rogers (he/him) (Apr 27 2020 at 09:45):

Woah hang on, we haven't established if it is a topos yet!

Fabrizio Genovese (Apr 27 2020 at 09:45):

I fear the answer is "not much wrt the concurrency stuff you usually study with a Petri net", but I'd be extra-glad to be proven wrong

Morgan Rogers (he/him) (Apr 27 2020 at 09:45):

Fabrizio Genovese said:

So for each transition you send all its inputs to the first place, all its outputs to the second place, then you sum all the arities of the arcs, you get m and n and there is exactly one transition from the place to the left to the place to the right that takes m tokens on the left and gives n tokens on the right

Why should this be the unique morphism into this object?

Fabrizio Genovese (Apr 27 2020 at 09:45):

I do agree with you, but I cannot avoid to ask "why" we want it to be a topos :D

Fabrizio Genovese (Apr 27 2020 at 09:46):

Morgan Rogers said:

Fabrizio Genovese said:

So for each transition you send all its inputs to the first place, all its outputs to the second place, then you sum all the arities of the arcs, you get m and n and there is exactly one transition from the place to the left to the place to the right that takes m tokens on the left and gives n tokens on the right

Why should this be the unique morphism into this object?

Oh. Hm, you are right, I could send some output places to the input places, say, and since I have a transition for each (m,n) then I'd be able to map transitions too, most likely

Fabrizio Genovese (Apr 27 2020 at 09:46):

So the morphism doesn't have to be unique

Thomas Read (Apr 27 2020 at 09:47):

What do you mean by output places and input places? My description only had one place

Fabrizio Genovese (Apr 27 2020 at 09:47):

(deleted)

Fabrizio Genovese (Apr 27 2020 at 09:47):

(deleted)

Fabrizio Genovese (Apr 27 2020 at 09:48):

(deleted)

Fabrizio Genovese (Apr 27 2020 at 09:49):

Thomas Read said:

What do you mean by output places and input places? My description only had one place

Sorry, you are rght xD

Morgan Rogers (he/him) (Apr 27 2020 at 09:49):

For $T = \{*\}$ and $S = \emptyset$ so that $\mathbb{N}[S] = \{*\}$, there is only one possible choice of $s,t$, and there is clearly at most one morphism from any Petri net to $(T',S')$ to it; one can check that the squares are always forced to commute, so it works :+1:

Thomas Read (Apr 27 2020 at 09:52):

If $S'$ is non-empty then there are no morphisms $S' \to \emptyset$ so no morphisms $(T', S') \to (T, S)$?

Fabrizio Genovese (Apr 27 2020 at 09:53):

You don't want morphism $S' \to \emptyset$, but morphisms between their free commutative monoids

Fabrizio Genovese (Apr 27 2020 at 09:54):

and the commutative monoid generated by the empty set is just the unit, so you can send any commutative monoid to it and get a homomorphism

Morgan Rogers (he/him) (Apr 27 2020 at 09:55):

Thomas Read said:

If $S'$ is non-empty then there are no morphisms $S' \to \emptyset$ so no morphisms $(T', S') \to (T, S)$?

Oh whoops... yep with the given def'n of morphisms this doesn't work!

Thomas Read (Apr 27 2020 at 09:55):

Jade Master said:

• a morphism from a Petri net $P$ to a Petri net $P'$ is a pair of functions $(f : T \to T', g : S \to S')$ commuting with the source and target maps of $P$ and $P'$.

Fabrizio Genovese (Apr 27 2020 at 09:55):

Yes, I was about to say, this is the tricky part

Fabrizio Genovese (Apr 27 2020 at 09:55):

It depends on the definition you choose. Montanari and Meseguer in Petri nets are monoids, for instance, do not require that the homomorphism has to come from a function between generators

Fabrizio Genovese (Apr 27 2020 at 09:56):

that is, for them $g$ is any homomorphism $\mathbb{N}[S] \to \mathbb{N}[S']$

Fabrizio Genovese (Apr 27 2020 at 09:57):

(Petri nets are monoids is arguably the most important paper in this research field, so it' not like it's an unknown definition)

Fabrizio Genovese (Apr 27 2020 at 09:59):

"The initial net has no transitions and no places, while the final net has one transition and no places. The construction of the coproduct of two Petri nets generalizes to arbitrary families of nets. Petri has neither arbitrary limits nor arbitrary colimits. This is due to the fact that the category of free commutative monoids lacks arbitrary limits and colimits. However, dropping the freeness requirement for the monoid of nodes leads to a bigger category GraIPetri that has all limits and colimits. "

Fabrizio Genovese (Apr 27 2020 at 10:00):

Lol, it's funny to see how anything you can ask about Petri nets has most likely already been worked out in Meseguer-Montanari. xD

Morgan Rogers (he/him) (Apr 27 2020 at 10:03):

Fabrizio Genovese said:

"The initial net has no transitions and no places, while the final net has one transition and no places. The construction of the coproduct of two Petri nets generalizes to arbitrary families of nets. Petri has neither arbitrary limits nor arbitrary colimits. This is due to the fact that the category of free commutative monoids lacks arbitrary limits and colimits. However, dropping the freeness requirement for the monoid of nodes leads to a bigger category GraIPetri that has all limits and colimits. "

Sounds like working with Kleisli vs Eilenberg-Moore!

Thomas Read (Apr 27 2020 at 10:07):

I think with @Jade Master 's definition we do have binary products, though they're a bit weird (haven't checked the details but feels like it works). Suppose we have nets $(S, T)$ and $(S', T')$. Then the product has a set of places $S \times S'$. The transitions are given by pairs of transitions $t \in T$, $$t' \in T'$ along with a choice of source tokens and target tokens such that if we "forget the second coordinate" we get the source and target tokens for $t$, and if we "forget the first coordinate" we get the source and target tokens for $t'$.

Thomas Read (Apr 27 2020 at 10:14):

image-fdac1a76-dc22-4b9e-b2e1-0025eddbec73.jpg

Thomas Read (Apr 27 2020 at 10:14):

^ the transitions in the product is the limit of that thing, where e.g. the map $\mathbb{N}[S \times T] \times \mathbb{N}[S \times T] \to \mathbb{N}[S] \times \mathbb{N}[S]$ is induced by the projection $S \times T \to S$.

Thomas Read (Apr 27 2020 at 10:18):

Oh we already had completeness from @Jade Master 's remark about comma categories anyway

Morgan Rogers (he/him) (Apr 27 2020 at 10:20):

Jade mentioned cocompleteness actually. I guess the lower right Ts should be S'

Thomas Read (Apr 27 2020 at 10:21):

Oh sorry yup - clearly changed my mind about letters half way through...

Morgan Rogers (he/him) (Apr 27 2020 at 10:22):

But anyway, with the original definition I think we've established that there's no terminal object, so no hope of it being a topos?

Thomas Read (Apr 27 2020 at 10:23):

She said cocompleteness, but I think both follow from her reference https://ncatlab.org/nlab/show/comma+category#properties since $\text{Set}$ is complete and cocomplete, and the identity on $\text{Set}$ is continuous and cocontinuous

Thomas Read (Apr 27 2020 at 10:25):

I wrote down something that I think is the terminal object - I don't think anyone's shown it isn't yet? (@Fabrizio Genovese thought he'd found a problem but had misread the definition)

Morgan Rogers (he/him) (Apr 27 2020 at 10:32):

Yep okay, I was briefly confused about how the free commutative monoid is defined. There is a unique morphism $S' \to \{*\}$, and composing $s',t'$ with the resulting morphism $\mathbb{N}[S'] \to \mathbb{N}$ we get two morphisms $T' \to \mathbb{N}$ and so a unique factoring map through $\mathbb{N} \times \mathbb{N}$. Nice one @Thomas Read !

Fabrizio Genovese (Apr 27 2020 at 10:58):

I reiterate my question: Assuming Jade definition or Meseguer definition, it's still interesting to establish what the internal logic of the topos gives you. To do this we still have to answer the obvious question: How does a subobject in Petri look like?

Fabrizio Genovese (Apr 27 2020 at 10:58):

My gut feeling is that it's just a subnet, maybe a generalized one?

Morgan Rogers (he/him) (Apr 27 2020 at 10:59):

Since I'm going around in circles on this, I'll share what I was trying to do, and anyone else who thinks it looks like a good idea can pick it up. Structurally, the objects of Petri look like coalgebras. I think that for a judicious choice of base topos ($[2,\mathrm{Set}]$? $[\bullet \to \bullet ,\mathrm{Set}]$?) and a suitable choice of forgetful functor, it could be expressed as the category of coalgebras for some comonad on a topos, which is one of the fastest ways to show that something is a topos, if it is a topos.
But it might be quicker to check that exponentials exist, and to double check the subobject classifier suggested earlier. :shrug:

Thomas Read (Apr 27 2020 at 11:00):

Think I've got power objects, though I'd need to sit down and check some details to be totally sure.

Let $(S, T)$ be a net. The set of places for the power object is the set $\mathcal{P}(S)$ of subsets of $S$. A transition in the power object consists of a source $A_1 + \dotsb + A_n \in \mathbb{N}[\mathcal{P}(S)]$ (i.e. $A_i \in \mathcal{P}(S)$), a target $B_1 + \dotsb + B_m \in \mathbb{N}[\mathcal{P}(S)]$, for each $1 \le i \le n$ a choice of $a_i \in A_i$ and for each $1 \le j \le m$ a choice of $b_i \in B_i$, and a transition $t \in T$ from $a_1 + \dotsb + a_n$ to $b_1 + \dotsb + b_m$.

Edit: actually you'll need to be a bit careful about when you say two transitions described like that are the same, though I think there's probably only one sensible way to do it.

Edit 2: sorry, a transition with given source and sink should be a set of $(a_i, b_i, t)$ as described above.

@Jade Master if that's all correct then we have finite limits, a subobject classifier and power objects, so a topos!

Thomas Read (Apr 27 2020 at 11:01):

@Fabrizio Genovese Jade described the subobjects under her definition near the start of the conversation

Thomas Read (Apr 27 2020 at 11:01):

(I imagine it's what you'd call a subnet)

Fabrizio Genovese (Apr 27 2020 at 11:36):

Yes, it's the same thing

Fabrizio Genovese (Apr 27 2020 at 11:36):

That is basically a mono in Petri, indeed

Fabrizio Genovese (Apr 27 2020 at 11:39):

Thomas Read said:

Think I've got power objects, though I'd need to sit down and check some details to be totally sure.

Let $(S, T)$ be a net. The set of places for the power object is the set $\mathcal{P}(S)$ of subsets of $S$. A transition in the power object consists of a source $A_1 + \dotsb + A_n \in \mathbb{N}[\mathcal{P}(S)]$ (i.e. $A_i \in \mathcal{P}(S)$), a target $B_1 + \dotsb + B_m \in \mathbb{N}[\mathcal{P}(S)]$, for each $1 \le i \le n$ a choice of $a_i \in A_i$ and for each $1 \le j \le m$ a choice of $b_i \in B_i$, and a transition $t \in T$ from $a_1 + \dotsb + a_n$ to $b_1 + \dotsb + b_m$.

Edit: actually you'll need to be a bit careful about when you say two transitions described like that are the same, though I think there's probably only one sensible way to do it.

Jade Master if that's all correct then we have finite limits, a subobject classifier and power objects, so a topos!

Well we still have to check that the proposed subobject classifier indeed classifies stuff :slight_smile:

Fabrizio Genovese (Apr 27 2020 at 11:44):

In any case, if this is a topos, I guess the internal logic would give you a way to identify subnets of a net that do some kind of stuff. It woul be indeed very nice if the "some kind of stuff" would be related to the reachability relation in a net, but that's just wild guessing for now

John Baez (Apr 27 2020 at 15:16):

I doubt the category of Petri nets is a topos, so I'd urge you to bite the bullet and try to prove it's not. It's tough for young mathematicians to try to prove the opposite of what they want, but the truth doesn't care what we want, so it's important to play both sides - it's best to learn the truth as soon as possible.

John Baez (Apr 27 2020 at 15:17):

Fabrizio Genovese said:

But anyway, since Graph is a topos I don't find too hard to believe Petri nets are too

Graphs are a presheaf category, Petri nets are not. Topoi are not a dime a dozen; if you're in one you tend to know it pretty quick.

John Baez (Apr 27 2020 at 15:17):

I would try to prove that Petri is not cartesian closed.

John Baez (Apr 27 2020 at 15:20):

I'd take two rather small Petri nets X and Y and show there's no Petri net [X,Y] such that morphisms A $\to$ [X,Y] correspond naturally to morphisms A $\times$ X $\to$ Y.

John Baez (Apr 27 2020 at 15:21):

On the other hand, it's worth checking out @Thomas Read's suggested power object. Play both sides of this game!

John Baez (Apr 27 2020 at 15:26):

You may recall that Daniel Cicala used "Artin gluing" to get a lot of topoi as comma categories: if $E$ and $F$ are topoi and $u : E \to F$ preserves finite limits, the comma category $\mathrm{id}_F/u$ is a topos.

John Baez (Apr 27 2020 at 15:29):

Since $\mathsf{Petri}$ is a comma category you could try to use this to prove it's a topos. I believe you'll find that $u = \mathbb{N}[-] \times \mathbb{N}[-]$ doesn't preserve finite limits, so this strategy fails. But please check! (It doesn't preserve the terminal object, does it?)

John Baez (Apr 27 2020 at 15:31):

Of course, even if this method of showing $\mathsf{Petri}$ is a topos fails, that doesn't mean $\mathsf{Petri}$ isn't a topos!

John Baez (Apr 27 2020 at 15:31):

So it's more efficient to go out and try to show $\mathsf{Petri}$ is not a topos (and also try to show it is).

Reid Barton (Apr 27 2020 at 15:37):

Yes, I also suspect $\mathsf{Petri}$ is not a topos for this reason; if it does succeed in being one, it would be good to understand exactly how this happens without the gluing functor preserving finite limits.

John Baez (Apr 27 2020 at 15:41):

Btw, I should remind Jade that for a long time we were talking about a topos where the objects are almost the Petri nets we consider now, but not quite, and the morphisms are very different than the morphisms we use now. This topos was a presheaf category: it was the category of bipartite graphs, where you have a set of places, a set of transitions, a set of "place-to-transition" edges, and a set of "transition-to-place" edges.

John Baez (Apr 27 2020 at 15:42):

I was really excited about this topos for a while, but then we decided that the morphisms were too weird.

Joe Moeller (Apr 27 2020 at 17:26):

I wonder if there is any interesting Grothendieck topology one could put on this?

Joe Moeller (Apr 27 2020 at 17:26):

Of course, that wouldn't solve the problem, since you would be restricting the objects, not the morphisms.

Fabrizio Genovese (Apr 27 2020 at 17:35):

I guess this is related to what I was trying to say before, that is: What does the internal logic buy you in this setting? Even if Petri is not a topos, what can we use its internal logic for? And how expressive is it? I guess these questions are relevant depending on which perspective you have on topos theory. For me it's a logical one, so I tend to think about Grothendieck topologies as something you want/not want wrt what you want the internal logic to do.

Jules Hedges (Apr 27 2020 at 17:37):

What can you do using the internal logic of $\mathbf{Gph}$? Has anyone done anything cool using it?

Fabrizio Genovese (Apr 27 2020 at 17:37):

This is indeed a very nice question I don't know anything about. :slight_smile:

Chad Nester (Apr 27 2020 at 17:47):

Petri nets strike me as more of a realizability topos thing than a "Topos on the nose" thing.

John Baez (Apr 27 2020 at 18:15):

@Mike Stay and @Christian Williams are the only people I know who have tried to do anything "cool" with the internal logic of $\mathsf{Gph}$.

John Baez (Apr 27 2020 at 18:29):

The internal logic of $\mathsf{Gph}$ is pretty simple. Its subobject classifier should be thought of as the "graph of truth values". It works like this: vertices of any graph can be in a subgraph or out, so the graph of truth values has two vertices: a vertex "true" and a vertex "false". But edges come in 5 kinds:

the subobject classifier for Gph

They can be completely in the subgraph, have neither source nor target in the subgraph, have their source in the subgraph but not their target, have their target in the subgraph but not their source, or they can have both source and target in the subgraph but not themselves lie in the subgraph!

Morgan Rogers (he/him) (Apr 27 2020 at 18:30):

John Baez said:

Since $\mathsf{Petri}$ is a comma category you could try to use this to prove it's a topos. I believe you'll find that $u = \mathbb{N}[-] \times \mathbb{N}[-]$ doesn't preserve finite limits, so this strategy fails. But please check! (It doesn't preserve the terminal object, does it?)

Well... we can fix that! The functor $X \mapsto \mathbb{N}[X] \times \mathbb{N}[X]$ naturally falls into the slice of $\mathrm{Set}$ over the $\mathbb{N} \times \mathbb{N}$, by equipping $\mathbb{N}[X] \times \mathbb{N}[X]$ with the morphism that sends an element to the sum of the coefficients in each argument. Now we have a functor that does preserve the terminal object; how much have we changed the comma category?

John Baez (Apr 27 2020 at 18:31):

I don't know. Is this trick enough to create a topos? Jade demands a topos! :upside_down:

Fabrizio Genovese (Apr 27 2020 at 18:34):

John Baez said:

The internal logic of $\mathsf{Gph}$ is pretty simple. Its subobject classifier should be thought of as the "graph of truth values". It works like this: vertices of any graph can be in a subgraph or out, so the graph of truth values has two vertices: a vertex "true" and a vertex "false". But edges come in 5 kinds:

the subobject classifier for Gph

They can be completely in the subgraph, have neither source nor target in the subgraph, have their source in the subgraph but not their target, have their target in the subgraph but not their source, or they can have both source and target in the subgraph but not themselves lie in the subgraph!

This is very cool, so the internal logic of the topos identifies subgraphs of a graph, that is, it does "the useful thing".

Fabrizio Genovese (Apr 27 2020 at 18:35):

E.g. You can define internal formulas that stand for things like "Give me the subgraph of this graph such that..."

John Baez (Apr 27 2020 at 18:37):

Right. The subobject classifier is doing its job, classifying subobjects.

Jade Master (Apr 27 2020 at 21:24):

@Morgan Rogers interesting idea. The objects of this proposed comma category aren't really Petri nets anymore. They are Petri nets with only one place.

Jade Master (Apr 27 2020 at 21:25):

@Fabrizio Genovese if Petri is a topos then it will have a sound theory of double pushout rewriting. More generally if it is an adhesive category then this is true.

Fabrizio Genovese (Apr 27 2020 at 21:25):

That would make me really happy :D

Mike Shulman (Apr 27 2020 at 23:04):

It seems very unlikely to me that Petri is a topos. Generally whenever you have strict commutativity appearing, topos-like properties tend to fail. See for instance https://arxiv.org/abs/1209.0414. It could be that the example therein could be adapted to Petri.

John Baez (Apr 27 2020 at 23:11):

I wonder if Petri could be adhesive. That's an interesting fallback position.

Jade Master (Apr 28 2020 at 00:00):

Hey is @Daniel Cicala here?

John Baez (Apr 28 2020 at 01:16):

Never seen him here. He barely made his presence felt on our UCR Zulip! Not that kind of guy.

sarahzrf (Apr 28 2020 at 04:07):

Joe Moeller said:

I wonder if there is any interesting Grothendieck topology one could put on this?

do you mean lawvere-tierney topology? otherwise i'm not sure what you'd mean by it restricting the objects

Thomas Read (Apr 28 2020 at 07:16):

I've figured out a problem with my proposed power object now, and I think it turns into a proof that no power object exists:

Let $X$ be a petri net with two places $A$ and $B$ and a single transition from $A+B$ to $0$. Suppose it has a power object $PX$.

By considering the petri net with one place and no transitions, we see that $PX$ must have four places which I label $(\emptyset), (A), (B), (AB)$. By naturality we see that these work in the same way as the subobject classifier in Set - that is, if we have a morphism $Y \to PX$ where a place $C$ maps to $(AB)$ then the corresponding subobject of $X \times Y$ contains the places $(A,C)$ and $(B, C)$, while if $C$ mapped to $(A)$ then the subobject would contain $(A, C)$ but not $(B, C)$, etc.

Now we will show that there is no natural bijection between subobjects of $X \times X$ and morphisms $X \to PX$. Note $X \times X$ is the net with four places $(A, A), (A, B), (B, A)$ and $(B, B)$, and a transition from $(A, A) + (B, B)$ to $0$ and a transition from $(A, B) + (B, A)$ to $0$.

Let $S \rightarrowtail X \times X$ be the subobject consisting of all the places and the transition $(A, A) + (B, B)$ to $0$. Then this corresponds to some morphism $X \to PX$, and we know that this morphism takes both $A$ and $B$ to $(AB)$, and the single transition to some transition from $2(AB)$ to $0$.
But we have an automorphism of $X$ which swaps the places $A$ and $B$. Pulling back along this automorphism takes the subobject $S$ to the subobject consisting of all four places and the transition from $(A, B) + (B, A)$ to $0$. But precomposing our morphism $X \to PX$ with this automorphism does nothing! So we can't have a power object.

Thomas Read (Apr 28 2020 at 07:23):

image-27fbc39f-0ad7-4289-ae1a-dadbb2915a8f.jpg

Thomas Read (Apr 28 2020 at 07:23):

^ relevant pictures

Morgan Rogers (he/him) (Apr 28 2020 at 09:40):

Jade Master said:

Morgan Rogers interesting idea. The objects of this proposed comma category aren't really Petri nets anymore. They are Petri nets with only one place.

I wasn't putting forward $\mathrm{Set}/\mathbb{N} \times \mathbb{N}$ as the topos, but the slice of the identity of this topos over the functor $\mathbb{N}[-] \times \mathbb{N}[-]$ coming from $\mathrm{Set}$. The result is your category of Petri nets but equipped with a function $T \to \mathbb{N} \times \mathbb{N}$ that sends each transition to the sum of the coefficients on its source and target, which is data already preserved by the morphisms you describe.

Morgan Rogers (he/him) (Apr 28 2020 at 09:47):

John Baez said:

I don't know. Is this trick enough to create a topos? Jade demands a topos! :upside_down:

Unfortunately no, it still isn't enough to make Artin gluing construction work. To show that it does is equivalent to checking that the original $\mathbb{N}[-] \times \mathbb{N}[-]$ functor preserves pullbacks, which actually would be enough on its own, as mentioned in the remarks at the end of the Artin gluing page that you linked. And in fact you can check that it manages to preserve the pullback of a monomorphism along any morphism, but it fails to pullback epis against one another: a minimal counterexample is to take $X = \{A,B\}, Y = \{C,D\}, Z = \{*\}$. Then $\mathbb{N}[X \times_Z Y] \times \mathbb{N}[X \times_Z Y]$ contains elements $((A,C)+(B,D),(A,C)+(B,D))$ and $((A,D)+(B,C),(A,D)+(B,C))$ which are identified by the comparison morphism to $(\mathbb{N}[X] \times \mathbb{N}[X]) \times_{(\mathbb{N}[Z] \times \mathbb{N}[Z])} (\mathbb{N}[Y] \times \mathbb{N}[Y])$. You can probably see that I've just doubled up an argument showing that the free commutative monoid functor doesn't preserve pullbacks; if you're trying to follow the reasoning it's easier to work with that.

Daniel Cicala (Apr 28 2020 at 12:29):

Hi @Jade Master , here I am.

Jade Master (Apr 28 2020 at 14:02):

Hi @Daniel Cicala I just thought you might be interested in this conversation.

Jade Master (Apr 28 2020 at 14:07):

@Morgan Rogers yes I agree that this category isn't $\mathsf{Set}/\mathbb{N} \times \mathbb{N}$. It's just that it might as well be because the objects of this category are completely unrelated to the sets of places.

Jade Master (Apr 28 2020 at 14:08):

Oh now I think I understand what you mean.

Joe Moeller (Apr 28 2020 at 15:20):

sarahzrf said:

Joe Moeller said:

I wonder if there is any interesting Grothendieck topology one could put on this?

do you mean lawvere-tierney topology? otherwise i'm not sure what you'd mean by it restricting the objects

I just meant that a Gr topology allows you to restrict to sheaves.

Morgan Rogers (he/him) (Apr 28 2020 at 15:50):

I suppose that what I said amounts to the observation that the "sum of coefficients" maps are invariant under the given morphisms of Petri nets. Given the failure of the functor to preserve all pullbacks, it doesn't actually help show that the category is (or isn't) a topos :shrug:
@Thomas Read's description of the subobject classifier from earlier, $(\{A\},\mathbb{N}^2) \hookrightarrow (\{A,B\},\mathbb{N}^2 + \mathbb{N}^4)$ does seem to work (ie I tried to construct one and ended up with the same thing and have convinced myself it works), although I don't yet understand his proof of the non-existence of certain power objects. The only example of a subobject classifier in the wild (ie in a non-trivial non-topos) that I've seen before is in the category $$\Set_*$$ of pointed sets, so I'm quite curious to see how far this fails to be a topos, as a nice example for the future!

Daniel Cicala (Apr 28 2020 at 20:40):

Thanks for thinking of me. I'm a genuine dummy when it comes to navigating these kind of sites. What conversation do you mean? I only see Christian welcoming everybody.

sarahzrf (Apr 28 2020 at 22:00):

Joe Moeller said:

I just meant that a Gr topology allows you to restrict to sheaves.

oh, whoops, i missed the message you were originally replying to so i thought you were talking about the original probably-not-a-topos category (in which case what is even the base category to put gr topology on)

Mike Shulman (Apr 29 2020 at 05:14):

Mike Shulman said:

Generally whenever you have strict commutativity appearing, topos-like properties tend to fail. See for instance https://arxiv.org/abs/1209.0414. It could be that the example therein could be adapted to Petri.

I went back and looked at this paper and I think their counterexample should almost literally apply to show that Petri is not cartesian closed (hence, of course, not a topos). Just read their section 2 with the following dictionary:

"2-degenerate 3-computad" = "Petri net"
"2-cell" = place
"3-cell" = transition

Thomas Read (Apr 29 2020 at 06:29):

Yes, I think that works! It's interesting comparing that to my proof that there's no power object - they both centre around a similar net (in their case the net with a transition $A + B \to C$, in mine the net with a transition $A + B \to 0$), and the key point is that the product of that net with itself has two distinct transitions. But of course the rest is somewhat different - theirs is nice in that it's very concrete, whereas I had to figure out a bit about what a power object would look like supposing it existed.

Jade Master (Apr 29 2020 at 07:37):

Thank you Mike! :pray:

Morgan Rogers (he/him) (Apr 29 2020 at 09:27):

Is that the end of the story, then? Personally I would still be interested to know how far it fails with more precision (which objects are exponentiable, for example?) and if it can be built from/on top of a topos in a way that resembles some other familiar constructions.
For example, if we replace "free commutative monoid" with "free monoid", the resulting Artin gluing does give a topos, which is the category of "Petri nets with the places in the source and target of each transition ordered", and that admits a canonical functor to the category of Petri nets by forgetting the ordering. If that has an adjoint on one side or the other, it's likely to be pretty big (desymmetrizing usually involves taking a copy for each possible ordering), but whatever the situation, understanding the relationship between these categories should yield some deeper insight.

Fabrizio Genovese (Apr 29 2020 at 09:42):

What you are defining are called pre-nets. They are more or less the same thing of free symmetric strict monoidal categories. You are tapping in a big research field right now :slight_smile:

Fabrizio Genovese (Apr 29 2020 at 09:43):

And yes, this is more or less how you do the left adjoint here, you have to take any possible ordering of the places into consideration.

Morgan Rogers (he/him) (Apr 29 2020 at 10:20):

Ooh thanks for the name! In the nLab page on pre-nets there's a paper by Joyal and Street cited, The Geometry of Tensor Calculus, I. While it has been cited many times, neither they nor any of the papers citing them that I can find observe that the category of pre-nets/tensor schemes is a topos? Considering all the topos theory that Joyal has contributed to, is it really possible that this just... hasn't been noticed?

Morgan Rogers (he/him) (Apr 29 2020 at 10:25):

Or is it just that they're known by yet another name (maybe 2-computads, given the contents of Cheng's article?) wherever it's recognized that they form a topos?

Mike Shulman (Apr 29 2020 at 15:10):

I expect it's just that no one had any particular use for the fact yet. It would have been obvious to Joyal and Street that they are a (presheaf!) topos.

Mike Shulman (Apr 29 2020 at 15:11):

Thomas Read said:

they both centre around a similar net (in their case the net with a transition $A + B \to C$, in mine the net with a transition $A + B \to 0$)

They mention somewhere early on that their morphisms could also have empty codomain.

Mike Shulman (Apr 29 2020 at 15:12):

Morgan Rogers said:

Is that the end of the story, then? Personally I would still be interested to know how far it fails with more precision (which objects are exponentiable, for example?) and if it can be built from/on top of a topos in a way that resembles some other familiar constructions.

I'd like to know the answer to John's question of whether Petri is adhesive. In particular, can anyone find a pushout of a monomorphism that is not stable under pullback? Any coequalizer can of course be written as a pushout, but not in general a pushout of a monomorphism.

Jules Hedges (Apr 29 2020 at 15:15):

I'm getting concerned that "some people talked about it on Zulip in 2020" will be the new "some people talked about it at a conference in Buffalo in 1965"

Nathanael Arkor (Apr 29 2020 at 15:17):

Jules Hedges said:

I'm getting concerned that "some people talked about it on Zulip in 2020" will be the new "some people talked about it at a conference in Buffalo in 1965"

There's a major difference, in that all the messages sent on Zulip are stored permanently, so it's possible to reference conversations here. In terms of folklore, this seems like a strict improvement.

Jules Hedges (Apr 29 2020 at 15:19):

I agree it's a strict improvement, but I don't think it's a very strict improvement. My hypothetical Buffalo conference was 55 years ago, wanna bet that the links into Zulip will still be alive in 2075?

Nathanael Arkor (Apr 29 2020 at 15:20):

It'd certainly be worth trying to make sure we have regular backups, although that's a conversation for #general: meta.

Morgan Rogers (he/him) (Apr 29 2020 at 15:54):

Mike Shulman said:

I expect it's just that no one had any particular use for the fact yet. It would have been obvious to Joyal and Street that they are a (presheaf!) topos.

If it's also obvious to you, would you mind describing the category over which prenets are presheaves? Not explicitly stating something "obvious" just because one doesn't yet have a use for it seems a little selfish; after all, no one else can make the fact useful if they don't know it!

Reid Barton (Apr 29 2020 at 16:01):

Imagine one sort for objects, and for each pair $(m, n) : \mathbb{N} \times \mathbb{N}$, a sort of morphisms with $m$ inputs and $n$ outputs, and for each $1 \le i \le m$ an operation which takes such a morphism to its $i$ th input, and so on.

Morgan Rogers (he/him) (Apr 29 2020 at 16:12):

So quite a big category, then! And we need to take covariant functors to Set from the category you're describing. Then if I write $S$ for the sort of objects/places, and $T_{(m,n)}$ for the sort of transitions with $m$ inputs and $n$ outputs, then the net corresponding to a functor $F$ has places $F(S)$ and the disjoint union of the $F(T_{(m,n)})$ for transitions?

Morgan Rogers (he/him) (Apr 29 2020 at 16:20):

It probably happens the other way around for everyone else, but having this description immediately made it much clearer to me how pre-nets can constructed out of individual transitions with fixed numbers of inputs and outputs and some free places.

Mike Shulman (Apr 29 2020 at 17:59):

Well, if one states all the facts one can think of about a definition just in case someone else might have a use for them, then the paper gets rather long.

Mike Shulman (Apr 29 2020 at 18:00):

Morgan Rogers said:

So quite a big category, then!

If by "quite big" you mean "countably infinite"...

Reid Barton (Apr 29 2020 at 18:05):

Mike Shulman said:

Well, if one states all the facts one can think of about a definition just in case someone else might have a use for them, then the paper gets rather long.

Surely it would only get countably infinitely long, at most? :upside_down:

Morgan Rogers (he/him) (Apr 29 2020 at 19:17):

Mike Shulman said:

Morgan Rogers said:

So quite a big category, then!

If by "quite big" you mean "countably infinite"...

Compared with the two sets and two functions that constitute the original definition... yes! Quite big!

Todd Trimble (Apr 29 2020 at 21:35):

John Baez said:

You may recall that Daniel Cicala used "Artin gluing" to get a lot of topoi as comma categories: if $E$ and $F$ are topoi and $u : E \to F$ preserves finite limits, the comma category $\mathrm{id}_F/u$ is a topos.

It's actually a little better than that: you only need $u:E \to F$ to preserve pullbacks. This strengthening occasionally comes in handy (for example, the pre-nets example).

John Baez (Apr 29 2020 at 22:37):

Oh, interesting! In one nLab article it said "pullback-preserving", but then in the article on Artin gluing it said "finite-limit preserving", so I corrected the "pullback-preserving" one. And I considered leaving y'all a note but I didn't.

John Baez (Apr 29 2020 at 22:38):

I'll fix that...

Todd Trimble (Apr 29 2020 at 23:46):

Just to add some detail: the Artin gluing along $u: E \to F$ is the category of coalgebras of a pullback-preserving comonad on the topos $E \times F$, taking $(e, f): E \times F$ to $(e, u(e) \times f): E \times F$. This is indeed pullback-preserving if $u$ is. The classic result about the category of coalgebras of a lex comonad can be strengthened by replacing "lex" by "pullback-preserving"; see Johnstone's Elephant, A.4.2.3. Or, to toot my own horn, see here.

Jade Master (Apr 30 2020 at 18:55):

@Mike Shulman Fact 4.21 of this book shows that $\mathsf{Petri}$ is a weak adhesive HLR category. I don't really understand weak adhesive HLR categories but it seems like a weaker version of being adhesive.

Jade Master (Apr 30 2020 at 18:56):

The point of this according to the book I linked is that that you can do double pushout rewriting in $\mathsf{Petri}$

Todd Trimble (Apr 30 2020 at 18:57):

Can you write out the definition of weak adhesive HLR category? I don't know what HLR means.

Jade Master (Apr 30 2020 at 19:16):

Sure.
A Category C is a weak adhesive HLR category with morphism class M if

• M is a class of monomorphisms closed under isomorphism, composition, and decomposition.
• C has pushouts and pullbacks of M-morphisms and M is closed under pushouts and pullbacks
• Pushouts in C under M-morphisms are weak VK squares.

Fabrizio Genovese (Apr 30 2020 at 19:17):

So who's M in the case of Petri nets?

Jade Master (Apr 30 2020 at 19:23):

M is the class of injective morphisms

Jade Master (Apr 30 2020 at 19:23):

I assume that means morphisms where each component is injective.

Jade Master (Apr 30 2020 at 19:23):

Btw I am not understanding this stuff yet :) I am just quoting the book

Fabrizio Genovese (Apr 30 2020 at 19:24):

I was asking because in your definition it seems that M is a parameter, so it can be everything you want, right?

Jade Master (Apr 30 2020 at 19:25):

Fact 4.21 proves that Petri satisfies these properties when M is the class of injective morphisms.

Jade Master (Apr 30 2020 at 19:25):

In general these categories can have any class of morphisms satisfying these properties though.

Fabrizio Genovese (Apr 30 2020 at 19:26):

Jade Master said:

Fact 4.21 proves that Petri satisfies these properties when M is the class of injective morphisms.

Now I get it :D

Todd Trimble (Apr 30 2020 at 19:37):

Thanks. Sorry for dumb questions, but I don't know what VK means, much less what a weak VK square is. Not sure what "closed under decomposition" means here. What does HLR stand for, please?

John Baez (Apr 30 2020 at 19:44):

VK must be "van Kampen"

Morgan Rogers (he/him) (Apr 30 2020 at 19:51):

Todd Trimble said:

Thanks. Sorry for dumb questions, but I don't know what VK means, much less what a weak VK square is. Not sure what "closed under decomposition" means here. What does HLR stand for, please?

Not a dumb question. I'm in the same boat. Out of context initialisms are always a recipe for confusion, and being closed under decomposition could mean one of four things to me (there's a "left" version, a "right" version, a "both" version, and an "either" version that come to mind), so I would like to second the request for clarification.

Reid Barton (Apr 30 2020 at 19:53):

In the second bullet point, I assume the second "C" should be "M"?

Todd Trimble (Apr 30 2020 at 19:54):

John Baez said:

VK must be "van Kampen"

Oh, yes. Should have thought of that.

Jade Master (Apr 30 2020 at 19:59):

Closed under composition means that for $f,g \in M$, then $g \circ f \in M$ whenever defined.

Jade Master (Apr 30 2020 at 20:00):

Reid Barton said:

In the second bullet point, I assume the second "C" should be "M"?

Yes you are correct.

Todd Trimble (Apr 30 2020 at 20:03):

Jade Master said:

Closed under composition means that for $f,g \in M$, then $g \circ f \in M$ whenever defined.

That one I knew. "Closed under decomposition" was what I was unsure about.

Jade Master (Apr 30 2020 at 20:03):

Todd Trimble said:

Thanks. Sorry for dumb questions, but I don't know what VK means, much less what a weak VK square is. Not sure what "closed under decomposition" means here. What does HLR stand for, please?

I would recommend reading the book I linked as I don't understand this all yet myself. On page 86 it says this:

The main difference between adhesive HLR categories and adhesive categories is that a distinguished class M of monomorphisms is considered instead of all monomorphisms, so that only pushouts along M-morphisms have to be VK squares. Moreover, only pullbacks along M-morphisms, not over arbitrary morphisms, are required

Jade Master (Apr 30 2020 at 20:04):

Todd Trimble said:

Jade Master said:

Closed under composition means that for $f,g \in M$, then $g \circ f \in M$ whenever defined.

That one I knew. "Closed under decomposition" was what I was unsure about.

I am confused a bit about this too. The book says that it means $g \circ f \in M \implies g \in M, f \in M$.

Jade Master (Apr 30 2020 at 20:04):

But I don't see how this could be well defined.

Jade Master (Apr 30 2020 at 20:05):

btw HLR stands for high-level replacement.

Reid Barton (Apr 30 2020 at 20:06):

That seems unlikely to be satisfied in practice (e.g., for M = monos in Set)

Todd Trimble (Apr 30 2020 at 20:07):

Well, what I can see from Google books is somewhat limited. I can maybe piece together "weak VK square" though. A little awkward to discuss here because it really helps to see the commutative cubes under discussion.

Yes, that seems like an entirely weird definition to make for decomposition.

"High-level replacement" -- thanks.

I'm pretty far from being enlightened, but I guess we're all in that boat at the moment.

Jade Master (Apr 30 2020 at 20:09):

Oh I made a mistake. The book says that $g \circ f \in M$ and $g \in M$ implies that $f \in M$. That makes more sense.

Todd Trimble (Apr 30 2020 at 20:09):

Ah, there we go. Thanks.

Jade Master (Apr 30 2020 at 20:10):

Also @Todd Trimble 2006_Book_FundamentalsOfAlgebraicGraphTr.pdf here's a pdf.

Jade Master (Apr 30 2020 at 20:11):

and for anyone else who wants to know what the heck I'm talking about.

Todd Trimble (Apr 30 2020 at 20:12):

Thanks!

Jade Master (Apr 30 2020 at 20:18):

vksquare.png weakadhesive.png

Todd Trimble (Apr 30 2020 at 20:25):

Just a little piece of terminology, which might come in handy: the condition that a functor T preserves pullbacks of monos is called "tautness". You might like this, Jade, as any analytic functor (coming from a Joyal species) is taut. That would appear to be a key feature in the proof of Fact 4.2.1. It's generally an important concept (one resonance for me is the way it features in Paul Taylor's theory of induction/recursion, which ought to be better known).

Todd Trimble (Apr 30 2020 at 20:36):

But I'm sorry: what did you want to use adhesiveness for, Jade?

Todd Trimble (Apr 30 2020 at 20:52):

Mike Shulman said:

Morgan Rogers said:

Is that the end of the story, then? Personally I would still be interested to know how far it fails with more precision (which objects are exponentiable, for example?) and if it can be built from/on top of a topos in a way that resembles some other familiar constructions.

I'd like to know the answer to John's question of whether Petri is adhesive. In particular, can anyone find a pushout of a monomorphism that is not stable under pullback? Any coequalizer can of course be written as a pushout, but not in general a pushout of a monomorphism.

So to get back to this, armed with the pdf that Jade provided, there seems to be an example on page 94. (I haven't absorbed this myself.)

Todd Trimble (Apr 30 2020 at 21:02):

Morgan Rogers said:

Mike Shulman said:

I expect it's just that no one had any particular use for the fact yet. It would have been obvious to Joyal and Street that they are a (presheaf!) topos.

If it's also obvious to you, would you mind describing the category over which prenets are presheaves? Not explicitly stating something "obvious" just because one doesn't yet have a use for it seems a little selfish; after all, no one else can make the fact useful if they don't know it!

So I expect one could get enlightenment here by reading the Carboni-Johnstone paper "Connected limits, familial representability and Artin glueing". Don't have details immediately to hand, but might be able to rummage them up in a bit.

Todd Trimble (Apr 30 2020 at 21:11):

Anyway, it must be reminiscent of $Set^{C^{op}}/F \simeq Set^{(C/F)^{op}}$ where the exponent on the right refers to the category of elements of $F$.

(Oh sorry, I see this was already answered by Reid Barton.)

John Baez (Apr 30 2020 at 21:17):

Todd wrote:

But I'm sorry: what did you want to use adhesiveness for, Jade?

Maybe Jade wants to use adhesiveness for rewriting Petri nets - "double pushout writing", to be specific. That's what Lack and Sobocinski invented adhesive categories for. My student @Daniel Cicala put some time into studying them, since his thesis Rewriting Structured Cospans was about this sort of thing. Appendix A5 in his thesis defines adhesive categories, and he says there that people use HLRS to mean "high-level replacement system" - a concept he gives the definition of.

(I dislike acronyms, myself. They save the writer a short time and make everyone else spend time looking them up.)

Jade Master (May 01 2020 at 00:40):

Yes that indeed is what I'm interested in.

Todd Trimble (May 01 2020 at 12:10):

Since Morgan gave an encouraging sign, I'll say more: if $T: Set^{C^{op}} \to Set^{D^{op}}$ preserves wide pullbacks (I'll write $T: \hat{C} \to \hat{D}$ instead), then the Artin gluing $\hat{D} \downarrow T$ is equivalent to the category of presheaves on a category sometimes referred to as a collage, $\mathbf{Coll}(T)$. Spelling this out: for each object $d: D$, the composite functor

$\hat{C} \stackrel{T}{\to} \hat{D} \stackrel{eval_d}{\to} Set,$

taking $F: \hat{C}$ to the set $T(F)(d)$, also preserves wide pullbacks, and also lifts through the forgetful functor $\Sigma: Set/T(1)(d) \to Set$ (consider, for any presheaf $F: Set^{C^{op}}$, the unique map $!: F \to 1$, which gives a map $T(F)(d) \to T(1)(d)$, i.e., an object of $Set/T(1)(d)$). Notice that this lift preserves wide pullbacks and the terminal object $1$, so preserves all limits, hence has a left adjoint $Set/T(1)(d) \to \hat{C}$, given by a family of presheaves $\{W_{(d, x)}: C^{op} \to Set\}_{x\in T(1)(d)}$. So $T$ takes a presheaf $F: C^{op} \to Set$ to a presheaf of the form $d \mapsto \sum_{x \in T(1)(d)} \hat{C}(W_{(d, x)}, F)$ (one says $T$ is familially representable).

Thus an object in $\hat{D} \downarrow T$ consists of a presheaf $F: C^{op} \to Set$, a presheaf $G: D^{op} \to Set$, and a family of maps

$G(d) \to \sum_{x \in T(1)(d)} \hat{C}(W_{(d, x)}, F)$

natural in $d$. These data taken together may be construed as a presheaf on a category $\mathbf{Coll}(T)$, which is something like a "graph" of a functor, or a fancy version of an ordinal sum in the sense of a paper by Lawvere. The objects are objects $c: C$ and pairs $(d: D, x \in T(1)(d))$. A morphism between objects of $C$ in $\mathbf{Coll}(T)$ is a morphism in $C$, a morphism of type $(d, x) \to (d', x')$ is a morphism $g: d \to d'$ in $D$ such that $(T(1)(g))(x') = x$ (so basically a Grothendieck construction), and a morphism of type $c \to (d, x)$ is an element in the set $W_{(d, x)}(c)$. There are no morphisms $(d, x) \to c$ in the other direction. The composition law is the obvious thing.

Daniel Cicala (May 01 2020 at 12:12):

Hi Jade, here are a few thoughts. In building a bi/double category where rewrites of structured cospans are the 2-arrows, the primary obstruction is getting certain spans (rewrite rules) of cospans (open Petri nets) to satisfy the interchange law. For this to work, it's not strictly necessary for Petri nets to form a topos. Here are two possible dodges.

(1) Instead of forming a topos, Petri nets can be regular, adhesive, and locally cartesian closed (i.e. all over-categories are cartesian closed). I talk about how these properties are sufficient for interchange in Section 3 of my paper Spans of Cospans (sorry for the self-promotion and not linking, I don't know how to link here but you can search arXiv or TAC). In this scenario, your 2-arrows are up-to-iso meaning that you can distinguish between different rewrite rules that have the same effect (rewrite A to B).

(2) If you don't care about distinguishing between different rewrites from A to B, then you can use what I called Bold Rewriting in Ch.4 of my thesis (Rewriting Structured Cospans on the arXiv). Here, you only need Petri nets to be nice enough to rewrite (adhesive, quasi-adhesive, high level replacements systems) and have enough limits and colimits. Bold rewriting takes 2-arrows to be connected components instead of isomorphisms. Here, interchange boils down to the existence of the canonical arrow colim lim --> lim colim (pushouts and pullbacks commute "laxly"? "lackadaisically"?). If you're working in a bicategory (inputs and outputs remain fixed during rewrites) instead of a double category (inputs and outputs can be permuted) then bold rewriting gets you a bicategory of relations, which is nice.

Todd Trimble (May 01 2020 at 12:14):

Jade Master said:

Yes that indeed is what I'm interested in.

Thanks! And thanks to John for supplying some context. In the past I'd only looked briefly at adhesive categories, mainly for "pure" reasons (it's a useful exactness property, after all), but now I'm motivated to understand the, um, motivation!

Morgan Rogers (he/him) (May 01 2020 at 13:08):

Todd Trimble said:

The objects are objects $c: C$ and pairs $(d: D, x \in T(1)(d))$. A morphism between objects of $C$ in $\mathbf{Coll}(T)$ is a morphism in $C$, a morphism of type $(d, x) \to (d', x')$ is a morphism $g: d \to d'$ in $D$ such that $(T(1)(g))(x') = x$ (so basically a Grothendieck construction), and a morphism of type $c \to (d, x)$ is an element in the set $W_{(d, x)}(c)$. There are no morphisms $(d, x) \to c$ in the other direction. The composition law is the obvious thing.

Thanks for expanding on this, understanding how and when a construction on presheaf/Grothendieck toposes gives another presheaf/Grothendieck topos is very enlightening. This collage category was a lot easier to parse thanks to my participation in a discussion between @sarahzrf and @Fabrizio Genovese on profunctors in optics: after composing with the Yoneda embedding on one side and the functor to the slice category over $T(1)$ on the other, a functor $T: \hat{C} \to \hat{D}$ becomes a functor $C \to \mathrm{PSh}(\int T(1))$, where $\int T(1)$ is the category of elements/Grothendieck construction for $T(1)$. After currying, this becomes a profunctor whose collage (in the profunctor sense) is exactly the category you describe. I take it left exactness is needed in a way that is not immediately obvious in order to get the equivalence between the presheaves over $\mathbf{Coll}(T)$ and the comma category $(1_{\hat{D}} \downarrow T)$, but I at least have some grip on where this construction comes from :grinning_face_with_smiling_eyes:

Morgan Rogers (he/him) (May 01 2020 at 13:14):

Daniel Cicala said:

I talk about how these properties are sufficient for interchange in Section 3 of my paper Spans of Cospans (sorry for the self-promotion and not linking, I don't know how to link here but you can search arXiv or TAC).

You can just paste the link directly, or use square bracketed text followed up by round bracketed web address,

[text](link address)

to make hyperlinked text. Your referenced papers are here, and here... I think! You have several papers with similar names which come up when searching.

Todd Trimble (May 01 2020 at 13:48):

I wasn't able to get my hands on Carboni-Johnstone, so I can't remember exactly how they go about it, but I was able to piece together what I wrote by recalling some stuff I had written in the nLab on connected limits and wide pullbacks (by the way, in case it wasn't clear, these wide pullbacks include the infinitary case as well: diagrams having one target and infinitely many sources, with one arrow from each source to the target, and no other arrows. If a category has a terminal object and wide pullbacks, then it is small-complete) -- and also, by cribbing from Tom Leinster's book, section C.3, which you might well find easier to read than what I put down here. The Carboni-Johnstone article is well worth having a look at (with little enjoyable nuggets, for example a functor that preserves finite pullbacks must preserve equalizers as well).

dusko (May 09 2020 at 05:48):

Todd Trimble said:

a functor that preserves finite pullbacks must preserve equalizers as well).

it seems like a nice exercise to reverse engineer the minimal assumptions for that. there seem to be finite counterexamples for the statement without any assumptions. if the category is monoidal and has the diagonals, then the equalizer of f and g is the pullback of <f,g> along the diagonal. but a functor that does not preserve the terminal object may preserve all pullbacks but not the diagonal. but the diagonal is the equalizer of the identity and the symmetry. what am i missing? is there a way to express the equalizers in terms of pullbacks without using the diagonals?

Todd Trimble (May 09 2020 at 06:44):

Suppose $C$ has finite limits. The claim is that a functor $F: C \to D$ preserves equalizers if it preserves pullbacks. I thought a proof went as follows. A functor $F: C \to D$ preserves the limit of a functor $W: J \to C$ iff $\hom(d, F-): C \to Set$ also preserves that limit for every object $d$ of $D$, so it suffices to prove the claim in the case $D = Set$. Suppose $F: C \to Set$ preserves pullbacks. There is a lift $\tilde{F}: C \to Set/F(1)$ of $F$ through the forgetful functor $\Sigma: Set/F(1) \to Set$, taking $c$ in $C$ to $F(!): F(c) \to F(1)$. Since $\Sigma: Set/F(1) \to Set$ preserves and reflects pullbacks, and $F$ preserves pullbacks by assumption, $\tilde{F}$ also preserves pullbacks, as well as the terminal object by construction, so it preserves all finite limits. Then $F \cong \Sigma \tilde{F}$ preserves equalizers since $\Sigma$ preserves equalizers.

Todd Trimble (May 09 2020 at 06:53):

See also Paré's paper here, page 742.

dusko (May 18 2020 at 07:53):

Todd Trimble said:

Suppose $C$ has finite limits. The claim is that a functor $F: C \to D$ preserves equalizers if it preserves pullbacks. I thought a proof went as follows. A functor $F: C \to D$ preserves the limit of a functor $W: J \to C$ iff $\hom(d, F-): C \to Set$ also preserves that limit for every object $d$ of $D$, so it suffices to prove the claim in the case $D = Set$. Suppose $F: C \to Set$ preserves pullbacks. There is a lift $\tilde{F}: C \to Set/F(1)$ of $F$ through the forgetful functor $\Sigma: Set/F(1) \to Set$, taking $c$ in $C$ to $F(!): F(c) \to F(1)$. Since $\Sigma: Set/F(1) \to Set$ preserves and reflects pullbacks, and $F$ preserves pullbacks by assumption, $\tilde{F}$ also preserves pullbacks, as well as the terminal object by construction, so it preserves all finite limits. Then $F \cong \Sigma \tilde{F}$ preserves equalizers since $\Sigma$ preserves equalizers.

sorry i disappeared. your proof looks complicated. since my example is simpler, maybe you could try to reconcile what we are saying, and whether we agree or disagree.

a functor that preserves pullbacks also preserves the equalizers if and only if it preserves the diagonals ((because every diagonal is an equalizer, and because every equalizer is a pullback of a diagonal)).

a functor that preserves pullbacks must preserve every diagonal $x \to x\times x$ ((because $x$ is a pullback of the identities, and $x\times x$ is a pullback of $x\to 1$, and $x \to x\times x$ factors one through the other)).

am i missing anything?

Todd Trimble (May 20 2020 at 20:56):

I'm sorry, dusko, but seeing how my taking the trouble to give a proof to settle a doubt is met with "your proof looks complicated" is just a little off-putting to me. Let's please not recreate a one-upmanship dynamic often seen on the categories list.

(Btw, I don't claim priority for the proof; it's probably much the same as you might find in Carboni-Johnstone. I do find it memorable -- it connects with the theme of parametrized right adjoints. And it's not that hard.)

By "reconcile what we are saying [using an example originally intended to demonstrate that something was wrong]" and "whether we agree or disagree", I can't tell if you're still claiming that something's wrong, or if you now agree that the statement is true (that if $C$ has finite limits and $F: C \to D$ preserves pullbacks, then it preserves equalizers) and you want me to certify an alternative proof of yours that you like more. I'll guess the latter.

It's not immediately clear what you intend "preserves the diagonals" to mean. Take for example a functor $X \times -: Set \to Set$. This preserves pullbacks. It takes a diagonal $Y \to Y \times Y$ to $X \times Y \to X \times Y \times Y$. The latter is not a diagonal in the ordinary sense. It can be interpreted as a diagonal in a slightly more subtle fiber-product-y sense, of course. But then one has to go back and re-examine the glib argument in that light. If you are missing anything -- I don't know whether you are or not -- could it be in not acknowledging that non-preservation of products and of the terminal object mentioned in your last paragraph makes the argument (which recalls how one gets equalizers by pulling back ordinary diagonals) slightly more complicated? Running it through my head without writing anything down, I'm guessing it all works out fine, after making some necessary adjustments. Does that settle the matter?

John Baez (Jul 31 2020 at 00:07):

I'm trying to work out some details here:

[Mod] Morgan Rogers said:

For example, if we replace "free commutative monoid" with "free monoid", the resulting Artin gluing does give a topos, which is the category of "Petri nets with the places in the source and target of each transition ordered", and that admits a canonical functor to the category of Petri nets by forgetting the ordering.

John Baez (Jul 31 2020 at 00:44):

Let $S^\ast$ be the underlying set of the free monoid on the set $S$ - the set of words in $S$. Let $F: \mathsf{Set} \to \mathsf{Set}$ be the obvious functor sending $S$ to $S^\ast \times S^\ast$.

John Baez (Jul 31 2020 at 00:44):

Let's form the comma category $1_{\mathsf{Set}} \downarrow F$.

John Baez (Jul 31 2020 at 00:45):

I think this is the category of pre-nets.

John Baez (Jul 31 2020 at 00:46):

An pre-net is a pair of sets $(T,P)$ together with functions $s,t \colon T \to P^\ast$. We can write the pre-net simply as

$s,t \colon T \to P^\ast$

John Baez (Jul 31 2020 at 00:47):

So yes, a pre-net is an object of $1_{\mathsf{Set}} \downarrow F$.

John Baez (Jul 31 2020 at 00:49):

Given pre-nets $s,t \colon T \to P^\ast$ and $s',t' \colon T' \to P'^\ast$, a morphism of pre-nets from the first to the second is a function $f: T \to T'$ and a function $g: P \to P'$ making the two squares you can draw with this data both commute.

John Baez (Jul 31 2020 at 00:49):

So yes, a morphism of pre-nets is a morphism in $1_{\mathsf{Set}} \downarrow F$.

John Baez (Jul 31 2020 at 00:50):

Now I'm going to show $1_{\mathsf{Set}} \downarrow F$ is a topos, using Artin gluing.

John Baez (Jul 31 2020 at 00:52):

I'll use this result: if $E$ and $F$ are topoi and $u : E \to F$ preserves pullbacks, the comma category $\mathrm{id}_F/u$ is a topos.

John Baez (Jul 31 2020 at 00:55):

To do this, I just need to check that $F$ preserves pullbacks. (This doesn't preserve finite limits since it doesn't preserve the terminal object.)

John Baez (Jul 31 2020 at 01:07):

Okay, I just checked by hand that the "underlying set of the free monoid" functor $S \mapsto S^\ast$ preserves pullbacks.

John Baez (Jul 31 2020 at 01:08):

(What's a nice general result that implies this?)

John Baez (Jul 31 2020 at 01:09):

Since pullbacks are computed pointwise, this implies that the functor from $\mathsf{Set}$ to $\mathsf{Set}^2$ sending $S$ to $(S^\ast, S^\ast)$ preserves pullbacks.

John Baez (Jul 31 2020 at 01:11):

The functor $\times : \mathsf{Set}^2 \to \mathsf{Set}$ preserves pullbacks because it's right adjoint to the diagonal. So, $L$ with $L(S) = S^\ast \times S^\ast$ preserves pullbacks, and we're done!

Dan Doel (Jul 31 2020 at 01:11):

Lists are like $Σn. S^n$, so is that Beck-Chevalley together with $-^n$ being a right adjoint?

John Baez (Jul 31 2020 at 01:13):

I don't get that... how do you use Beck-Chevalley to show something preserves pullbacks? I see that $S \mapsto S^n$ preserves pullbacks.

John Baez (Jul 31 2020 at 01:14):

I'm not very good at this stuff, you may be perfectly right.

Dan Doel (Jul 31 2020 at 01:20):

I think I might be wrong. Beck-Chevalley might be about the wrong pullback.

Tobias Fritz (Jul 31 2020 at 01:21):

This is about the underlying functor of the free monoid monad preserving pullbacks, right? Then this is part of the statement that the free monoid monad is a cartesian monad. A more general statement is that every monad that comes from a non-symmetric operad is cartesian. This is Example 4.1.6 in Higher Operads, Higher Categories.

I haven't followed this thread, but is the way in which this comes up related to $T$-multicategories?

John Baez (Jul 31 2020 at 01:28):

Okay, "cartesian monad" is the generalization I want. I found that concept overly subtle the first dozen times I met it. I think I'm slowly getting why it's cool.

Yes, there's some connection between T-multicategories and what I'm talking about right now. One difference is that a morphism in a T-multicategory has a "T-thing of inputs and one output", very loosely speaking, while a transition in a pre-net has a "finite ordered set of inputs and a finite ordered set of outputs".

John Baez (Jul 31 2020 at 01:28):

There are people who have generalized T-multicategories to allow multi-input, multi-output situations. Probably Mike Shulman is one?

Mike Shulman (Jul 31 2020 at 02:06):

John Baez said:

There are people who have generalized T-multicategories to allow multi-input, multi-output situations.

Really? I've been saying for a while that someone should do this, but I've never seen it done.

Mike Shulman (Jul 31 2020 at 02:14):

The closest thing I know of in the literature is Garner's paper "Polycategories via pseudo-distributive laws" that suggests how such a thing should go -- instead of one monad you have two, one for the inputs and one for the outputs, with some kind of distributive law between them.

John Baez (Jul 31 2020 at 03:12):

Hmm. If you don't think anyone has done general "(T,T')-polycategories" yet, you must be right.