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: Well-defined functions/transformations on PROPs

Jesse Sigal (Oct 29 2020 at 12:43):

Hi everyone, I'm trying to find resources/references/get advice on the following. I'm trying to design a PROP diagrammatically, and one of the features I want is a factorization in the sense of Theorem 4.6 from "Composing PROPs" [1] and Proposition 3.6 from "Lawvere Categories as Composed PROPS" [2].

So far, I've come up with enough equations to add to my PROP that I think I have a factorization algorithm based on the form my diagrams must take. The algorithm is both deterministic and terminating, and thus can be seen as an endofunction on diagrams of my PROP. I'm trying to make sure that the algorithm is well-defined. I believe well-defined for a factorization has the following meaning in this context:

Let $D_1$ and $D_2$ be equivalent diagrams in my PROP $\mathcal{T}$. Apply the algorithm to both to produces $L_1 ; R_1$ and $L_2 ; R_2$ from $D_1$ and $D_2$ respectively, where $L_i$'s belong to a sub-PROP $\mathcal{T}_L$ and $R_i$'s belong to a sub-PROP $\mathcal{T}_R$. Then the algorithm is well defined when $L_1$ is equivalent to $L_2$ in $\mathcal{T}_L$ and $R_1$ is equivalent to $R_2$ in $\mathcal{T}_R$ up to a mediating permutation from the cited papers.

My main question is how to prove this effectively and rigorously. I think it is sufficient to prove the following, where $N$ is the function induced by the algorithm:

1. Show $N$ respects the the symmetry and monoidal axioms of PROPs.
2. Show $N$ respects vertical and horizontal composition of PROP diagrams.
3. Show $N$ respects the generating equations of my PROP.

I feel like I've been thrown a bit through a loop trying to formally prove things just with diagrams, because I know completely formalizing them can be quite a challenge combinatorially. Any advice is appreciated! :smiley:

[1]S. Lack, ‘Composing PROPs.’, Theory and Applications of Categories [electronic only], vol. 13, pp. 147–163, 2004.
[2]F. Bonchi, P. Sobocinski, and F. Zanasi, ‘Lawvere Categories as Composed PROPs’, in Coalgebraic Methods in Computer Science, Cham, 2016, pp. 11–32, doi: 10.1007/978-3-319-40370-0_3.

Cole Comfort (Oct 29 2020 at 12:48):

What exactly is the question? Can you push all of the morphisms past each other in a way that respects the symmetric monoidal structure? Perhaps it would also be worth reading this paper of Rosebrugh and Wood:
https://www.mta.ca/~rrosebru/articles/fac.pdf

Jesse Sigal (Oct 29 2020 at 12:59):

Yeah sorry that was a bit too much information maybe. Basically: I have a function $N$ on diagrams of a PROP, what do I need to do to show it's well-defined?

(Link is dead :frown: )

Cole Comfort (Oct 29 2020 at 13:15):

Updated the link

Cole Comfort (Oct 29 2020 at 13:19):

So in the basic case when the sub prop is just the free prop, a relaxed distributive law on ${\mathbb X} \otimes_{\mathbb P} {\mathbb Y}$ is a function taking formal compositions ${\mathbb Y}; {\mathbb X}$ to formal compositions ${\mathbb X}; {\mathbb Y}$ in a way that respects the symmetric monoidal structure picked out by the actions of $\mathbb P$. When both categories are presented in terms of generators, then this is just a way to push past all of the generators of $\mathbb Y$ past those of $\mathbb X$ as string diagrams.

Cole Comfort (Oct 29 2020 at 13:22):

This is formally descibed in terms of a distributive law over a symmetric monoidal category (in this case the free prop) in the category of profunctors internal to $\sf Mon$.

Jesse Sigal (Oct 29 2020 at 13:40):

Thanks for the resource and the summary, definitely seems relevant :smile: