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: "change of domain" for coends

Jules Hedges (Jun 16 2021 at 10:16):

Exercise 1.13 in Co/end Calculus (https://arxiv.org/abs/1501.02503) states that if you have an adjunction $L \dashv R$ between $L : \mathcal C \to \mathcal D$ and $R : \mathcal D \to \mathcal C$, and another functor $G : \mathcal D^{op} \times \mathcal C \to \mathcal E$, then $\int^{C \in \mathcal C} G (LC, C) \cong \int^{D \in \mathcal D} G (D, RD)$. The actual exercise asks to prove a converse of this, but I'm interested in the forwards version, which is the only result I've seen that lets you change the "domain of integration" of a coend. I can't see how to prove it... can anyone help?

Jules Hedges (Jun 16 2021 at 10:18):

The thing I think I actually need is a dual of this where everything is the same except $G : \mathcal D \times \mathcal C^{op} \to \mathcal E$, which I think is probably equivalent to the same result but for ends. But I think I'd better understand the proof before naively dualising it

Amar Hadzihasanovic (Jun 16 2021 at 11:31):

I tried to do it, but I only got that there is a canonical morphism $\int^C G(LC, C) \to \int^D G(D, RD)$. You can get this by observing that composing

$$G(LC, \eta_C): G(LC, C) \to G(LC, RLC) \quad \quad \text{with} \quad \quad \imath_{LC}: G(LC, RLC) \to \int^D G(D,RD)$$

where $\imath_D$ are the components of the initial cowedge for $G(-,R-)$ gives you a cowedge from $G(L-,-)$ to $\int^D G(D,RD)$ (that's an exercise in definitions), so by universality you get a unique morphism $\int^C G(LC, C) \to \int^D G(D, RD)$.

Amar Hadzihasanovic (Jun 16 2021 at 11:33):

However you can't apply the same reasoning to get a morphism the other way, because the counit “points the wrong way”.

Oh silly me, I got mixed up with the variances, of course.

Amar Hadzihasanovic (Jun 16 2021 at 12:30):

Above in my first attempt with coends I got mixed up with the variance of the first argument of $G$ and thought there was a problem which wasn't there.

So in fact, you can use the symmetric argument, that you can compose

$$G(\varepsilon_D, RD): G(D,RD) \to G(LRD, RD) \quad \quad \text{with} \quad \quad j_{RD}: G(LRD, RD) \to \int^C G(LC, C)$$

to get a cowedge from $G(-,R-)$ to $\int^C G(LC,C)$, hence a universal morphism $\int^D G(D,RD) \to \int^C G(LC, C)$.

At this point I guess you can do some “standard” calculations to show that these two are each other's inverse.

Amar Hadzihasanovic (Jun 16 2021 at 12:37):

(Sorry, I have deleted a bunch of messages which are only me failing to dualise things properly, didn't want to confuse things further :rolling_eyes: )

Jules Hedges (Jun 16 2021 at 17:32):

Thanks!

Jules Hedges (Jun 16 2021 at 17:34):

For the dual, I may be lucky because my left adjoint is fully faithful, and in fact the unit of the adjunction is the identity on the nose

Jules Hedges (Jun 16 2021 at 17:34):

This is referring to something that you deleted

Jules Hedges (Jun 16 2021 at 17:41):

Even then, only the first half of this goes through with all the variances reversed

Amar Hadzihasanovic (Jun 16 2021 at 18:49):

Jules Hedges said:

Even then, only the first half of this goes through with all the variances reversed

No, I think your first guess was right: it should all go through in the same way for ends, if you have $G: \mathcal{D} \times \mathcal{C}^\mathrm{op} \to \mathcal{E}$ (and the same adjunction)...

Amar Hadzihasanovic (Jun 16 2021 at 18:50):

All the four families of morphisms that I used in the sketch are reversed by exchanging the variances of $G$ and passing from coends to ends.

Amar Hadzihasanovic (Jun 16 2021 at 18:52):

Jules Hedges said:

This is referring to something that you deleted

Yeah that was when I had misjudged the variances, you don't need any additional hypotheses :)

Guillaume Boisseau (Jun 18 2021 at 10:15):

@Jules Hedges That's just a few steps of coend calculus

Guillaume Boisseau (Jun 18 2021 at 10:18):

image-b441dcca-3a5f-414a-8c1a-59eeb3ef4d79.jpg

Guillaume Boisseau (Jun 18 2021 at 10:19):

The end case is similar, with Yoneda instead of coYoneda

Guillaume Boisseau (Jun 18 2021 at 10:31):

image-8db369cd-9702-4f7f-af1e-8e66bcf12440.jpg

Amar Hadzihasanovic (Jun 18 2021 at 10:57):

Wow this is just like quantum mechanics... when in doubt insert a resolution of the identity

Amar Hadzihasanovic (Jun 18 2021 at 10:57):

I should learn coend calculus!

Dan Marsden (Jun 18 2021 at 11:00):

Doesn't your use of the yoneda lemma in the first step place quite strong assumptions on the types of the functions involved. Or am I misinterpreting?

Guillaume Boisseau (Jun 18 2021 at 11:15):

which functions do you mean?

Jules Hedges (Jun 18 2021 at 11:15):

Guillaume Boisseau said:

image-b441dcca-3a5f-414a-8c1a-59eeb3ef4d79.jpg

Oh, pretty!

Guillaume Boisseau (Jun 18 2021 at 11:16):

knew you'd like it

Jules Hedges (Jun 18 2021 at 11:17):

(I'm still not finished with figuring out how Amar's answer fits into my slightly more awkward situation. I'll come back and explain once I've figured things out)

Dan Marsden (Jun 18 2021 at 13:42):

Sorry, I meant functors. In particular doesn't G(-,C) have to have codomain Set (or the base of enrichment) so you can use Yoneda in the first step? So there's a restriction on the type of the bifunctor G which doesn't seem to appear in the original statement.

Jules Hedges (Jun 18 2021 at 13:57):

Oh yeah... I'm pretty sure it's implicit in the original statement

Jules Hedges (Jun 18 2021 at 13:58):

It may be that Fosco uses $\mathcal E$ for that everywhere in the book

Dan Marsden (Jun 18 2021 at 14:07):

Ah, that convention is particularly confusing when the types go C,D,E. If that's the case, nice proof @Guillaume Boisseau. Good to see it can be done with coend calculus without having to resort to lower level arguments.

Guillaume Boisseau (Jun 18 2021 at 14:32):

Oh you're absolutely right, I just assumed they ranged over the base of enrichment out of habit

Guillaume Boisseau (Jun 18 2021 at 14:40):

image-d2b7619b-8e70-4091-9ab2-74475606ae52.jpg

Guillaume Boisseau (Jun 18 2021 at 14:40):

Here's a proof that works for an arbitrary E (assuming all categories are locally small or whatever). I just use one more Yoneda to get back to a case where the domain is indeed Set/the enrichment base. Since the iso is natural in X we can lift it to the required iso in E.

Jules Hedges (Jun 18 2021 at 15:53):

Nice!

Jules Hedges (Jun 18 2021 at 15:54):

I also got my own variances back to front, which means my problem is actually an instance on the nose of the original statement in the book, so I'm done

Guillaume Boisseau (Jun 18 2021 at 15:56):

Nice!

Jules Hedges (Jun 18 2021 at 15:58):

This is for corollary 3.32 of Bayesian Open Games (https://arxiv.org/abs/1910.03656) which the referee (rightly) complained didn't contain enough detail. (Previously I "proved" it by squinting at diagrams, which at least was enough for me to be certain it was true)

Proposition: If $\mathcal C$ is a monoidal category whose monoidal unit is terminal, then $\mathbf{Optic} (\mathbf{Optic} (\mathcal C)) (I, ((S, T), (A, B)) \cong \mathbf{Optic} (\mathcal C) ((I, B), (S, A))$

Jules Hedges (Jun 18 2021 at 16:00):

The meat of the proof is to notice that if the monoidal unit of $\mathcal C$ is terminal, then the map $\mathcal C \to \mathbf{Optic} (\mathcal C)$, $S \mapsto (S, I)$ has a right adjoint, which on objects is $(S, T) \mapsto S$. (When your monoidal product is moreover a cartesian product then this right adjoint is the "view fibration" which I've written quite a bit about)

Jules Hedges (Jun 18 2021 at 16:03):

The $\mathcal C$ s we actually care about are categories of stochastic functions, for which the monoidal unit is typically terminal (because there is exactly 1 probability distribution on a point), but the monoidal product is not cartesian (since a joint distribution cannot be determined by its marginals), so this heavier machinery is really needed

Jules Hedges (Jun 18 2021 at 16:04):

This lemma is super important to the paper, it would have been a giant headache if it was false, because the thing on the left of the isomorphism is more convenient for doing general theory, but the thing on the right is more convenient for doing calculations

Guillaume Boisseau (Jun 18 2021 at 17:02):

Hm I don't get the proof in the paper. If I were to guess what's happening in the middle step: it looks like you go from coend over objects of Lens and coend over pairs of objects of C, which is wrong because they don't have the same arrows; and then you drop a variable because it appears nowhere, which is also not allowed in general (though that's allowed when C is connected, which it is here).

Guillaume Boisseau (Jun 18 2021 at 17:03):

I don't see how you can use the change of domain above to prove this differently, could you elaborate?

Jules Hedges (Jun 18 2021 at 17:16):

I hope I didn't make another mistake!

Jules Hedges (Jun 18 2021 at 17:18):

Specifically, take $G : \mathbf{Optic} (\mathcal C)^{op} \times \mathcal C \to \mathbf{Set}$, $(\Psi, \Psi'), \Theta \mapsto \mathcal C (I, \Theta \otimes S) \times \mathbf{Optic} (\mathcal C) ((\Psi, \Psi') \otimes (A, B), I)$

Jules Hedges (Jun 18 2021 at 17:21):

Then $\int^{\Theta \in \mathcal C} G ((\Theta, I), \Theta) \cong \mathbf{Optic} (\mathcal C) ((I, B), (S, A))$ and $\int^{(\Psi, \Psi') \in \mathbf{Optic} (\mathcal C)} G ((\Psi, \Psi'), \Psi) \cong \mathbf{Optic} (\mathbf{Optic} (\mathcal C)) (I, ((S, T), (A, B)))$

Guillaume Boisseau (Jun 18 2021 at 18:02):

ohh I see it, it works really well!

Jules Hedges (Jun 18 2021 at 18:13):

The thing I find weird is how it was so "obvious" by squinting at the right string diagrams, but that gave no hint that the proper proof would involve an adjunction or 2 uses of coyoneda. I'm used to string diagrams being unreasonably effective but this one seemed to be even more so than usual

Guillaume Boisseau (Jun 18 2021 at 20:09):

here's how I understand it: most of coend calculus is about adding and removing identities at the right location. The magic of string diagrams is that you don't need to do that because all those things already look the same. It's like trying to use the exchange law on the term formula; it's nonobvious where to apply it in a non-trivial case

Guillaume Boisseau (Jun 18 2021 at 20:11):

Mario's coend diagrams (https://www.ioc.ee/~mroman/publications/opendiagrams.pdf) could actually make the isomorphism both obvious and formal

Guillaume Boisseau (Jun 18 2021 at 21:08):

image-f4c263d6-3a38-4550-8421-a2c19f116201.jpg

Guillaume Boisseau (Jun 18 2021 at 21:08):

image-eab59090-2a18-4be4-be24-535c46ef458d.jpg

Guillaume Boisseau (Jun 18 2021 at 21:09):

Couldn't resist trying. It works! Hope it's legible