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.
Ruby Khondaker (she/her) (Aug 17 2025 at 11:45):I've been learning a bunch about profunctors recently (e.g. my recent question about #learning: questions > ✔ Comma Categories vs Categories of Elements ), and I wanted to ask a "soft" question about why they end up being so useful.
It seems that most forms of formal category theory need a way to include profunctors within them, whether that be with a yoneda structure, or with something like a virtual equipment. I've also heard that in the enriched setting, they're vital for talking about weighted limits and pointwise kan extensions!
These feel like pretty sophisticated/"high-level" reasons to care about profunctors. A low-level reason might be that they naturally correspond to "categorified relations". Yet (perhaps naively) it feels like profunctors play a much larger role in category theory than relations do in ordinary math - the biggest use-case for ordinary relations are equivalence relations, which can also be modelled with e.g. coequalizers. But "relations between groups" or "linear relations" or "relations between modules" seem to be far less common? (Of course, this could just be my lack of math experience!).
So to me, it feels like there's some kind of "unreasonable effectiveness" of profunctors within category theory, beyond them just being categorified relations. For people who work with them often, what would you say is a soft, "intuitive" reason for why this is the case?
Cole Comfort (Aug 17 2025 at 12:50):Much of linear algebra can framed in the internal language of linear relations. For example, a linear subspace is not a morphism in FVect, nor an object; but rather a subobject. It is natural to think of linear subspaces as linear relations.
Linear algebra developed before regular categories were invented, so classical results in linear algebra were not originally framed in this language.
However, mathematical abstraction can be very useful. So if we already have the tools at our disposal, and we are developing new mathematics, why not use them?
Ruby Khondaker (she/her) (Aug 17 2025 at 13:01):I see, so in some sense this is more a historical accident rather than something intrinsic to category theory?
Cole Comfort (Aug 17 2025 at 13:20):That is just my personal opinion, but I don't think that linear relations are less useful for linear algebra than profunctors are for category theory. Even in category theory, profunctors are relatively niche, but it doesn't mean that they aren't useful.
Mike Shulman (Aug 17 2025 at 15:32):I think relations are very important in ordinary math. For one thing, one shouldn't restrict artificially to the case of binary relations (or profunctors), even though many contexts for formalizing them require such a structure: usually the (bi/double/virtual/etc.) category of relations or profunctors is compact closed, so you can talk about relations of other arities by tensoring in the domain and codomain. And unary relations are, of course, just subsets (subobjects) which are important. Even binary relations include inequalities, which are also very important.
Ryan Wisnesky (Aug 17 2025 at 18:08):presentations of pro functors have the same syntax as 'naturally' related families of conjunctive (select/from/where) queries in SQL, that's one reason categoricaldata.net uses them and certainly select/from/where queries have been quite useful in computer science so I'd expect the same of pro functors within math more generally.
Ruby Khondaker (she/her) (Aug 17 2025 at 18:14):Ooh, that’s a use case I hadn’t even come across before!
John Baez (Aug 17 2025 at 19:20):I think I've told Ruby this before, but I think mysterious effectiveness of profunctors in category-based math is deeply analogous to the equally mysterious effectiveness of linear operators (or matrices) in set-based math. Linear algebra has a lot of benefits - for example that's why group representations are so much nicer than actions of groups on sets. So it would be a shame not to bring some of those benefits to category theory!
John Baez (Aug 17 2025 at 19:29):Btw, control theory is nicely phrased in terms of linear relations, as Jason Erbele and I worked out in our paper Categories in control, and the same is true for electrical circuits, as Brendan Fong and I discovered in A compositional framework for passive linear networks. Cole has also done a lot of work on linear relations. The category of linear relations is so rich that Pawel Sobocinski has a blog about it... not a blog post, an entire blog.
Ruby Khondaker (she/her) (Aug 17 2025 at 19:39):Is that Graphical Linear Algebra? I came across that a while back and quite enjoyed it (though admittedly the early sections were a little slow-going); it definitely helped me significantly in understanding Hopf algebras!
John Baez (Aug 18 2025 at 08:57):Yes, that's it. Two teams independently characterized the category LinRel: one being Bonchi-Sobocinski-Zanasi and the other being Baez-Erbele. In LinRel, every object is a commutative Frobenius monoid and a bicommutative Hopf monoid in two ways, and these interact in a nice way! So Pawel got very excited about this and blogged about it.
Alonso Perez-Lona (Aug 18 2025 at 13:14):John Baez said:
I think mysterious effectiveness of profunctors in category-based math is deeply analogous to the equally mysterious effectiveness of linear operators (or matrices) in set-based math
This sounds like a statement comparing pre- and fully-quantum field theory, is there an article that elaborates on this phenomenon from a more general perspective (as oppose to through concrete examples)?
John Baez (Aug 18 2025 at 13:26):I don't really know what "pre- and fully quantum field theory", though I know about [[prequantization]] as the first step in [[geometric quantization]]. Anyway, I don't know anything written from the perspective you want, though Urs Schreiber may have written something, which may be visible on those nLab articles I just linked to. Prequantization is like 'linearization' of a classical phase space.
John Baez (Aug 18 2025 at 13:28):Okay, Urs talks about [[prequantum field theory]]. I suspect he invented that term.