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: "Orthogonal" composition of profunctors


view this post on Zulip Moana Jubert (Jan 23 2024 at 22:18):

Given two profunctors P:Aop×BSetP : \mathcal{A}^{\mathsf{op}} \times \mathcal{B} \to \mathrm{Set} and Q:Bop×CSetQ : \mathcal{B}^{\mathsf{op}} \times \mathcal{C} \to \mathrm{Set} there is a canonical way to compose them using coends (or weighted colimits)

QP(A,C)BBQ(B,C)×P(A,B)colimQ(,C)P(A,)QP(A, C) \coloneqq \int^{B \in \mathcal{B}} Q(B, C) \times P(A, B) \cong \operatorname{colim}^{Q(-, C)} P(A, -)

There are many ways to interpret this construction: as a matrix multiplication, a tensor product of bimodules, some kind of "generalized existential quantification", ...

There seems to be another way to compose profunctors using ends (or weighted limits) when they are "orthogonal", i.e. given P:Aop×BSetP : \mathcal{A}^{\mathsf{op}} \times \mathcal{B} \to \mathrm{Set} and Q:Cop×BSetQ : \mathcal{C}^{\mathsf{op}} \times \mathcal{B} \to \mathrm{Set} (notice B\mathcal{B} is on the right in both signatures) I can define

PQ(A,C)BBP(A,B)Q(C,B)limQ(C,)P(A,)P^Q(A, C) \coloneqq \int_{B \in \mathcal{B}} P(A, B)^{Q(C, B)} \cong \operatorname{lim}^{Q(C, -)} P(A, -)

Does this construction have a name? What are good interpretations (or references) for it?

Thank you very much!

view this post on Zulip Dylan Braithwaite (Jan 23 2024 at 22:39):

I think this is the right Kan lift of PP along QQ in the bicategory Prof\mathbf{Prof} (or extension depending on your convention for the direction of the profunctors)

view this post on Zulip Dylan Braithwaite (Jan 23 2024 at 22:42):

See the first example at [[Kan lift]]

view this post on Zulip Dylan Braithwaite (Jan 23 2024 at 22:49):

And as they note in that page it makes Prof\mathbf{Prof} into a [[closed bicategory]]

view this post on Zulip Cole Comfort (Jan 23 2024 at 23:34):

Dylan Braithwaite said:

And as they note in that page it makes Prof\mathbf{Prof} into a [[closed bicategory]]

Also, one might be interested to know that quantaloid-enriched profunctors are closed linear bicategories, so that you actually have two interacting tensor products on top of the closure: one given by the end and the other by the coend. This is a categorification underappreciated fact that sets and relations form a closed linear bicategory, with respect to the usual "existential" composition and the "universal" composition. This has yielded some cool string diagrams..

Finally, Simon Willerton has some beautiful slides which you may be interested in.

view this post on Zulip Ryan Wisnesky (Jan 24 2024 at 00:03):

When you formalize families of relational conjunctive queries (e.g. SQL views) using pro-functors, one of these two constructions (the colimit one, I think, but I haven't thought hard about which direction arrows are pointing) is called "view unfolding" / "conjunctive query inlining" in CS literature

view this post on Zulip Max New (Jan 24 2024 at 14:53):

It's mentioned in these notes by Joyal (Section 4): https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf

If you like Logic/Type Theory, Dan Licata and I had a paper last year where we give a type theoretic syntax for profunctors: https://link.springer.com/chapter/10.1007/978-3-031-30829-1_6. In that syntax the profunctor composition is a sort of tensor product and the operation you describe is the corresponding Hom.

view this post on Zulip Moana Jubert (Jan 24 2024 at 16:40):

Max New said:

It's mentioned in these notes by Joyal (Section 4): https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf

If you like Logic/Type Theory, Dan Licata and I had a paper last year where we give a type theoretic syntax for profunctors: https://link.springer.com/chapter/10.1007/978-3-031-30829-1_6. In that syntax the profunctor composition is a sort of tensor product and the operation you describe is the corresponding Hom.

Yes, thank you! This is what I was looking for

view this post on Zulip fosco (Jan 27 2024 at 08:56):

Max New said:

It's mentioned in these notes by Joyal (Section 4): https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf

Not by Joyal ;-) The notes are written by Thomas Streicher, following Bénabou's lectures. A precious resource! Most of what I know on profunctors comes from reading them.