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.
Nathaniel Virgo (Apr 01 2020 at 12:44):This might be a basic question, but I figure the broader topic probably belongs in the ACT stream, so I'm posting here.
Suppose I have a monoidal category. In my case it's a Markov category (in the sense of {1}) but I'm not sure if that matters - it would be nice to be general. I'll use Set as my example (with Cartesian product as the monoidal product.)
I can draw morphisms like this
Nathaniel Virgo (Apr 01 2020 at 12:47):and in Set they're just functions that take inputs and return outputs. I can also chain them together like this
Nathaniel Virgo (Apr 01 2020 at 12:48):What I want to do is to treat A and B (just the red ones) as a single item like this
Nathaniel Virgo (Apr 01 2020 at 12:48):that can then be plugged into any other morphism with the right inputs and outputs, like so:
Nathaniel Virgo (Apr 01 2020 at 12:49):I met similar things in Jules Hedges' lectures on open game theory {2}, and that's where I'm copying the drawing style from. But those lived in a more complicated category, and I'm hitting a few bumps in the road from "this kind of diagram is really intuitively reasonable and I want to use them" to "I understand exactly what these diagrams represent and how to manipulate them formally."
In my diagram above, the "AB" object is a very intuitively reasonable thing - it's a machine that takes an input in X, then gives an output in Y, then you have to give it another input in W before it gives a final output of type V. But formally I'm not sure how to think about it. I'm not even sure if it lives in Set (it's not a morphism there) or if I have to construct some other category for it to live in.
So the question is just what should I be reading/learning/doing to think about these "input-output machines" properly? What are they in formal category-theoretic terms, and how do they relate to the underlying category? (Set in this case.)
Nathaniel Virgo (Apr 01 2020 at 12:49):Of course we might to connect morphisms in various topologies, for example to get things like this (where the output B depends on X and A but not C, and similarly for D).
Nathaniel Virgo (Apr 01 2020 at 12:49):And we might also want to consider composing these machines together, for example to model a communication process:
Nathaniel Virgo (Apr 01 2020 at 12:49):Sorry if the question's a trivial one.
{1} Fritz 2019, A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics, https://arxiv.org/abs/1908.07021
{2} part 1 https://www.youtube.com/watch?v=5Qny8YmLUzk (there are another 3 lectures as well, but I couldn't find a playlist)
Antonin Delpeuch (Apr 01 2020 at 12:58):Very interesting! Let's ping @Jules Hedges :) For your last image, it intuitively sounds like axiomitizing this sort of composition must be quite hard!
Nathanael Arkor (Apr 01 2020 at 13:01):@Nathaniel Virgo: I think what you're describing is similar to a properad
Nathanael Arkor (Apr 01 2020 at 13:01):(although I only learnt what that was a few days ago, so take this with a pinch of salt)
Nathanael Arkor (Apr 01 2020 at 13:02):a properad is like a category, except that each morphism has multiple inputs and outputs
Nathanael Arkor (Apr 01 2020 at 13:02):and if you think of it like a graph, with morphisms being vertices and objects being edges, then you can contract (i.e. compose) any connected subgraph
Nathanael Arkor (Apr 01 2020 at 13:04):although there are just "inputs" and "outputs" for an operation in a properad — so your last diagram is a little stranger
Nathanael Arkor (Apr 01 2020 at 13:04):but maybe this would simply be representable as a sequence of multimorphisms?
Nathanael Arkor (Apr 01 2020 at 13:06):it's hard to tell without a specific example
Jules Hedges (Apr 01 2020 at 13:45):So, there's a few aspects to this. For the specific case where you're building these combs starting from a monoidal category, this is exactly the category of optics in the 2-legged case. For the many-legged case, for a while I was doing things by hand using common sense. Now, it turns out that these are exactly "states in the bicategory of Tambara modules". Guillaume Boisseau wrote a very nice paper about string diagrams in that bicategory, which we conjecture is more or less equivalent to comb diagrams over a monoidal category: https://arxiv.org/abs/2002.11480
Jules Hedges (Apr 01 2020 at 13:45):This is all work in progress, mind
Jules Hedges (Apr 01 2020 at 13:48):For comb diagrams themselves, I finally have what I think is a workable definition for the comb-inatorics of how they compose, forming an operad whose operations are all the ways of interleaving a bunch of combs. That's more general than the previous thing: given a monoidal category you should get an algebra of the combs operad, but there are other reasonable examples that don't arise that way (for example, Aleks Kissinger and other people in quantum mechanics use comb diagrams over a compact closed category)
Jules Hedges (Apr 01 2020 at 13:49):The wiggly example isn't something I ever thought about, so I have no idea about that. I doubt it's covered by any of what I said. Do you have any motivation for using a diagram element with that shape?
Jules Hedges (Apr 01 2020 at 13:56):In the meantime, I recommend just to proceed on common sense. It's safe to use these diagrams, nothing will go wrong
Mario Román (Apr 01 2020 at 14:45):Hi! An early version of this idea seems to come from the beautiful graphical language Mitchell Riley uses in "Categories of optics" (https://arxiv.org/abs/1809.00738). I also happen to have a preliminary note that may be relevant here (https://arxiv.org/abs/2003.06214). I think a fair answer is that you can model these "combs" as tuples of functions quotiented by an equivalence relation, at least in many useful cases. The nice thing is that the equivalence relation coincides with a coend and you can then apply Yoneda lemma to obtain nice concrete descriptions for these "combs". For instance, monoidal lenses coincide with combs (Riley's paper, without that name), and you can show that the combs Kissinger and Uijlen use as notation to model the work of Chiribella, D'Ariano and Perinotti, in the very restricted case of compact closed categories, also coincide with this idea (https://arxiv.org/abs/0712.1325).
The approach with coends seems to extend nicely to other topologies. We can try the example you were proposing :) The idea is to treat every "invisible wire" as quotiented out by a coend. For instance, your second topology example could be an element of the following coend, with the two invisible wires being U and V:
∃ U V . hom(X , U ⊗ V) × hom(A ⊗ U, B) × hom(C ⊗ V, D)
So, for instance, in the cartesian case, we can prove using Yoneda that it reduces to a pair of morphisms:
∃ U V . hom(X, U × V) × hom(A × U, B) × hom(C × V, D)
≅ (By the universal property of the product)
∃ U V . hom(X, U) × hom(X, V) × hom(A × U, B) × hom(C × V, D)
≅ (By Yoneda lemma!)
hom(A × X , B) × hom(C × X, D)
In non-cartesian cases, you may use some properties of your category to get a similar description.
So I think a nice way to go seems to be coends (at least, it should not be neglected). A very nice introduction to coend calculus has been written by Fosco Loregian; I really recommend the reading if you want to pursue this direction https://arxiv.org/pdf/1501.02503.pdf. And I would be actually interested in any applications of these things! :)
(edited: I made public some days ago a note on this approach that, among others, treats diagrams like these: http://compose.ioc.ee/git/mroman/coend-calculus-and-open-diagrams/raw/branch/master/opendiagrams.pdf But please mind that this is work in progress :) )
Reid Barton (Apr 01 2020 at 15:13):Interesting. These are large coends (indexed over all of Set) so a priori they might not exist, right? What happens in the example shown in the third and fourth images?
Jules Hedges (Apr 01 2020 at 15:22):Yes... in Mitchell Riley's paper Categories of Optics I think there's a section with proofs that the relevant coends do exist in ZF. I don't know whether it continues to work for these more complicated examples
Jules Hedges (Apr 01 2020 at 15:23):(Personally if they didn't exist in ZF I'd just chuck in enough assumptions until they did)
Reid Barton (Apr 01 2020 at 15:25):Proofs? I just skimmed the paper to look at the pictures :slight_smile:
Reid Barton (Apr 01 2020 at 15:26):Ah, so the example labeled above is exactly an optic
Reid Barton (Apr 01 2020 at 15:27):By "exist" I meant existing in the original universe--I'm perfectly fine with considering them to exist in some possibly higher universe.
Reid Barton (Apr 01 2020 at 15:30):Okay yes, it's Proposition 2.0.4. :thumbs_up:
Matteo Capucci (he/him) (Apr 01 2020 at 16:01):Jules Hedges said:
(Personally if they didn't exist in ZF I'd just chuck in enough assumptions until they did)
Always carry an inaccesible cardinal in your pocket
Gershom (Apr 01 2020 at 16:28):Mario's answer is very nice. Just using type-theoretic notation (and assuming a full CCC for now, tho the question is how much less we "really" need), the AB diagram sort of "obviously" reads as: X -> (Y x (W -> V)) = (X -> Y) x (X -> (W -> V)). The "recipe" is just to build a chain of functions each spitting out inputs or new functions demanding output as you go, from left to right, and each time there's a branch representing that by an appropriate product or tensor. The only "CCC" bit is the manipulation to equate the left and the right of the above formula. So any category that can handle linear logic should be enough to do this in as long as you stick to the representation on the left?
Jules Hedges (Apr 01 2020 at 16:38):Yes... you don't need a closure though, all you need is to be locally small, so the hom is a set, then you take the coend in the category of sets. In fact the original question was for a Markov category, which typically are not monoidal closed (that's also my most common use case, but in programming you'd nearly always have a closure)
Jules Hedges (Apr 01 2020 at 16:41):@John Baez you got your wires crossed there
David Egolf (Apr 01 2020 at 17:33):This reminds me a lot of the question I asked in the "Structured cospans" topic under "basic questions". I'm still working on fully understanding John Baez's answer, but he was indicating that the structured cospan approach can enable us to talk about sticking different objects together that have more than two connections.
Joe Moeller (Apr 01 2020 at 17:34):Are you watching his talk, which is going on right now?
David Egolf (Apr 01 2020 at 17:34):Oh, I didn't realize it was now! I'm planning to watch the recording.
T Murrills (Apr 01 2020 at 17:35):is this the OWLS talk, or a different one?
Joe Moeller (Apr 01 2020 at 17:37):This in the ACT@UCR seminar
Zulip Stream: #ACT@UCR seminar
Joe Moeller (Apr 01 2020 at 17:38):Zoom link: https://ucr.zoom.us/j/607160601
Joe Moeller (Apr 01 2020 at 17:39):Seminar Website: https://sites.google.com/ucr.edu/actucr/home