Coend computation

Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

Let

$F:A^{\mbox{op}} \to \mbox{Set}$

and define

`$G_a:A\times A^{\mbox{op}} \to \mbox{Set}$`

`$G_a(b,c) = \mbox{hom}(a,b) \times F(c)$`.

I think the coend of `$G_a$`,

`$\int^AG_a$`,

ought to be $F(a)$--it's certainly true when A is discrete, since then hom is a delta function. But my colimit-fu isn't good enough to actually compute the thing and verify it's true. Can someone walk me through the computation, please?

-
is this a category-theoretic analogue of the main theorem of the fundamental theorem of calculus? – Martin Brandenburg Apr 6 2010 at 0:13

2
@Martin: an FToC analogue would require a 'boundary' computation of some sort. This seems more like a distribution computation, where the hom works like $\delta(a-b)$, so the integral over the whole space is just evaluation. – Jacques Carette Apr 6 2010 at 3:20

1 Answer

Hi Mike. This is what's often called the Density Formula, or (at the n-Lab) the coYoneda Lemma (I think), or (by Australian ninja category theorists) simply the Yoneda Lemma. (But Australian ninja category theorists call everything the Yoneda Lemma.) In any case, it's a kind of dual to the ordinary Yoneda Lemma.

But you asked to be walked through it. First: yes, it is $F(a)$. Another way of writing your coend $$\int^A G_a$$ is as $$\int^{b \in A} G_a(b, b) = \int^b \mathrm{hom}(a,b) \times F(b).$$ I claim this is canonically isomorphic to $F(a)$. I'll prove this by showing that for an arbitrary set $S$, the homset $\mathrm{hom}(\mathrm{this}, S)$ is canonically isomorphic to $\mathrm{hom}(F(a), S)$. The claim will then follow from the ordinary Yoneda Lemma.

So, let $S$ be a set. Then ```$$
\begin{align}
\mathrm{Set}(\int^b \mathrm{hom}(a, b) \times F(b), S) &
\cong 
\int_b \mathrm{Set}(\mathrm{hom}(a, b) \times F(b), S) \\
&\cong 
\int_b \mathrm{Set}(\mathrm{hom}(a, b), \mathrm{Set}(F(b), S)) \\
&\cong 
\mathrm{Nat}(\hom(a, -), \mathrm{Set}(F(-), S)) \\
&\cong 
\mathrm{Set}(F(a), S)
\end{align}
$$``` I don't know how much of this you'll want explaining, so I'll just say it briefly for now. If you want further explanation, just ask. The first isomorphism is kinda the definition of colimit. The second is the usual exponential transpose/currying operation. The third is maybe the most important: it's a fundamental fact about ends that if $F, G: C \to D$ are functors then $$\mathrm{Nat}(F, G) = \int_c D(F(c), G(c)).$$ The fourth and final isomorphism is the ordinary Yoneda Lemma applied to the functor $\mathrm{Set}(F(-), S)$.

-
I'm a little confused by your notation: specifically, what is the category $\mathrm{Nat}$? From the types its objects are functors $A^{op} \to \mathrm{Set}$, so it's the functor category whose objects are the natural transformations between those functors? – Neel Krishnaswami Apr 6 2010 at 14:14
FWIW You can formalise the steps in the construction of this isomorphism as a Haskell program. Here's one direction, with `f` being the relevant morphism: hpaste.org/fastcgi/hpaste.fcgi/view?id=24722 I suspect that by interpreting Haskell code as the internal language of some family of categories then this becomes a perfectly good definition of the isomorphisms for mathematical purposes too, and not just a statement about some Haskell functions. – Dan Piponi Apr 6 2010 at 16:53
Thanks! The third step is really the one I need to understand, so I'll think about that for a while and come back if I need more help. – Mike Stay Apr 6 2010 at 18:30

1
Neel, I guess Nat is a slightly unspecific notation, like hom. The first occurrence of Nat meant "hom in $[A^{op}, \mathrm{Set}]$". Here $[A^{op}, \mathrm{Set}]$ is the category whose objects are functors $A^{op} \to \mathrm{Set}$. So: Nat is not a category; it means "hom" in that functor category. I might equally well have written "$[A^{op}, \mathrm{Set}]$" in place of "Nat". (In fact I prefer to; I was making a perhaps misguided effort to be more widely comprehensible.) Similarly, the second occurrence of "Nat" could be replaced by "$[C, D]$". – Tom Leinster Apr 6 2010 at 20:08

1
Ah, thanks -- I've just never seen Nat used like that before. Amusingly, the $[A^{op}, \mathrm{Set}]$ notation is the one I've seen before. :) – Neel Krishnaswami Apr 6 2010 at 22:43
show 1 more comment
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 19, "mathjax_display_tex": 3, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": false, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9310299754142761, "perplexity_flag": "middle"}