Consistent usage of essentially small collections

[ScriptRaccoon]

CatDat works with set-theoretic foundations based on sets and collections. Sets are also called small collections. But in many situations, collections appear that are only bijective to a set, either implicitly or explicitly. This calls for a term for such collections and a consistent usage of this term.

I went with "essentially small collection" in this PR, since it is consistent with the definition of a locally essentially small category (which was added months ago) and also because a discrete category is essentially small if and only if its collection of objects is essentially small in this sense. The page on foundations (/content/foundations) has been improved accordingly.

The usage of "small set" has been removed, since it is not compatible with the foundations we are using, or rather, it leaks an implementation detail (collections are also sets in a certain universe, just renamed). Instead, we should speak of sets, aka small collections.

While going through all usages of the term "small" in the repository, some usages turned out to be redundant, while others turned out to be wrong.

An example appears in the definition of an accessible category, where it was stated that there "is a (small) set of objects G such that ...". First of all, it is confusing (regardless of what we are working with here) to use parentheses in a definition, since this raises the unanswered question of whether the word in parentheses is required or not. As mentioned, "small set" is redundant and can simply be abbreviated to "set".

But a more important problem is that this definition of an accessible category is not entirely correct. A set has sets as elements. This means that the objects in G are sets. But there are accessible categories in nature whose objects (which must only be collections) are not sets. For example, it can happen that they are only isomorphic to sets. But it is not correct here anyway to go "inside" the structure of the objects. The definition of an accessible category should merely require that G is an essentially small collection of objects. (Equivalently, it can be "parametrized" by a set.) This has been fixed:

Let $\kappa$ be a regular cardinal. A category is $\kappa$-accessible if it has $\kappa$-filtered colimits and there is an essentially small collection $G$ of $\kappa$-presentable objects such that every object is a $\kappa$-filtered colimit of objects in $G$. A category is accessible if it is $\kappa$-accessible for some regular cardinal $\kappa$.

For similar reasons, the terminology "generating set" was not quite correct. This notion is now called a "generating collection", and it is essentially small by convention (since otherwise every category would have one). It is a bit unfortunate that we cannot simply use the term "generating set", which is much more common in the literature, but it is not correct since the objects of a category are not necessarily sets, so an essentially small collection of objects is not necessarily a set. The same changes apply to the related properties, which are now called: "extremal generating collection", "cogenerating collection", and "extremal cogenerating collection".

In issues on set-theoretic questions (#25, #83), my suggestion of an "essentially small collection" and of a "locally essentially small category" (which was added long ago) has been criticized because an essentially small collection of objects in a category does not necessarily constitute a full subcategory that is essentially small (namely, when the ambient category is not locally essentially small). To this, I would just respond that the identification between a collection of objects and a full subcategory should be made explicit, and this avoids any confusion. If we clearly speak, for example in the definition of an accessible category, about a collection of objects, I am convinced that no confusion can arise.

Another criticism was that "essentially small" already means "equivalent to a small category". But this is only true for categories. The new term applies to a completely different type of mathematical object, so there is no overlap as long as we distinguish the types properly, which we should do anyway. Compare this with the notions "exact category" and "exact functor", which cannot be confused as long as we do not identify a category with its identity functor.

Other set-theoretic formulations have been improved as well. For example, since diagrams and hence their limits are small by convention unless otherwise stated, it is redundant to write "small products", or even worse, "(small) products".

This PR was motivated by working on #365. For such categories, precise set-theoretic foundations are required.

[ScriptRaccoon]

FYI @varkor @dschepler. To summarize the most important changes:

• a collection isomorphic to a set is now called "essentially small"
• the term "small set" is banned
• "generating set" is now called "generating collection", and it is essentially small by convention (not a set)

⚠️ The objects of a category are not necessarily sets. Hence, an ess. small collection of objects is not necessarily a set.