proper class

Proper classes

Proper classes


A proper class is a set that is too big to be a set. Exactly what this means depends on the foundations of mathematics, but something must be said about it to study large categories.


There are several ways to deal with this and define a proper class.

A proper class is a large discrete category. But since a large category is usually defined as having a proper class of objects, this just moves the bubble under the wallpaper to ‘large category’ and something must be applied there.

A proper class is a collection that can be put in bijection with the class of all ordinals, OrdOrd. But this requires the global axiom of choice to be correct.

A proper class is a class that is not a set. So now we have to define ‘class’.

A proper class is a class whose cardinality is not the cardinal number of any set. This is a version of the previous definition not violating the principle of equivalence; however, in some foundations these are actually equivalent (using the axiom of replacement).

A class is a collection of sets. Here the bubble is moved to ‘collection’, but we will be able to pop that bubble below. Also we might want to allow the members of a proper class to be other than sets (such as structured sets); certainly it is true, however, that a pure class is a collection of pure sets.

A class is a formula in the language of set theory for a truth value, equipped with a specified free variable for a set. This is a formalisation of the previous definition, but it must be interpreted metamathematically: a formula for a class in a given context Γ\Gamma is a formula for a truth value in the extension of Γ\Gamma by one more free variable for a set.

A class may even be an undefined concept; the real definition is to define a set as a class that is itself a member of some class. With appropriate axioms, this is equivalent to the previous definition (and conservative over set theory without classes), but it's also possible to apply stronger axioms here; this choice is the difference between BNGBNG and MKMK as extensions of ZFC.

A class is a subset of a Grothendieck universe UU, while a (small) set is merely an element of UU. This gives a relative notion, depending on UU. As stated here, we get a concept of class like that of the strong theory MKMK; to be more like BNGBNG (and therefore conservative over set theory without an axiom of universes) we should define a class to be a subset of UU that is definable in the language of set theory.


A large category is a category whose class of morphisms is a proper class. It is sufficient that the class of objects be a proper class, which is also necessary if the category is locally small.

Category theorists care about proper classes because many examples of categories in practice (such as Set, to begin with!) are large.

Category of classes

The category of classes ClassClass is a large category that is not locally small. It admits all colimits, understood in the following sense.

First, given a class II, we define an II-indexed family of classes as a map of classes f:TIf:T\to I. The preimage f 1({i})f^{-1}(\{i\}) is precisely the class with index ii. Such families can be pulled back along maps of classes JIJ\to I and pushed forward along maps IJI\to J.

Next, given a category II (not necessarily locally small), we define an II-indexed diagram of classes as a pair (o:T OOb(I),m:T MMor(I))(o:T_O\to Ob(I),m:T_M\to Mor(I)) of indexed families of classes that satisfies the obvious reformulation of conditions in the definition of a functor.

We now claim that an arbitrary II-indexed diagram of classes admits a colimit.

First, the standard reduction of II-indexed colimits to a coequalizer of a pair of arrows between coproducts indexed by Mor(I)Mor(I) and Ob(I)Ob(I) still works in this context since class-indexed families of classes can be pulled back along source and target maps Mor(I)Ob(I)Mor(I)\to Ob(I).

Secondly, class-indexed coproducts of classes can be computed simply by taking the total class of the corresponding class-indexed family of classes.

Thirdly, coequalizers of classes exist by Scott's trick. Observe that given a pair of arrows f,g:XYf,g:X\to Y between classes, we can define an equivalence relation on YY by saying that y~yy~y' if there is a map h:[0,n]Yh:[0,n]\to Y such that h(0)=yh(0)=y, h(n)=yh(n)=y' and for any i[0,n)i\in[0,n) there is xXx\in X such that h(i)=f(x)h(i)=f(x) and h(i+1)=g(x)h(i+1)=g(x) or h(i)=g(x)h(i)=g(x) and h(i+1)=f(x)h(i+1)=f(x). The quotient of YY by this equivalence relation exists by Scott's trick and is precisely the desired coequalizer.

If one is working in the category of (definable) classes for ZF or ZFC, or the category of classes of NBG, then all finite external diagrams DClassD\to Class have colimits. The reduction to a coequaliser of a pair of finite coproducts works as per usual. Finite coproducts exist as one can use finite disjunctions of the defining formulas (in ZF(C)) or Class Separation (in NBG) to define a new class. Coequalisers then exist by the above argument, as Scott's trick is available due to the class VV of sets having well-founded stratifications by sets (for instance the von Neumann cumulative hierarchy V= αORDV αV = \bigcup_{\alpha\in ORD} V_\alpha).

Just as an elementary topos is an axiomatization of basic properties of the category Set, a category with class structure is an axiomatization of basic properties of the category ClassClass. See also algebraic set theory.


A paper detailing one approach to the technical side of how classes appear in category theory (namely using Grothendieck universes) is

  • Paul Blain Levy, Formulating Categorical Concepts using Classes (arXiv:1801.08528)

Last revised on November 30, 2019 at 01:19:36. See the history of this page for a list of all contributions to it.