[Math] co-Yoneda lemma and representable functors

category-theory

I'm interested in the fact that every presheaf on a category $C$ is a colimit of representable functors. The nLab claims that this can be stated as:
$$F \simeq \int^{c \in C} Y(c) \otimes F(c)$$
Where $F: C^{op} \to \mathbf{Set}$ and $Y: C \to [C^{op}, \mathbf{Set}]$ is the Yoneda embedding. This can reasonably be called the co-Yoneda Lemma.

The fact that every presheaf can be expressed as a colimit of representables can be proven by shown that:
$$F \simeq \mathrm{colim}\left(\left(\int F\right)^{op} \to C \xrightarrow{Y} [C^{op}, \mathbf{Set}] \right)$$
Here $\int F$ is the category of elements. This is proven for example in Mac Lane, Moerdijk – Sheaves in geometry and logic. My question is:
Is there an easy proof for
$$\int^{c \in C} Y(c) \otimes F(c) \simeq \mathrm{colim}\left(\left(\int F\right)^{op} \to C \xrightarrow{Y} [C^{op}, \mathbf{Set}] \right)$$
The co-Yoneda Lemma and the statement about presheaves seem to be linked by that fact, and the literature suggests (by interchanging the results without mentioning the isomorphism) that this is somehow easy to see, but the only proof I know is by showing the first two identities.

Best Answer

Let: $$\Gamma = \operatorname{colim} \left\{ \left(\int F\right)^{op} \to C \to [C^{op}, \mathbf{Set}] \right\}.$$

Then a morphism $u : \Gamma \to Z$ is the same thing as a collection of morphisms: $$u_{c,x} : Y(c) \to Z$$ for all $c \in C$ and $x \in F(c)$, such that if $\varphi : d \to c$ is a morphism in $C$, then the obvious commutative diagram commutes. More precisely, we should have: $$u_{d, F(\varphi)(x)} = u_{c,x} \circ Y(\varphi). \tag{1}$$

This collection is the same thing as a collection $U_c : Y(c) \times F(c) \to Z$ for $c \in C$, defined by: $$U_c(\xi, x) = u_{c,x}(\xi)$$ for all $c \in C$, $x \in F(c)$ and $\xi \in Y(c)$. If you inspect what the equation $(1)$ means for $U$, you will see that it exactly means that $U$ can factor through the coequalizer that usually defines the coend: $$\int^{c \in C} Y(c) \times F(c) = \operatorname{coeq} \left\{ \bigsqcup_{c,d} Y(c) \times F(d) \rightrightarrows \bigsqcup_c Y(c) \times F(c) \right\}$$ And we can check that this defines a bijection on the level of $\hom$-sets (the reverse construction, given some $U$, simply sets $u_{c,x}(\xi) = U_c(\xi,x)$): $$\hom(\Gamma, Z) \cong \hom(\int^c Y(c) \times F(c), Z).$$ I'll let you check that it's natural in $Z$ (simple exercise in definitions), so that finally: $$\Gamma \cong \int^c Y(c) \times F(c).$$

Related Question