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: Computing (co)ends

Harrison Grodin (Dec 28 2023 at 15:01):

When can I expect a coend (over a large category) to exist? For simplicity, let's say we're only working in $\mathbf{Set}$. Suppose I have a profunctor $P : \mathbf{Set}^\text{op} \times \mathbf{Set} \to \mathbf{Set}$. How can I know if the coend $\int^\mathbf{Set} P$ exists; and if it exists, is there a good way to compute it?

In case this is tricky for all $P$, is there a nice class of profunctors for which the question becomes easier (maybe compositions of products, coproducts, and exponentials or something)?

Jade Master (Dec 28 2023 at 15:32):

@Harrison Grodin I know of two explicit ways to compute a coend. One is by taking a coequalizer of a certain diagram. The other is by taking the colimit over its category of elements. You can get the first by dualizing this nlab and the second way is also on the same article. It's here. I think if you are only considering $Set$-valued profunctors then all such coends exist because $Set$ has all colimits.

Harrison Grodin (Dec 28 2023 at 15:37):

Thanks Jade! I guess I was a bit concerned about size issues - can I take $\mathbf{Set}$-wide coproducts in $\mathbf{Set}$? Or, for the second link, it seems like $D$ has to be a small category?

Harrison Grodin (Dec 28 2023 at 15:40):

(I would believe that all coends exist - this would be great! All the examples I've tested manually seem okay. But, my "guess and check" strategy doesn't constitute a proof, and it wasn't clear to me that I could take these large colimits in all cases.)

Jade Master (Dec 28 2023 at 15:41):

Yes you're right. Saying Set has all colimits needs qualification. I'm sort of ignorant of the size stuff, but I think it's something like: to get colimits which are as wide as small sets you need to be in a universe with large sets.

Todd Trimble (Dec 28 2023 at 15:44):

For $G: C \to Set$, the coend $\int^c Gc \cdot C(c, d)$ exists and equals $Gd$, even if $C$ is large; this is a version of what is sometimes called the "co-Yoneda lemma". That this holds for large categories is treated in Kelly's book.

If $F$ is a small colimit of representables, then $\int^c Gc \cdot Fc$ also exists, even if $C$ is large.

Harrison Grodin (Dec 28 2023 at 16:05):

Thanks! I was hoping to compute coends like $\int^c C(Hc, Ic) \cdot C(c, d)$, for example, where $H, I : C \to C$. (As a concrete example, let $Hc = 1 + c^2$ and $Ic = c$.) It doesn't quite seem to fit the co-Yoneda pattern, since $Gc$ is replaced by a profunctor $C(Hc, Ic)$; do you know if there's a similar result saying that this style of coend exists?

Jade Master (Dec 28 2023 at 16:27):

Harrison Grodin said:

Thanks! I was hoping to compute coends like $\int^c C(Hc, Ic) \cdot C(c, d)$, for example, where $H, I : C \to C$. (As a concrete example, let $Hc = 1 + c^2$ and $Ic = c$.) It doesn't quite seem to fit the co-Yoneda pattern, since $Gc$ is replaced by a profunctor $C(Hc, Ic)$; do you know if there's a similar result saying that this style of coend exists?

Where does the d come from in this coend? I'm not sure about this coend, but here's another coend formed from two polynomial functors that I find interesting. First take the profunctors $C(-,H(-))$ and $C(I(-).-)$ and then take the coend $\int^b C(a,H(c)) \cdot C(I(b),c)$ (which is actually the profunctor composition valued on the pair (a,c) )

Harrison Grodin (Dec 28 2023 at 16:47):

In Todd/my messages, $d$ is just some fixed object in $C$. [Typo - do you mean $H(b)$?] The coend you described is quite nice!

Mike Shulman (Dec 28 2023 at 16:48):

This doesn't answer your specific question, but another class of large coends that exist is $\int^c Gc \cdot c$ for any $G: \mathrm{Set}^{\mathrm{op}} \to \mathrm{Set}$. This is because Set is a [[total category]]; see also [[large cocompleteness]].

fosco (Dec 29 2023 at 10:04):

Harrison Grodin said:

In Todd/my messages, $d$ is just some fixed object in $C$. [Typo - do you mean $H(b)$?] The coend you described is quite nice!

What Todd mentioned (a presheaf that results as a small colimi of representables) is usually called a "small" presheaf. Handling the category of small presheaves on $C$ is often quite difficult. But some results stay true. I think the clas of profunctors you want to compute the coend of will likely be small (as soon as they are polynomials, indexed on a set, for example, you'll be fine.)

:smile: Also, give me more coends to compute! I have fun with that.

Harrison Grodin (Dec 29 2023 at 15:27):

Thanks, Fosco, for the response and for the excellent book!!

I think the clas of profunctors you want to compute the coend of will likely be small (as soon as they are polynomials, indexed on a set, for example, you'll be fine.)

I think I will probably want products of exponentials, where the domains and codomains are polynomials. For example, things like:

$$\int^{X : \mathcal{C}} X^{1 + X^2} \times (X + 1)^{\mathbb{N} \times X} \times \mathbb{N}^X$$

Does it seem plausible that this kind of thing would exist in $\mathbf{Set}$? Or even better, if $\mathcal{C}$ is a ($\mathbf{Set}$-enriched) category (like the category of algebras for a monad) and the profunctor is $\mathcal{C}^\text{op} \times \mathcal{C} \to \mathbf{Set}$, might this exist?

All of my desired examples are inspired by impredicative encodings ($\forall$/$\exists$ types) in type theory. Some fun ones I've been thinking about accordingly:

• $\int_X X^A \Rightarrow X$
• $\int_X (FX \Rightarrow X) \Rightarrow X$ (where $F$ is a functor)
• $\int^X (X \Rightarrow FX) \times X$ (where $F$ is a functor)

I think the answers are:

(By the way, I would assume someone has thought about all of these. Is there a known reference for them?)

fosco (Dec 29 2023 at 16:22):

When the integration variable appears a certain number of times covariantly, and another number contravariantly, do you interpret it "diagonalizing completely" all the occurrences? Meaning: are you considering the coend of ${\cal C}^{op}\times {\cal C} \to {\cal C}^{-2}\times {\cal C}^3 \to \cal C$ sending $(Y,X)$ to $X^{1+Y^2}\times (X+1)^{\mathbb N \times Y} \times \mathbb N^Y$?

fosco (Dec 29 2023 at 16:24):

If yes, these are "coends of higher arity", which reduce to (1,1)-ary coends, cf. https://arxiv.org/abs/2011.13881 (I'm using a similar notation, ${\cal C}^{-p} \times {\cal C}^q$ is the product of $p$ copies of $\cal C^{op}$ and $q$ copies of $\cal C$.

fosco (Dec 29 2023 at 16:26):

Their existence is now a matter of smallness, and I believe these exist. As far as computing them, it often is a mess :grinning:

Harrison Grodin (Dec 29 2023 at 16:30):

Yes, I'm thinking about diagonalizing completely. (I was thinking of $\mathcal{C}^\text{op} \times \mathcal{C} \to \mathcal{C}$, but I suppose the type you gave works too?)

fosco (Dec 29 2023 at 16:31):

Regarding your examples, do you know about Neumann's "Paranatural co/ends"? See proposition 4.4 here https://arxiv.org/pdf/2307.09289.pdf, where the "structural end" $\int X^{TX}$ for an endofunctor T of $Set$ is the carrier of the initial T-algebra. Paranatural ends, i.e. terminal paranatural wedges, coincide with terminal wedges (because wedges and parawedges coincide, although this simple observation isn't made in Neumann's paper), so the carrier of the initial T-algebra of a functor is the end $\int_X X^{TX}$ (provided the equalizer formula given in Neumann yields the terminal parawedge, which I haven't been able to see).

Harrison Grodin (Dec 29 2023 at 16:36):

Oh, yes, of course this would be in there!! I'll look further, thanks!