Category Theory
Zulip Server
Archive

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

Stream: theory: category theory

Topic: ✔ Free colored PROP on sets of objects and morphisms

Jean-Baptiste Vienney (Jul 21 2023 at 00:34):

Suppose that we have a set $\mathcal{A}$. Define the set of words $\mathcal{A}^{\otimes}:=\{a_1 \otimes ... \otimes a_n \quad n \ge 1\quad a_1,...,a_n \in \mathcal{A}\} \cup \{\epsilon\}$. Now, suppose for every two words $u,v \in \mathcal{A}^{\otimes}$, we have a set $\mathcal{A}[u,v]$. I want to define the free colored PROP with set of colors $\mathcal{A}$ and sets of generating morphisms $\mathcal{A}[u,v]$. This is obtained by considering grids of morphisms in $\mathcal{A}[u,v] \cup \{ swap_{u,v}: u \otimes v \rightarrow v \otimes u\}$ (where $swap_{u,v}$ is just a symbol, which will give the exchanges) (not exactly grids because you can have a line with 5 cells, then a line with 3 cells and then a line with 7 cells for instance, if they compose). Then you must quotient your grids by the appropriate equivalence relation to obtain a colored PROP.

Is this construction described somewhere ? I want to use this setting to make some math (I mean something more like algebra) but I would prefer if these construction of "grids" is already described by somewhere else in order to concentrate on the math. It doesn't seem something very original but I would want a formal description of this.

Mike Shulman (Jul 21 2023 at 00:42):

It's too bad that googling for "free prop" doesn't get you anything useful! (-:

Mike Shulman (Jul 21 2023 at 00:44):

This isn't exactly the same sort of description that you sketched, but in my paper A practical type theory for symmetric monoidal categories there is a description of the free (colored) prop on the data you describe (which at that time I called a "signature", but I have since learned is also called a [[pre-net]], and was called a "tensor scheme" by Joyal and Street) using terms in a type theory.

Mike Shulman (Jul 21 2023 at 00:44):

(By the way, in your definition of $\mathcal{A}^\otimes$, you won't have to $\cup \{\epsilon\}$ if you just allow $n=0$!)

Mike Shulman (Jul 21 2023 at 00:46):

I expect there is a description of this construction in different language somewhere in the Petri net literature. Maybe @Jade Master knows.

Jean-Baptiste Vienney (Jul 21 2023 at 01:03):

Thanks! "free prop" returns lot of things that are absolutely not mathematical :) . So let's see is she knows and I'll look at this and your paper.

Ralph Sarkis (Jul 21 2023 at 07:21):

This paper has describes this for non-colored PROPs but also briefly talks about colored PROPs. This other paper also has a similar construction, but the laws of symmetric monoidal categories are drawn with string diagrams in Figure 5, so that could help (non-colored case again).

John Baez (Jul 21 2023 at 08:11):

@Brandon Coya and Franciscus Rebro and I wrote a paper that develops a lot of tools to work with props using generators and relations:

• Props in network theory.

For example, you'd like to know that adding extra generators to a presentation of a prop gives rise to a monomorphism between props, while adding extra relations gives rise to an epimorphism. For this you want a category of props and an adjunction between props and 'signatures', which are collections of generators. This is the sort of thing we prove in the appendix to this paper!

Alas, we only do the case of uncolored props, because that's all we need - but most of the results and proofs extend to the colored case. (We point out one that does not.)

Jade Master (Jul 21 2023 at 08:23):

Thanks for the ping @Mike Shulman, @Jean-Baptiste Vienney Yes it is described as the operational semantics of pre-nets (which have exactly the generating data you have described). You can find a description of them as the functor Z in this paper or this paper the relevant inference rules and axioms are described in both. In either case, you end up with a left adjoint from pre-nets to free strict symmetric monoidal categories (strict symmetric monoidal categories whose objects form a free monoid). Maybe someone can correct me, but I believe these are the same as colored props. I could probably tell you lots more about this adjoint or many related constructions, just let me know if you have questions :)

Jade Master (Jul 21 2023 at 08:29):

To advertise my own work, I've written this paper which aims to generalize this free construction to many different varieties of nets. In particular, in Section 6 I show how the free construction introduced in the previous two papers I linked can be understood as the natural free functor from pre-nets to strict monoidal categories composed with the functor that "freely symmetrizes" a strict monoidal category into a strict symmetric monoidal category.

Jade Master (Jul 21 2023 at 08:35):

I could argue that my construction (the composite $F_Mon \circ N$) is slightly better than the constructions in the earlier papers because it is a left adjoint into all strict symmetric monoidal categories, not just the ones that have a free monoid of objects. However, this is a matter of personal aesthetics and I'm not sure if it is relevant to your problem.

John Baez (Jul 21 2023 at 09:18):

Wow, I actually forgot that Jade and Mike and I wrote, along with @Fabrizio Genovese, a paper that nicely analyzes how to build the free colored prop on some set of object generators and morphism generators! Here it is:

• Categories of nets.

John Baez (Jul 21 2023 at 09:23):

So, @Jean-Baptiste Vienney, if you want to see a free colored prop on a collection of object and morphism generators, check out our adjunction between $\mathsf{SSMC}$ (the category of strict symmetric monoidal categories and strict symmetric monoidal functors) and $\Sigma\mathsf{Net}$ (a category where an object is a collection of object and morphism generators).

John Baez (Jul 21 2023 at 09:26):

As we explain, the usual concept of Petri net is not good for describing free strict symmetric monoidal categories! It's good for describing free commutative monoidal categories, where the symmetry is the identity.

Jade Master (Jul 21 2023 at 14:04):

John Baez said:

So, Jean-Baptiste Vienney, if you want to see a free colored prop on a collection of object and morphism generators, check out our adjunction between $\mathsf{SSMC}$ (the category of strict symmetric monoidal categories and strict symmetric monoidal functors) and $\Sigma\mathsf{Net}$ (a category where an object is a collection of object and morphism generators).

My only nitpick is that this adjunction is from $\Sigma \mathsf{Net}$ and it sounds more like the original question is interested in pre-nets. Of course you may actually want $\Sigma$-nets, as they turn out to be the best sort of gadget for freely generating props. The situation is summarized by this diagram:
image.png
$\mathsf{SSMC}$ is the category of props, but you can get to them starting from either pre-nets, $\Sigma$-nets, or Petri nets by taking the other paths in this diagram.

Jade Master (Jul 21 2023 at 14:14):

Okay actually reading what we wrote (always a good idea :laughing: ) I'm seeing that a colored PROP isn't the same as an SSMC.
image.png
The former has to have objects which are freely generated by a set of colors.

Mike Shulman (Jul 21 2023 at 16:33):

That paper of ours was the first thing I thought of, actually, but I assumed Jean-Baptiste was looking for a more explicit description of the free prop on a net than we had. I guess you can extract something fairly concrete from our construction, but it would be a bit of work.

Mike Shulman (Jul 21 2023 at 16:35):

Jade Master said:

Okay actually reading what we wrote (always a good idea :laughing: ) I'm seeing that a colored PROP isn't the same as an SSMC.
The former has to have objects which are freely generated by a set of colors.

Right; although we did construct the adjunction between $\Sigma$-nets and SSMCs by factoring it through PROPs.

Jean-Baptiste Vienney (Jul 21 2023 at 19:11):

Yes, I want something fairly explicit, because what I want to do is very "geometric".

(I explain it a bit below, but I don't think it's very understandable as it.)

$\bigg($ I consider $\{n \ge 1\}$ as my colors and the generating morphisms are "creation operators" $\{c_n:n \otimes 1 \rightarrow (n+1), ~n \ge 1\}$ and "annihilation operators" $\{a_n:(n+1) \rightarrow n \otimes 1,~n \ge 1\}$.

After that I'm interested by a rewriting process on the free PROP hence generated. This rewriting process is such that the normal forms of $c_{1} \otimes id_{1^{\otimes (n-2)}}; c_2 \otimes id_{1^{\otimes(n-3)}};...;c_n;a_n;...;a_2 \otimes id_{1^{\otimes(n-3)}};a_1 \otimes id_{1^{\otimes (n-2)}}:1 \otimes ... \otimes 1 (n~times) \rightarrow 1 \otimes ... \otimes 1 (n~times)$ are exactly the permutations $\sigma:1 \otimes ... \otimes 1 (n~times) \rightarrow 1 \otimes ... \otimes 1 (n~times)$ and there is exactly one "terminating rewriting path" for every permutation. In a way I generate the whole symmetric group from a sequence of local choices which refine this string diagram more and more until finishing with the desired permutation. This rewriting process is generated by two possibilities for rewriting $c_n;a_n$. All of that is dedicated to prove a "characterization of the families of symmetric tensor powers through creation/annihilation operators in a symmetric monoidal $\mathbb{Q}^+$-linear category".

I once posted a picture that took me hours to draw which illustrate this weird rewriting process:
bi4graphs.jpg

$\bigg)$

I want something explicit and very easy to use in order to work on this specific question. But I think nothing is enough explicit so I'm going to write my own very explicit and hands-on description of free PROPs. I don't want a chain of two left adjoints functors to generate this PROP, that's all the contrary :sweat_smile:. I want something visual, but at the same time I want to be very formal to make things clear.

Anyway, thank you for the references, in particular the key-word "pre-net". I want to generate a PROP from a pre-net
and the section "Pre-nets" of the paper "Functorial Models for Petri Nets" contains an explicit description of this, but using some kind of sequent calculus, whereas I think it's better to talk explicitly of "grids" as I was sketching for my own problem.

If ever, you also have some reference on rewriting of free PROPs that would be even better.

Tobias Fritz (Jul 21 2023 at 20:51):

I'm a bit late to the party here and haven't clicked all the links, but here are some further references that may not have been mentioned yet:

• An Introduction to String Diagrams for Computer Scientists has a nice informal exposition of how morphisms in free PROPs are described by certain cospans of hypergraphs in Section 3. However, as far as I can see their description is missing the crucial acyclicity condition on the hypergraph (briefly mentioned later at the beginning of 4.2.1).

Here are also the earliest papers that I know of on free uncolored PROPs, which give graph-based descriptions that should be relatively straightforward to generalize to the colored case:

• On the invertibility of quantization functors by Enriquez and Etingof considers free PROPs, in a linear setting of modules over a ring, in Lemma 2.1. Their description in terms of graphs should be easy to adapt to PROPs over Set.
• A similar construction seems to appear in Vallette's thesis Dualité de Koszul des PROPs in Section 4.1 (in French).
• A cleaner exposition of this kind of construction is in Fresse's Props in model categories and homotopy invariance of structures, Section A.2.

Tobias Fritz (Jul 22 2023 at 08:54):

There's also Aleks Kissinger's new interactive theorem prover Chyp, in which string diagrams (being the morphisms in a free PROP) are implemented as cospans of acyclic monogamous hypergraphs. This is based on the paper is String Diagram Rewrite Theory II: Rewriting with Symmetric Monoidal Structure, where the cospans of hypergraphs description of free colored PROPs is developed.

John Baez (Jul 22 2023 at 14:37):

Jean-Baptiste Vienney said:

But I think nothing is enough explicit so I'm going to write my own very explicit and hands-on description of free PROPs. I don't want a chain of two left adjoints functors to generate this PROP, that's all the contrary :sweat_smile:.

By the way, we go directly from $\Sigma$ -nets to props; the chain of two left adjoints Mike mentioned was to go from $\Sigma$- nets to strict symmetric monoidal categories. The second step, going from props to strict symmetric monoidal categories, is quite evident.

John Baez (Jul 22 2023 at 14:45):

Our way of turning a $\Sigma$ -net (basically a presentation of a free prop) is rather tricky, so if you want something direct and elementary you won't like what we did!

John Baez (Jul 22 2023 at 15:08):

But one reason our construction is tricky is the concept of $\Sigma$ -net is subtle: I said it's a presentation of a "free prop" but we don't require the the symmetric groups act freely on the morphism generators! If you are willing to let permutations act freely on all the morphism generators then you can use a simpler and older concept: pre-nets.

Jean-Baptiste Vienney (Jul 22 2023 at 18:53):

For the moment, I think that pre-nets are sufficient for me even if I'm working on very permutation related matters. And thanks @Tobias Fritz for you last two references. The paper "String Diagram Rewrite Theory II: Rewriting with Symmetric Monoidal Structure" adresses exactly the kind of questions I'm interested by on how to formalize free PROPs and rewriting in free PROPs -- that I'm confronted to in my algebra problem which main character is one particular free PROP. In particular, I still don't know if I prefer using terms or graphs.

(Therefore, I'm not very much interested by morphisms of PROPs now. But in fact I should because I realize that I've probably been working with several free PROPs and morphisms between them previously but I didn't feel the need of so much formalization before I attack the trickiest part that I'm confronted to. I felt that too much formalism would be a constraint, but for my new question on the contrary, I feel the need of much formalization to clarify the problem).

Jean-Baptiste Vienney (Jul 22 2023 at 19:07):

(I'm using a very weird proof technique which needs clear formalization of the framework. In order to prove that something is equal to $\underset{\sigma \in \mathfrak{S}_{n}}{\sum}\sigma:A^{\otimes n} \rightarrow A^{\otimes n}$ in a symmetric monoidal category enriched over commutative monoids, I explain how to generate permutations as normal forms of a rewriting process starting from some big string diagram ie. a morphism of a free coloured PROP. I've never seen this technique anywhere but that's the only way I see to prove clearly what I want to prove)

John Baez (Jul 22 2023 at 20:10):

Jean-Baptiste Vienney said:

(Therefore, I'm not very much interested by morphisms of PROPs now. But in fact I should because I realize that I've probably been working with several free PROPs and morphisms between them previously but I didn't feel the need of so much formalization before I attack the trickiest part that I'm confronted to. I felt that too much formalism would be a constraint, but for my new question on the contrary, I feel the need of much formalization to clarify the problem).

I'm sure you know this, but the very concept of "free" involves morphisms.

Jean-Baptiste Vienney (Jul 22 2023 at 20:33):

That’s true… And I want to prove some fact about a free PROP but in fact I want to prove it for all the models of this PROP so maybe I will have to use the definition of freeness, and morphisms of PROPs indeed. s

Jean-Baptiste Vienney (Jul 22 2023 at 20:37):

But for now I was just interpreting free as “combining the generators without imposing equations” in order to speak about my little string diagrams…

Jean-Baptiste Vienney (Jul 22 2023 at 20:41):

Wait two minutes, I'm going to state very clearly what I want to prove and you will see that it's tricky to explain it without being very formal.

Jean-Baptiste Vienney (Jul 22 2023 at 20:56):

Ok, so here is this problem which makes me want to use free colored PROPs:

Jean-Baptiste Vienney (Jul 22 2023 at 20:56):

Let $(\mathcal{C},\otimes,I)$ be a symmetric monoidal category enriched over commutative monoids, that I will suppose strict monoidal to simplify.

Jean-Baptiste Vienney (Jul 22 2023 at 20:57):

Let $(A_{0})_{n \ge 0}$ be a family of objects of $\mathcal{C}$ such that $A_{0}=I$.

Jean-Baptiste Vienney (Jul 22 2023 at 20:59):

Let $(c_{n}:A_{n} \otimes A_{1} \rightarrow A_{n+1})_{n \ge 0}$ and $(a_{n}:A_{n+1}\rightarrow A_{n} \otimes A_{1})_{n \ge 0}$ be two families of morphisms such that $a_{0}=c_{0}=1_{A_1}$.

Jean-Baptiste Vienney (Jul 22 2023 at 21:01):

I will represent the $c_{n}$ and $a_{n}$ using string diagrams in the same way that the multiplications and comultiplications of bialgebras are ususually represented.

Jean-Baptiste Vienney (Jul 22 2023 at 21:01):

Suppose that for every $k \ge 0$ the following equation is verified:

Jean-Baptiste Vienney (Jul 22 2023 at 21:02):

Screenshot-2023-07-22-at-5.01.48-PM.png

Jean-Baptiste Vienney (Jul 22 2023 at 21:03):

Note that for the special case $k=0$, given that $a_0=c_0=1_{A_1}$, it's easier to write it like this:

Jean-Baptiste Vienney (Jul 22 2023 at 21:03):

Screenshot-2023-07-22-at-5.03.40-PM.png

Jean-Baptiste Vienney (Jul 22 2023 at 21:06):

Being in a symmetric monoidal category, using exchanges, you can define a natural transformation $\sigma:A_{1}^{\otimes n} \rightarrow A_{1}^{\otimes n}$ for every permutation $\sigma \in \mathfrak{S}_{n}$, obtained by permuting the $A_1$ in the obvious way (actually, you can interpret how act the permutations it in two different ways, but it doesn't change anything to this question).

Jean-Baptiste Vienney (Jul 22 2023 at 21:07):

Problem: Given this data, prove that for every $n \ge 2$, this equation is verified:

Jean-Baptiste Vienney (Jul 22 2023 at 21:09):

Screenshot-2023-07-22-at-5.08.09-PM.png

Jean-Baptiste Vienney (Jul 22 2023 at 21:09):

Jean-Baptiste Vienney (Jul 22 2023 at 21:10):

Here we are, if anybody can prove this quickly without using rewriting in a free PROP, I will gladly listen to you.

Jean-Baptiste Vienney (Jul 22 2023 at 21:16):

If you want to understand why it's true, verify that this equation is verified for $n=3$, or for $n=4$ if you have 30 minutes and want to write the string diagrams for the $24$ permutations of order $4$.

Jean-Baptiste Vienney (Jul 22 2023 at 21:23):

This theorem is more or less a constructive version of the fact "symmetric groups are generated by adjacent transpositions": it provides an algorithm which decomposes any permutation in a composite of adjacent transpositions.

Jean-Baptiste Vienney (Jul 22 2023 at 21:35):

That's funny that I arrived to this while thinking very hard to differential linear logic.

Notification Bot (Jul 23 2023 at 00:00):

Jean-Baptiste Vienney has marked this topic as resolved.

Tom Hirschowitz (Oct 11 2023 at 12:51):

Sorry I missed this for so long, @Jean-Baptiste Vienney!

@Richard Garner and I have a paper in which we give a graphical/combinatorial description of the free (colored) prop on a "hypergraph". In fact the paper is precisely about delineating a class of monads which admit such a graphical description. We fail to isolate a satisfactory general class, but propose a method which works on a few examples including props, properads, (symmetric) multicats, iirc.

It might be tedious to unpack all the abstraction to get the idea: maybe you'll find this talk easier.

Jean-Baptiste Vienney (Oct 11 2023 at 14:49):

Ok, thanks @Tom Hirschowitz . It could be useful to me!