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: Properads that are not props


view this post on Zulip Amar Hadzihasanovic (Aug 24 2022 at 08:51):

One way of defining (coloured) props, (coloured) properads and symmetric polycategories is as structures with the same type of underlying data — morphisms with "multiple inputs" and "multiple outputs" — but different classes of "composable string diagrams":

So given a prop, you can always get a properad and a polycategory by restricting the composition operations, and conversely you can ask whether it is possible to consistently extend the compositions of a polycategory to that of a properad or prop, or the compositions of a properad to those of a prop.

While there is plenty of natural examples of polycategories that do not extend to properads/props (for example those arising from "nondegenerate" models of linear logic), I realised I do not know any particularly natural examples of properads that are not restrictions of props.
(By "natural" I mean ones that are not free, or do not somehow have "connected graphs" built in the definition).

Can someone teach me some examples?

view this post on Zulip Mike Shulman (Aug 24 2022 at 17:25):

there are plenty of natural examples of polycategories that do not extend to properads/props (for example those arising from "nondegenerate" models of linear logic)

I certainly believe there are polycategories that can't be embedded fully and faithfully in props; I think you can argue for this using traces among other ways. But are there polycategories that can't be embedded faithfully in any prop? I have wondered this for a while but haven't found an answer.

view this post on Zulip Amar Hadzihasanovic (Aug 24 2022 at 19:12):

I don't know the answer to that question but I'd also like to know!

I realise the phrasing “do not extend to” was ambiguous; I only meant “they are not in the essential image of the forgetful functor from (props) to (polycategories)”.

So my first constraint is to exclude

while one attempt to phrase the “natural example” constraint in a slightly more specific way is to exclude

This, for example, rules out the “properad of connected d-cobordisms” that somebody suggested to me elsewhere, since the free prop it generates is equivalent to the prop of all d-cobordisms, arguably more/equally “natural”.

view this post on Zulip Mike Shulman (Aug 24 2022 at 19:54):

I think "in the essential image of the forgetful functor from (props) to (polycategories)” is the same as saying "embeds fully-faithfully in a prop"?

view this post on Zulip Amar Hadzihasanovic (Aug 25 2022 at 08:49):

Oh, of course, that makes sense.

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 18:21):

To derive equalities between pasting diagrams in polycategories, you swap out contractible sub-pasting-diagrams for their equals. To derive equalities between pasting diagrams in properads, you swap out connected sub-pasting-diagrams for their equals.

But connected sub-pasting-diagrams of contractible pasting diagrams are contractible. So there shouldn't be any new equalities you can derive between contractible pasting diagrams after you pass from a polycategory to the free properad on it.

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 18:41):

Meanwhile, to derive equalities between pasting diagrams in props, you can swap out sub-pasting-diagrams that are not even necessarily connected.

Any sub-pasting-diagrams newly obtained when viewing a polycategory pasting diagram as a prop pasting diagram are not themselves contractible. So if we start with a contractible pasting diagram, we'll only be able to perform swaps that we already could in the original polycategory.

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 18:43):

Does that make sense?

view this post on Zulip Amar Hadzihasanovic (Sep 27 2022 at 18:56):

If I understand what you are saying, it is an argument for the fact that every polycategory embeds faithfully in a properad and every properad embeds faithfully in a prop (specifically, the free properad and the free prop, respectively).

view this post on Zulip Amar Hadzihasanovic (Sep 27 2022 at 18:56):

Asking whether they embed fully faithfully is much stronger.

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 18:56):

Yes.

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 19:01):

For comparison, you can't always faithfully embed props in props-with-duals.

To derive equalities between pasting diagrams in a prop-with-duals, you're now allowed to swap out "sub-pasting-diagrams" with some of their outputs appearing upwards of some of their inputs.

Prop pasting diagrams, when viewed as living in a prop-with-duals, obtain new "sub-pasting-diagrams" not present before that are themselves prop pasting diagrams.

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 19:08):

pasting.png pasting2.png

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 19:09):

The second diagram is a subdiagram of the first diagram in a prop-with-duals, but not in a prop.

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 19:10):

pasting3.png

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 19:28):

I've edited my messages, changing "compact closed category" to "prop-with-duals", to be more clear.

view this post on Zulip Mike Shulman (Sep 27 2022 at 19:34):

Aaron David Fairbanks said:

Does that make sense?

That's also my intuition, but it's a ways from that to a proof.

view this post on Zulip Mike Shulman (Sep 27 2022 at 19:35):

Ideally, a conceptual/semantic proof, rather than a tedious and error-prone analysis of syntax...

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 19:38):

I wondered if that would be your response. Do you have any examples of similar conceptual proofs you might point me to? I'm fairly new to this kind of reasoning.

view this post on Zulip Mike Shulman (Sep 27 2022 at 19:40):

Well, there's a nice technique due to Lafont for proving full-and-faithful embeddings of this sort using a gluing construction. In *-Autonomous Envelopes and Conservativity I used it to prove results of that sort about structured polycategories. I don't have any idea how to adapt that technique to prove faithful-but-not-full embeddings, but at least it should give some idea of the sort of proof I like. (-:O

view this post on Zulip Aaron David Fairbanks (Sep 27 2022 at 19:41):

Thanks!