PROPs as theories of connection

In this post, I want to articulate a little idea I’ve had for a while about using PROPs to describe diagrammatic languages of interconnection in a quick way. Really, it’s nothing more than the observation that certain wiring diagram operads arise from finitely presented symmetric monoidal categories. I’m not very familiar with the PROP literature, so I wouldn’t be surprised if this is already known and articulated somewhere, or is at least folklore. If you’ve seen it before, I’d love to see!

Let me say right off the bat that when I use the terms “PROP” and “operad” here, I will always mean their colored (i.e. many object) variants.

The idea is simple. Every PROP P determines a symmetric monoidal category FP, and every symmetric monoidal category M gives rise to an operad OM. Putting this together, we get a functor

\mathsf{PROP} \to \mathsf{SMCat} \to \mathsf{Operad}

That, explicitly, sends a prop P to the operad OFP whose objects are lists of objects in P, and with morphisms OFP(\vec{p}_1, \ldots, \vec{p}_n; \vec{q}) = P(\vec{p}_1, \ldots, \vec{p}_n; \vec{q}) . This formula is a little abusive: on the left we have an op of arity n, where on the right we have a prop of arity \left( \sum_i \mathsf{len}(\vec{p}_i);\, \mathsf{len}(\vec{q})\right). In other words, we have flattened the list of lists into a single list, and mapped out of that.

The point I want to make here is that PROPs of very simple finite presentation give rise to operads of nesting wiring diagrams that can be more difficult to describe in other ways. For example:

  • If P is the PROP on a single object generated by a special commutative Frobenius algebra, then by this paper FP is the symmetric monoidal category of cospans on finite sets with disjoint union. Therefore, OFP is the operad of (cospan) bubble diagrams, composing by nesting.

  • If P is the PROP of a “dualizable object”: that is, two objects i and o, two maps w : () \to (i, o) and c : (i, o) \to () satisfying the zig-zag laws familiar from an adjunction. Then OFP is the operad of wiring diagrams for traced symmetric monoidal categories: an object is a formal sum ni + mo which represents a box with n input ports and m output ports, so an op will involve putting k boxes inside an outer box, and we are allowed to connect any inner input to any inner output (using c), any inner input to any outer input and same for outputs (using the identities on i and o), and we can wire an outer input straight to an outer output (using w). The zig-zag propagate connections through passing wires:

  • If P is the PROP on a “heteromorphism between a cocommutative comonoid and a commutative monoid”, then OFP is the operad \mathsf{Lens}(\mathsf{Arity}) of lens based wiring diagrams. I made up the term “heteromorphism” here so let me explain. We have two objects i and o where i is a commutative monoid and o is a commutative comonoid, and a “heteromorphism” c : (i, o) \to () which commutes with the (co)monoid structure in a way best described by string diagrams:

To see how this works, imagine “cutting open each box” in a wiring diagram and stretching it so that all the inner boxes are splayed out on the left and the outer box is splayed on the right:

This won’t work for all theories of interconnection, of course. It only works for those that don’t treat ports on the same box different from ports on distinct boxes, since of course the definition is not sensitive to the boundaries of boxes. This rules out the diagrams for SMCs for example, which allow connection between different boxes but not between the same box. It also rules out special shapes for boxes, like the diagrams for operads where the boxes are corollas and the diagrams form trees.

2 Likes

:clap: :clap: let’s reclaim the term operad

1 Like

My paper Props in network theory with Brandon Coya and Franciscus Rebro uses props in a different way, to describe “specific” symmetric monoidal categories rather than diagrammatic languages of interconnection. The interplay is probably worth thinking about!

We focus on single-sorted (i.e. uncolored) props. We formalize the (already widely used) diagrammatic way of presenting such props using generators and relations by describing a multi-sorted Lawvere theory whose algebras are props. This lets us apply all the usual technology relating Lawvere theories, monads and presentations of algebraic gadgets to props.

We mention that there’s also a multi-sorted Lawvere theory for multi-sorted props with a fixed set of sorts, so everything can be generalized to that case. In fact there’s also a multi-sorted prop for multi-sorted props with a fixed set of sorts! But this would not give us much leverage for proving results about multi-sorted props, at least not at first, due to the circularity!

2 Likes

Ah, great to see that PROPs are models of a Lawvere theory — it makes perfect sense, it’s great to see it worked out and used!

We mention that there’s also a multi-sorted Lawvere theory for multi-sorted props with a fixed set of props, so everything can be generalized to that case. In fact there’s also a multi-sorted prop for multi-sorted props with a fixed set of props!

What does a prop having a fixed set of props mean? Are you using “prop” in the second sense like “op” in operad, i.e. as a synonym for morphism?

It would be interesting to see these two ways of looking at things compared. My first thought is that a “concrete PROP” should give an algebra over some associated operad of wiring diagrams. Let me try to feel this out.

It seems pretty obvious that algebras of OFP should correspond to right modules of P; ideally this would be deduced by extending the functor \mathsf{Prop} \to \mathsf{Operad} to equipments. This suggests that a “concrete prop” with arities in P should the collage i : P \to C of a right module of P (there aren’t really “props of elements” of right modules, so this is the only choice for representing a right module as a prop in its own right).

But this isn’t right, and it comes down to the difference in biased or unbiased composition of systems. Props-as-systems use biased composition; a system is a morphism, and its interface is its signature, which has built in “input” and “output” sides. Systems as algebras for wiring diagram operads is unbiased — it only has “inputs” and “outputs” if the wiring diagram operad has them as part of its diagrams.

Still worth working out the relation here!

What does a prop having a fixed set of props mean?

Luckily one can edit things here. I meant to write:

We mention that there’s also a multi-sorted Lawvere theory for multi-sorted props with a fixed set of sorts, so everything can be generalized to that case. In fact there’s also a multi-sorted prop for multi-sorted props with a fixed set of sorts!

I agree that this is an interesting challenge:

Props-as-systems use biased composition; a system is a morphism, and its interface is its signature, which has built in “input” and “output” sides. Systems as algebras for wiring diagram operads is unbiased — it only has “inputs” and “outputs” if the wiring diagram operad has them as part of its diagrams.

Maybe this isn’t such a big deal for compact props - i.e. props that are compact closed when regarded as symmetric monoidal categories. Almost all the props considered in my paper “Props for network theory” are compact. But for those that aren’t, there seems to be a real difference here.

I doubt I’ll have the energy to sort out this issue, but it seems like a good thing to grapple with!

(By the way, I’m glad you seem to be going along with me on this point: we can drop the all-caps spelling of the acronym PROP and nothing terrible will happen; it’ll become just another ordinary math term.)

Very nice. I would like to +1 the paper that John mentioned as I think the ideas are relevant to what you are doing. I am also a little bit confused about the way you are using prop, as something which generates a symmetric monoidal category. I thought that a prop already was a symmetric monoidal category. The functor F you are describing should be the adjunction in Appendix B of “Props in Network Theory” which takes a signature and freely generates a prop from it…which is a symmetric monoidal category. So in that paper what you mean by “prop” is what they mean by “signature” if I am understanding correctly?

If a prop is a special sort of symmetric monoidal category, then F is just the inclusion. But I usually think of a prop as more like an operad — which is to say, a different kind of category and not a category-with-structure. In this case F actually does something. But yeah, the right way to do it is the way John does in that paper, treating it as a model of a special algebraic theory. In this way, a prop should be a signature (object of \mathsf{Set}^{\mathbb{N}\langle A\rangle^2} where \mathbb{N}\langle A \rangle is the free commutative monoid on a set A) together with an algebra structure for the prop-monad.

2 Likes

Even if we think of a prop as a special sort of symmetric monoidal category, I believe it’s wise to treat it as a symmetric monoidal category with extra structure, not just extra properties. The point is that you want to know, not just that all objects are prop are tensor products of some generator, but what this generator is. This may be obvious to everyone here, but let me spell it out.

Traditionally, a prop (C,x) is a strict symmetric monoidal category C with a specified object x such that every object is equal to some power x^{\otimes n}. This object is extra structure. Thus, a map of props f: (C,x) \to (D,y) is a symmetric monoidal functor f: C \to D that preserves this extra structure: f(x) = y.

This definition is ‘evil’ in a couple of ways, but Props in network theory includes some propositions that justify this evil.

In Prop. 4.3, we show this. Suppose C is a symmetric monoidal category with an object x for which every object is isomorphic to some power x^{\otimes n}. Then C is equivalent to a prop. More precisely, C is equivalent, as a symmetric monoidal category, to a symmetric monoidal category D with an object y for which every object is equal to some power y^{\otimes n}.

In Prop. 4.4, we show this. Suppose (C,x) and (D,y) are props, and suppose f: C \to D is a symmetric monoidal functor. Then f is isomorphic, as a symmetric monoidal functor, to a strict symmetric monoidal functor g: C \to D. If also f(x) \cong y then g is a morphism of props.

These results were ‘well-known’ or at least ‘obvious’ to a few experts, but we thought it would be good to include proofs.

All this stuff generalizes to the case of colored props: instead of a single generator we have a list (or indexed set) of generators. But we (alas) did not do this generalization.

2 Likes