Proof verification: Yoneda preserves limits

Question

$\newcommand{cop}{C^{op}}$ $\newcommand{cSet}{\mathsf{Set}}$ $\newcommand{Hom}{\operatorname{Hom}}$ $\newcommand{\eval}{\operatorname{eval}}$ Let $J$ be a small category, and let $C$ be locally small. Let $F: J \to C$ be a diagram in $C$ and let this have a limit $\lim F \in C$. Let $Y: C \to [\cop, \cSet]$ be the Yoneda functor given by $Y(c) \equiv \hom(-, c)$. Now we claim that $Y(\lim F)$ is a limit, and is given by $\lim (Y \circ F)$. This is the claim that the Yoneda functor preserves limits, and I provide a proof below which I would like to have vetted.

Proof

Consider the right hand side, $\lim (Y \circ F) \in [\cop, \cSet]$. This is a limit in a functor category, where limits are computed pointwise. Formally, this means that $[\lim (Y \circ F)](c) =\lim (\eval_c \circ Y \circ F)$ where $\eval_c: [\cop, \cSet] \to \cSet$ is the evaluation functor, whose action on objects (functors) is to evaluate the functor at $c$ --- $\eval_c(F) \equiv F(c)$, and whose action on morphisms (natural transformations) is to pick the component at $c$ --- $\eval_c(F \Rightarrow_\eta G) \equiv \eta_c$ .

Now, in the case of yoneda, we example $\lim (eval_c \circ Y \circ F)$, which can be written as $\lim (j \mapsto \eval_c(Y(F(j)))$. Plugging in the definition of $Y$, this is equal to $\lim (j \mapsto \eval_c(\Hom(-, F(j)))$. Now plugging in $\eval_c$, this is equal to $\lim (j \mapsto Hom(c, F(j))$. This can be written as $\lim (Hom(c, F(-))$.

Since the $\Hom$ functors preserve limits, we can write $\lim (\Hom(c, F(-)) = \Hom(c, \lim F)$. Plugging this back into where we started, we find that $[\lim (Y \circ F)](c) = \lim (\eval_c \circ Y \circ F) = \Hom(c, \lim F)$. we re-introduce $Y$ on the right-hand-side by writing $\Hom(c,\lim F)$ as $\eval_c \circ Y \circ \lim F$. This gives us the equality $[\lim (Y \circ F)](c) = \eval_c \circ Y \circ \lim F$.

Finally, ranging over all $c$, we remove the $\eval_c$ on the right-hand side to arrive at $[\lim (Y \circ F)] = Y \circ \lim F$ which is the equality $\blacksquare$

---

Is the proof correct? Can I simplify it? I find that the proof does a lot of 'definition chasing', so maybe there is a succinct way to phrase this?

What is the moral of the proof? What I took away from this was that (a) limits in functor categories are computed pointwise, (b) $\Hom$ preserves limits (c) Pointwise Yoneda is $\Hom$, thus Yoneda preserves limits. Is this an accurate summary?

Answer 1

For your first question, is the proof correct, the answer is yes, with the minor caveat that you should replace your equality signs with natural isomorphisms (because a limit is only defined up to natural isomorphism unless you've selected a particular limit, so asserting an equality with limits is meaningless).

As for the moral of the proof, you've given an accurate summary of the proof you gave.

An alternate perspective

The main reason I'm answering is to give an alternate perspective on limits that should make this fact obvious.

One definition of limit is the following: The limit of a diagram $\newcommand\C{\mathcal{C}}F:J\to \C$ is an object $c\in\C$ together with a natural isomorphism $\C(-,c)\simeq \lim_j\C(-,F(j))$ (where we've defined limits in $\mathbf{Set}$ already. The right hand side is the functor that assigns to an object $d$ the set of cones from $d$ to $F$, so if you follow through the argument of the Yoneda lemma, you can see that this is equivalent to an object $c$ together with a universal cone from $c$ to $F$.

In other words definitionally, a limit for $F$ is an object $c$ with a natural isomorphism $$ Y(c) \simeq \lim Y\circ F, $$ so from this perspective the fact that Yoneda preserves limits is actually just how we define limits.

The value of this perspective

To be clear, from one point of view the entire proof here is in the justification of the first line where I tell you to trace through and check that this is the same as the "usual" definition of the limit. And that's definitely true.

I'm really just trying to get at a different way of understanding the concept of limits in category theory as starting off being defined as objects representing a particular functor. This turns out to be a super helpful way of thinking about universal objects in general, but is also critical to generalizing limits to, for example, weighted limits in enriched category theory.

The basic idea here is that we ought to think of the Yoneda lemma as embedding our category in a larger one. We can then construct new objects in this larger category where we have more tools and then try to figure out if these new objects are representable.

Answer 2

FWIW, one can also prove the result by contemplating the definition of limits as representing the relevant functor of cones and then throwing Yoneda's lemma at it a couple times.

In particular, given a category $\textbf{C}$ and a diagram $\text{F}\ \colon\ \textbf{D}\to\textbf{C}$ with limit $\text{lim}\left(\text{F}\right)$, construct the Yoneda embedding $$よ\ \colon\ \textbf{C}\to\textbf{C}^{\text{op}}\to\textbf{Set}$$ and observe the following chain of isomorphisms natural in $\text{c}$ as it varies over $\textbf{C}^{\text{op}}$: \begin{align*}よ\left(\text{lim}\left(\text{F}\right)\right)\left(\text{c}\right)\ &\simeq\ \text{c}\Rightarrow\text{lim}\left(\text{F}\right)\\ &\simeq\ \text{Cones}_{\text{F}}\left(\text{c}\right)\\ &\simeq\ \text{Cones}_{よ\circ\text{F}}\left(よ\left(\text{c}\right)\right)\\ &\simeq\ よ\left(\text{c}\right)\Rightarrow\text{lim}\left(よ\circ\text{F}\right)\\ &\simeq\ \text{lim}\left(よ\circ\text{F}\right)\left(\text{c}\right)\end{align*} where

• The first isomorphism is tautological from the definition of $よ$.

• The second isomorphism is tautological from the definition of the limits of a diagram as representing the functor of cones over said diagram with vertex the argument.

• The third isomorphism is from that the Yoneda embedding is fully faithful.

• The fourth isomorphism is tautological from the definition of the limits of a diagram as representing the functor of cones over said diagram with vertex the argument.

• The fifth isomorphism is by the Yoneda lemma.

and where all limits in question extant because, as you mention, limits in functor categories that exist in the codomain evaluate pointwise, and $\textbf{Set}$ is complete. $\blacksquare$

---

P.s.: Instead of starting with that hom commutes with limits (in the covariant argument) and then deducing via the pointwise evaluation of limits in functor categories that exist in the codomain that the Yoneda embedding commutes with limits, one can via the above actually start with that the Yoneda embedding commutes with limits and then use the pointwise evaluation of limits in functor categories that exist in the codomain in conjunction with the completeness of $\textbf{Set}$ to deduce that hom commutes with limits (in the covariant argument).