# Sets, Universes, and the small Yoneda Lemma

Suppose we fix a universe $U$ and a $U$-small category $C$. The regular Yoneda lemma gives us some locally small (not necessarily locally U-small?) functor category $C'=[C^{op},Sets]$ with a fully faithful embedding $C\rightarrow C'$ and the canonical bijection between $Nat(F,Hom(-,x))$ and $F(X)$. Suppose we consider now, the U-small Yoneda lemma, that is, we look at $[C^{op},U-Sets]$. This is well-behaved since even though it is not U-small, $Ob([C^{op},U-Sets])$ is still a set.

So the main question I have is: Are there any useful properties of the standard Yoneda lemma that we cannot reproduce with the $U$-small Yoneda lemma for some $U$?

-

Well, for any universe U, the U-small sets satisfy the axioms of ZFC (or whatever your preferred set theory is). Therefore, anything that we can prove in ZFC about the Yoneda embedding into "all" presheaves will also be true about the Yoneda embedding into U-small presheaves. So on that score, the answer would seem to be "no."

There might be other interpretations that would make the answer "yes," since in vanilla ZFC every class is definable, whereas not every U-large set is definable in terms of U-small ones. Thus an informal statement like "for every large thingumbob X, ..." might be true in ZFC, but no longer provable relative to a universe, since the meaning of "large" has changed (unless we change the quantifier to "for every U-small-definable large thingumbob X"). This doesn't contradict the first observation, since such a statement cannot be a single theorem of ZFC, only a meta-theorem, and each instance of the meta-theorem is about a particular definable class and therefore still true about the corresponding U-small-definable U-large set. However, right now I can't think of any interesting or useful properties of the Yoneda embedding that would fall under this heading.

So I think that probably the answer is still "no."

-
Then why would we ever bother working with the proper class of all sets? It seems like it complicates things for no reason. –  Harry Gindi Nov 23 '09 at 2:17
I find the formalism of Grothendieck universes conceptually much simpler, too. –  Reid Barton Nov 23 '09 at 4:36
I can't answer that in 600 characters! –  Mike Shulman Nov 23 '09 at 16:04
Then write something up somewhere and link me, or just edit your answer here to avoid the character limit. –  Harry Gindi Nov 24 '09 at 0:46