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: Optics and coequalisers


view this post on Zulip Nathaniel Virgo (Jan 19 2021 at 04:29):

This is a technical question about optics and coends. I'm going to paste in two relevant quotations from Riley's Categories of Optics and then ask my question.

on p. 3:
image.png

on p. 4:
image.png

This is then used to derive the nice graphical representation of optics as "diagrams with holes", aka comb elements.

This seems to rely on C\mathscr{C} being small, in order for lemma 1.2.1 to apply, but typically we want to consider optics in categories like Set\mathsf{Set}, FinSet\mathsf{FinSet} or the Kleisli category of a probability monad, which are generally not small.

So I'm wondering how I should think about the string diagram calculus for optics in these non-small categories. Do we have to treat it as a sort of metaphorical thing (as in, it shows us how optics would behave if the category were small, but it's not, so we have to independently check all the results some other way), or is there some way that I can interpret diagrammatic proofs as correct even when C\mathscr{C} is not small?

view this post on Zulip John Baez (Jan 19 2021 at 05:59):

FinSet is "essentially small" : it's equivalent to a small category. So I would not worry about that case.

For the other examples, it's quite safe to assume your set, measure space, etc. has cardinality less than some inaccessible cardinal. If you do that - e.g., replace Set\mathsf{Set} by the category of sets Setκ\mathsf{Set}_\kappa whose cardinality is κ\le \kappa for some inaccessible κ\kappa - you'll get a category that's essentially small. You can then replace Setκ\mathsf{Set}_{\kappa} by an equivalent small category X\mathsf{X} and work with that. I bet everything will be fine and you'll never notice the difference.

view this post on Zulip John Baez (Jan 19 2021 at 06:00):

This is just my first impression.

view this post on Zulip fosco (Jan 19 2021 at 20:55):

For what is worth, and as the official "coend guy" of profunctor optics ( :grinning: ) I have the same feeling as @John Baez that the solution is to either take a small category equivalent to the one you work with (when possible) or bound the size of the category from above in some way.

view this post on Zulip Nathaniel Virgo (Jan 20 2021 at 01:22):

Thank you both. That makes a lot of sense, but also induces a sense of vertigo, because I never thought of myself as someone who would need to know anything about inaccessible cardinals. But it sounds like for most practical purposes I don't need to worry about it, at least for the time being.

view this post on Zulip John Baez (Jan 20 2021 at 02:06):

Right, the point is that your "sets" could just as well be "sets in some set of sets that's so big you don't notice it's not the whole universe".

view this post on Zulip John Baez (Jan 20 2021 at 02:13):

So, you really don't need to worry about it.

view this post on Zulip Jules Hedges (Jan 20 2021 at 11:13):

Something I didn't figure out until surprisingly recently is that if your base category is something like the kleisli category of a strong monad on a cartesian closed category (not 100% certain the exact conditions when it works), you can directly prove that the coend is isomorphic to a set:

view this post on Zulip Jules Hedges (Jan 20 2021 at 11:15):

Θ(SM(Θ×A))×(Θ×BM(T))Θ(SM(Θ×A))×(Θ(BM(T)))SM((BM(T))×A)\int^\Theta (S \to M (\Theta \times A)) \times (\Theta \times B \to M (T)) \cong \int^\Theta (S \to M (\Theta \times A)) \times (\Theta \to (B \to M (T))) \cong S \to M ((B \to M (T)) \times A)

view this post on Zulip Nathaniel Virgo (Jan 20 2021 at 12:06):

Oh, that's really neat, thanks!

view this post on Zulip Jules Hedges (Jan 20 2021 at 12:09):

Me not knowing this earlier (or rather somebody did tell me but I never internalised it and then forgot) led to a huge amount of unnecessary work by my previous PhD student Joe Bolt in what is now the Bayesian Open Games paper. He figured out all the coend optics stuff before it became well known, and we could have just avoided optics entirely

view this post on Zulip Nathaniel Virgo (Jan 20 2021 at 12:14):

I wonder if that also partially answers my other question here about Markov categories and optics, in the case where the Markov category is the Kleisli category of a monad with the right properties. That SM((BM(T))×A)S\to M((B\to M(T))\times A) sort of looks like a stochastic map with the desired conditional independence property.

view this post on Zulip Nathaniel Virgo (Jan 20 2021 at 12:21):

(These questions are partly inspired by reading the Bayesian Open Games paper, so this is good to know!)

view this post on Zulip Jules Hedges (Jan 20 2021 at 12:29):

Hmmm, could be...

view this post on Zulip Jules Hedges (Jan 20 2021 at 12:33):

There's an updated version of the paper that's under review but I think I didn't upload to arXiv yet. This fact is now in the paper, together with a post-hoc justification for overkilling it with coend calculus on the grounds that: 1) it's more general, 2) it matches the diagrams from Riley, which are still super useful, and 3) in the case of contexts (but not co/play maps!) the bound variable has a direct interpretation as the set of unobservable states of the game

view this post on Zulip Nathaniel Virgo (Jan 20 2021 at 12:40):

Here's what I mean about the conditional independence thing. An element of SM((BM(T))×A)S\to M((B\to M(T))\times A) is a thing that I give an SS to, and it gives me an AA together with something that I can give a BB and it will give me a TT. So the TT can depend on the SS and the BB, but the AA can only depend on the SS. It's not quite the same thing as a morphism S×BM(T×A)S\times B \to M(T\times A) with a conditional independence relation, but it seems like they ought to be isomorphic.