You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Davi Sales Barreira (Apr 09 2023 at 18:16):On the book "Handbook of Categorical Algebra - Vol I" the author writes:
"Again a careless argument would deduce the existence of a category whose objects are the functors from
to and whose morphisms are the natural trasnformation between them. But since and
have merely classes of objects, there is in general no way to prove the existence of a set of natural transformations between two functors! But when is small, that problem disappears..."
I noticed that in many other sources I've read, the claim of a category of functors between two categories is simply assumed to exist by postulating that functors are the objects, and natural transformations are the morphisms together with the vertical composition...
Hence, my question is how can we construct category of functors when the underlying categories are not small. I'm assuming this is possible, as people usually talk about categories such as [๐๐๐ญ,๐๐๐ญ], where ๐๐๐ญ is only locally small.
Moreover, the definition of natural transformations requires indexing
by . How can we then claim that a natural transformation exists between two functors when the domain category
has a non-set class of objects?
John Baez (Apr 09 2023 at 19:11):Davi Sales Barreira said:
I noticed that in many other sources I've read, the claim of a category of functors between two categories is simply assumed to exist by postulating that
Hence, my question is how can we construct category of functors when the underlying categories are not small.
John Baez (Apr 09 2023 at 19:16):One approach is to allow these functor categories to have hom-classes rather than hom-sets - i.e., to not be locally small. Another approach, a more refined version of the same idea, is to use the axiom of universes and let the hom-sets be 'large' sets.
Davi Sales Barreira (Apr 09 2023 at 19:18):Thanks, @John Baez . I see now that in the Handbook of Categorical Algebra, the author is assuming categories to always be locally small... Hence the claim that such category might not exists.
Davi Sales Barreira (Apr 09 2023 at 19:18):About the indexing issue... I for a moment tought that constructing things (e.g. natural transformations) via indexing was only "allowed" for sets... My guess is that this is a wrong assumption?
Mike Shulman (Apr 09 2023 at 21:54):This sort of question gets into some complicated questions of mathematical foundations and what you mean by a "set" or a "small" category. If you work in ZFC and take "small" to mean "a set" and "large" to mean "a class", then you cannot even talk about the collection of all functors between two large categories, let alone the category of such. You can talk about any individual such functor, but each such functor is itself a class, and proper classes in ZFC are not the "elements" of any kind of collection.
Mike Shulman (Apr 09 2023 at 21:56):Often people find this annoying, and so they use a different foundational system. E.g. if you assume the existence of a Grothendieck universe and define "small" to mean "element of " and "large" to mean "set not necessarily in ", then there is a perfectly good large category of functors between any two large categories. But now you don't any more have a category of all sets, only of the small sets.
Mike Shulman (Apr 09 2023 at 21:56):I wrote at length about some of the various options for how to use set theory for category theory in https://arxiv.org/abs/0810.1279.
Davi Sales Barreira (Apr 10 2023 at 11:40):Thanks, @Mike Shulman . One question regarding universes, I was under the impression that using the universes one would still require something to be a "small set" in order to index on it. I'm guessing this is not the case?
Mike Shulman (Apr 10 2023 at 15:49):That's correct, when we use universes, nothing prevents us from talking about families indexed by large sets. In that case large sets are just a particular kind of sets, so we can use all of ordinary set theory to talk about them.
Of course, in some particular application we may only be interested in families indexed by small sets. For instance, a large category is "complete" if it has limits for diagrams indexed by all small categories.
John Baez (Apr 10 2023 at 16:23):One reason I said using universes is a "more refined version" of working with classes is that large sets, unlike classes, are still sets, so you can still do all the usual stuff with them. Another is that the [[axiom of universes]] gives you an infinite hierarchy of small sets, large sets, extra-large sets, extra-extra-large sets, etc. - all of which are still sets.
John Baez (Apr 10 2023 at 16:24):So you have a lot of flexibility in working with things like the category of large categories, which is an extra-large category.
Josselin Poiret (Apr 11 2023 at 07:27):John Baez said:
One reason I said using universes is a "more refined version" of working with classes is that large sets, unlike classes, are still sets, so you can still do all the usual stuff with them. Another is that the [[axiom of universes]] gives you an infinite hierarchy of small sets, large sets, extra-large sets, extra-extra-large sets, etc. - all of which are still sets.
one thing to note is that this is basically how type theories and hence proof assistants do it! In Coq the universe levels are hidden from you, but in Agda you have to specify them yourself.
Mike Shulman (Apr 11 2023 at 15:29):Nowadays Coq also allows you to specify the universe levels manually if you need to.