Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: learning: questions

Topic: Is the Grothendieck construction adhesive?


view this post on Zulip Jade Master (Feb 27 2022 at 11:56):

Suppose that CC is an adhesive category and F:CCatF: C \to Cat is a pseudofunctor such that F(c)F(c) is an adhesive category for all objects c of C. Then is the total category of the Grothendieck construction F\int F an adhesive category?

view this post on Zulip Jade Master (Feb 27 2022 at 11:57):

Maybe I also need for the functors F(f)F(f) for morphisms f of C, to be structure preserving in some way...but I'm not sure exactly what.

view this post on Zulip Jade Master (Feb 27 2022 at 17:29):

Hi, just to give my motivation for thinking about this question. If you ignore the blue in this picture it's a standard application of a double pushout rule (top row) to graph on the bottom left. It's done in two steps, first find the pushout complement (bottom middle) and then take the pushout (bottom right) to get the result. doublepushout.png.

view this post on Zulip Jade Master (Feb 27 2022 at 17:30):

The blue circles represent tokens or a specific state of the graph. So maybe they represent specific instances of a resource.

view this post on Zulip Jade Master (Feb 27 2022 at 17:32):

So reading the top row, the production rule carries the states with them, but also tokens can change dynamically as part of the rule. So you can see in the picture that on the top right, the rightmost blue token travels along a green arrow in the application of the rule to give a new state on the new graph that is being rewritten to. When you perform these rewrites to the larger graph, then mostly the tokens just go along for the ride, but also the dynamics or changes in token must be accounted for as well.

view this post on Zulip Jade Master (Feb 27 2022 at 17:38):

How can we represent this mathematically? Well first consider the free category functor F:GrphCat F : Grph \to Cat sending a graph GG to the category F(G)F(G) whose objects are vertices of G and morphisms are either identity arrows or finite sequences of composable edges...it's the standard construction. To do rewriting we will need to be able to take pushouts at the very least but there's a problem because F(G) does not usually have pushouts. What's the solution? Freely complete F(G) to SetF(G)Set^{F(G)}. An object m:F(G)Setm : F(G) \to Set of this free cocompletion I am thinking of as a marking of state, for each object x in F(G), m(x)m(x) is like the set of tokens which live above the state x.

view this post on Zulip Jade Master (Feb 27 2022 at 17:41):

So after taking free cocompletion, you have a functor Set()FSet^{(-)} \circ F and I think the Grothendieck construction Set()F\int Set^{(-)} \circ F may be an appropriate setting to do double pushout graph rewriting of these stateful graphs. If this Grothendieck construction is an adhesive category, then everything should work okay to get a well-behaved rewriting system.

view this post on Zulip Jade Master (Feb 27 2022 at 17:42):

This is a half developed mathematical idea...I'm not sure all the details make sense but I hope that this makes a little bit of sense.

view this post on Zulip Jade Master (Feb 27 2022 at 17:44):

I'm a little bit worried about functors, m:F(G)Setm : F(G) \to Set actually being like markings...defining their value on morphisms might be a bit much. But anyway I'm done rambling for now.

view this post on Zulip Fabrizio Genovese (Feb 27 2022 at 22:03):

I don't know the answer to your question, but what would be the interpretation of markings in a graph-theoretic context? Graphs are often used as the underlying structure representing a state machine, but usually only one state of the machine is marked, as concurrency is not considered

view this post on Zulip Morgan Rogers (he/him) (Feb 28 2022 at 07:43):

If C and F(c) have a give class of limits and the functors F(f) preserve them then the Grothendieck construction will have those limits. For pullbacks, say, the pullback of (u,f) along (v,g) is obtained by computing the pullback of f and g in C, pulling back u and v along the respective components, and then pulling back the results along one another in the common fibre.
The only analogous general result for colimits that I know of requires the functors F(f) to have left adjoints, and the colimits are constructed by transporting along these instead.

If you happen to have those rather strong conditions in place, then adjointness should enable you to prove that the adhesive structure lifts to the Grothendieck construction too. Otherwise, you'll need to do some more hands-on work.

view this post on Zulip Jade Master (Feb 28 2022 at 10:03):

Fabrizio Genovese said:

I don't know the answer to your question, but what would be the interpretation of markings in a graph-theoretic context? Graphs are often used as the underlying structure representing a state machine, but usually only one state of the machine is marked, as concurrency is not considered

That's true. Thanks. I haven't really decided on an interpretation yet but the formalism sort of requires multiple tokens. If you take the coproduct of two tokens, it has to be something like their superposition? Maybe this should represent non-deterministic branching of the state machine. On the other hand, you could probably use Petri nets instead for this whole setup and then the concurrency would be more natural.

view this post on Zulip Jade Master (Feb 28 2022 at 10:05):

Morgan Rogers (he/him) said:

If C and F(c) have a give class of limits and the functors F(f) preserve them then the Grothendieck construction will have those limits. For pullbacks, say, the pullback of (u,f) along (v,g) is obtained by computing the pullback of f and g in C, pulling back u and v along the respective components, and then pulling back the results along one another in the common fibre.
The only analogous general result for colimits that I know of requires the functors F(f) to have left adjoints, and the colimits are constructed by transporting along these instead.

If you happen to have those rather strong conditions in place, then adjointness should enable you to prove that the adhesive structure lifts to the Grothendieck construction too. Otherwise, you'll need to do some more hands-on work.

Oh that's interesting. I didn't realize that colimits were harder to transport along Grothendieck than limits...adhesive requires both. I suppose that for pushouts the trick you described doesn't work?

view this post on Zulip Morgan Rogers (he/him) (Feb 28 2022 at 11:19):

One path to extract results for the more general situation would be to apply the arguments I described to geometric morphisms between categories of presheaves on the fibres? We can discuss this in DMs if you like, but I expect @Joe Moeller will be able to make some helpful remarks here

view this post on Zulip Fabrizio Genovese (Feb 28 2022 at 23:57):

Jade Master said:

Fabrizio Genovese said:

I don't know the answer to your question, but what would be the interpretation of markings in a graph-theoretic context? Graphs are often used as the underlying structure representing a state machine, but usually only one state of the machine is marked, as concurrency is not considered

That's true. Thanks. I haven't really decided on an interpretation yet but the formalism sort of requires multiple tokens. If you take the coproduct of two tokens, it has to be something like their superposition? Maybe this should represent non-deterministic branching of the state machine. On the other hand, you could probably use Petri nets instead for this whole setup and then the concurrency would be more natural.

I was thinking along these lines, doing this using monoidal categories seems more natural application-wise :smile:

view this post on Zulip Fabrizio Genovese (Mar 01 2022 at 00:01):

Jade Master said:

How can we represent this mathematically? Well first consider the free category functor F:GrphCat F : Grph \to Cat sending a graph GG to the category F(G)F(G) whose objects are vertices of G and morphisms are either identity arrows or finite sequences of composable edges...it's the standard construction. To do rewriting we will need to be able to take pushouts at the very least but there's a problem because F(G) does not usually have pushouts. What's the solution? Freely complete F(G) to SetF(G)Set^{F(G)}. An object m:F(G)Setm : F(G) \to Set of this free cocompletion I am thinking of as a marking of state, for each object x in F(G), m(x)m(x) is like the set of tokens which live above the state x.

Now that I read this better I have noticed something else. Usually the double pushout construction is performed in the category of graphs and their morphisms, which as you mention is Adhesive. But what is the meaning of performing rewriting in the free category generated by a graph? In this case we aren't rewriting the graph itself but its history, I guess

view this post on Zulip Fabrizio Genovese (Mar 01 2022 at 00:04):

So, if I understand things correctly, you basically want to define a double pushout rewriting framework for "marked graphs", where a "marked graph" is basically a graph together with some notion of marking or "state". Have you tried working in a category where objects are marked graphs, so for instance couples (G,f)(G, f) with ff a morphism of F(G)F(G), the free cat generated by GG?

view this post on Zulip Fabrizio Genovese (Mar 01 2022 at 00:06):

Since a morphism of graphs GHG \to H sends vertexes and edges of GG to vertexes and edges of HH preserving source and targets, you should also be able use this definition to define morphisms (G,g)(H,h)(G,g) \to (H,h) as morphisms ff sending GG to HH and such that applying ff to each component of the list gg gives you the list hh

view this post on Zulip Fabrizio Genovese (Mar 01 2022 at 00:08):

I am not sure if this category is adhesive or if it does what you are looking for, but checking adhesivity now is "just" a matter of seeing what happens on the second component of the couple, I guess...

view this post on Zulip Jade Master (Mar 03 2022 at 11:45):

Fabrizio Genovese said:

So, if I understand things correctly, you basically want to define a double pushout rewriting framework for "marked graphs", where a "marked graph" is basically a graph together with some notion of marking or "state". Have you tried working in a category where objects are marked graphs, so for instance couples (G,f)(G, f) with ff a morphism of F(G)F(G), the free cat generated by GG?

What is the interpretation of this? In my setup you mark the vertices but in yours the markings are sequences of edges or identity arrows.

view this post on Zulip Fabrizio Genovese (Mar 04 2022 at 23:15):

Yes, my interpetation is that ff is an execution. The market state would be its codomain

view this post on Zulip Fabrizio Genovese (Mar 04 2022 at 23:15):

But I guess you can use objects as well. Recently I was working with @fosco and @Daniele Palombi on decorating graphs with their own executions, so I intuitively thought about that

view this post on Zulip Fabrizio Genovese (Mar 04 2022 at 23:17):

If you use objects more or less the deifnition of morphisms works the same way, you can still use the morphism between graphs to carry the marking along (or the markingS, if for instance you choose to decorate the graph with, say, a multiset on its vertexes)

view this post on Zulip John Baez (Mar 04 2022 at 23:31):

Fabrizio Genovese said:

Yes, my interpetation is that ff is an execution. The market state would be its codomain

Marking? It sounds like you've been studying too much economics. :upside_down:

view this post on Zulip Fabrizio Genovese (Mar 05 2022 at 16:07):

Lol, you are right. Maybe all these grim economic war forecasts are influencing me!