Why is Nat(hom(A,-),F) a class?

[rasmhop]

I'm trying to read a bit up on category theory, but I'm a bit confused about one aspect of the proof of Yoneda's lemma. Suppose we have a locally small category C, a functor $F : C \to \textrm{Set}$ and an object A in C. Now according to Yoneda's lemma there exists a bijection from $Nat(hom(A,-),F)$ to $FA$. Assuming $Nat(hom(A,-),F)$ is a class I can easily construct an explicit bijection which shows that $Nat(hom(A,-),F)$ is actually a set. However all sources I have looked at take it for granted that $Nat(hom(A,-),F)$ is a class and simply starts by defining a function $\Theta_{F,A} : Nat(hom(A,-),F) \to FA$ and then shows that it's bijective. I'm not convinced that $Nat(hom(A,-),F)$ actually exists and isn't contradictory in some way though. I guess it's something obvious I'm missing as it's always left out, but I would appreciate it if someone would tell me what I'm missing.

 

[Hurkyl]

Hrm. I think you have a legitimate question, there.

Well, the easiest answer is to use foundations that include large cardinals. Hom(A,-) and F are just large sets, and so Nat is a large set of large sets.

Second-order ZFC should do the trick too. Hom(A,-) and F are first-order classes, so Nat(Hom(A,-), F) would be a second-order class.

I think you could manage the same trick in first-order NBG, since Hom(A,-) and F are classes (in the sense of being objects), and Nat(Hom(A,-),F) would be a class (in the sense of being a logical predicate).

 

[rasmhop]

Thanks for the answer. That makes sense.

For a fixed object $B$ in category C both hom(A,B) and FB are sets so the class of functions from hom(A,B) to FB is a set. Hence if $\eta$ is a natural transformation from hom(A,-) to F, then $\eta_B$ is a set and thus $\{\eta_B | B \in ob(C)\}$ is a class in the sense of NBG. Hence we can define Nat(hom(A,-),F) in terms of a formula $\varphi(x,p_1,\ldots,p_n)$ where $p_1,\ldots,p_n$ are free variables and x is a class. This is sufficient to allow us to set up the bijection from Nat(hom(A,-),F) to FA in the usual sense and that shows that Nat(hom(A,-),F) is actually a set.

It just seems odd to me that such an argument is omitted, and I still wonder whether there is some easier way to do this that doesn't resort to using logical predicates.