Proof verification: Yoneda preserves limits

$\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?

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.