Adjusting the definition of a well-powered category to category theory with universes: size issues

Question

Wikipedia and Borceux (Handbook of Categorical Algebra, Part I) give the following definitions of subobjects and well-powered categories:

A subobject of an object $X$ of a category $\mathsf{C}$ is an equivalence class of the equivalence relation $\equiv$ on the class of all monomorphisms with codomain $X$ where $f \equiv g$ whenever there is an isomorphism $h$ such that $g = f\circ h$.

A category $\mathsf{C}$ is well-powered if, for any $X \in \mathsf{C}$, all subobjects of $X$ form a set.

There are two different approaches to handling size issues with universes, although they agree on what a (Grothendieck) universe is. One, following Grothendieck, declares that, for a universe $\mathcal{U}$,

a set $X$ is $\mathcal{U}$-small if it is isomorphic to an element of $\mathcal{U}$, a category $\mathsf{C}$ is $\mathcal{U}$-category if its $\mathsf{Hom}$-sets are $\mathcal{U}$-small and it is $\mathcal{U}$-small if it is a $\mathcal{U}$-category and with $\mathsf{Ob(C)}$ being $\mathcal{U}$-small.

This approach depends heavily on Bourbaki set theory and the global choice operator $\tau$. For example, a covariant $\mathsf{Hom}$-functor $\mathsf{Hom}(X,-)\colon\mathsf{C}\to\mathcal{U}\text{-}\mathsf{Set}$ doesn't actually send $Y \in \mathsf{C}$ to $\mathsf{Hom_C}(X,Y)$ but merely to a set in $\mathcal{U}$ isomorphic to it. Another approach (which I'm not sure due to whom, but the book Higher Categories and Homotopical Algebra by Cisinski and the paper Homotopy Limit Functors on Model Categories and Homotopical Categories by Dwyer-Hirschhorn-Kan-Smith use this approach) is to declare that

a set $X$ is $\mathcal{U}$-small (or a $\mathcal{U}$-set, the form which I will use here to avoid confusion) if it belongs to $\mathcal{U}$, a category $\mathsf{C}$ is a $\mathcal{U}$-category if objects constitute a subset of $\mathcal{U}$ and all $\mathsf{Hom}$-sets are actually $\mathcal{U}$-sets and it is $\mathcal{U}$-small if it is a $\mathcal{U}$-category whose set of objects is a $\mathcal{U}$-sets.

My question regards the latter approach.

Now an obvious choice for a category to be called $\mathsf{C}$ a $\mathcal{U}$-well-powered is to have a $\mathcal{U}$-set of subobjects as in the definition above. However, this turns out to be useless, since it is not true for most of the categories that we want to be well-powered (again, in the category $\mathcal{U}\text{-}\mathsf{Set}$ of $\mathcal{U}$-sets the set $\bigcup_{Y \in \mathcal{U}} X^Y$ is generally not a $\mathcal{U}$-set). Another approach is to make an exception and relax the definition of $\mathcal{U}$-"smallness", requiring the set of equivalence classes to be $\mathcal{U}$-small in the sense of the first definition. This will now exclude any categories which should be well-powered as when we demanded that the set in question actually belong to $\mathcal{U}$. However, this is not in line with the philosophy of second approach and will probably turn out to be useless in applications if we stick with it.

Now I think of redefining a subobject of $X$ to be any monomorphism with codomain $X$ (some books do this, like Riehl's Category Theory in Context) and to say that

a category $\mathsf{C}$ is $\mathcal{U}$-well-powered if, for any $X \in \mathsf{C}$, there exists a $\mathcal{U}$-set of monomorphisms with codomain $X$ containing precisely one monomorphism for each equivalence class of the aforementioned equivalence relation $\equiv$.

This is stronger than requiring each equivalence class to be a $\mathcal{U}$-small, but it seems to work for the usual categories such as those of sets, groups, topological spaces, etc.

What I'm not sure about is how useful will it be if we work with $\mathcal{U}$-sets rather than $\mathcal{U}$-small sets (in particular, if our $\mathcal{U}$-categories have $\mathcal{U}$-sets of morphisms between every two objects rather than simply $\mathcal{U}$-small sets). I thought a little about relation of these approach to the Special Adjoint Functor Theorem, and I think it should work fine. The intuition is this: even if we need to find a monomorphism in this $\mathcal{U}$-set $S$ of distinct representative subobjects with a certain property and we find an object with said property which may not be its element, then we can "replace" it with an equivalent element $S$ which should still satisfy the same property due to the $\equiv$ relation. This is vague, but I think this is what happens in the proof of a Special Adjoint Functor Theorem.

However, I don't know much about well-powered categories and their uses in mathematics, so I need an advice from experts whether this approach leads to any trouble. In particular, I'd like to know if "my" definition of well-poweredness works well with theory of presentable and accessible categories (whose definitions also need to be adjusted if we use universes a-la the paper of Low: see here).

Answer 1

Borceux's Definition 4.1.1

An equivalence class of monomorphisms with codomain A is called a subobject of A.

in combination with Definition 4.1.2

A category A is well-powered when the subobjects of every object constitute a set.

and the subsequent claim that the category of sets is well-powered contradicts Axiom 1.1.7 in his book:

A class is a set if and only if it belongs to some (other) class.

A large category (meaning the collection of objects is a proper class) can have a proper equivalence class of subobjects, which cannot be an element of any set. So a contractible groupoid with a proper class of objects is not a well-powered category in this definition, even though it is equivalent to the terminal category, which is well-powered.

The problem arises from the fact that the definition of a quotient of classes using equivalence classes is only correct when each equivalence class is a set. Otherwise one must define quotients using universal properties.

Thus, this problem can be resolved by using a categorical definition of a quotient instead of a set-theoretical one:

A category C is well-powered if for any object A∈C there is a surjective map Sub(A)→Q such that two subobjects of A are mapped to the same element of Q if and only if they are isomorphic, and, additionally, Q is a set (or a U-small set, etc.).

(Categorically, we could also say that Q is the quotient of Sub(A) with respect to the equivalence relation of isomorphism, where the quotient is defined using a universal property as the initial object in the category of maps Sub(A)→Q that send isomorphic subobjects to equal elements, without any reference to equivalence classes.)

Then Scott's trick, as explained in Andrej Bauer's answer, shows that other (correct) definitions are equivalent to this one.

Answer 2

Your dilemma can be resolved by Scott's trick, if your universes are cumulative von Neumann universes. Briefly, given an equivalence relation $E \subseteq C \times C$ on a class $C$ and $x \in C$, consider the (possibly proper) class $[x]'_E = \{y \in C \mid x E y\}$. Let $\alpha$ be the least ordinal such that $[x]'_E$ intersects $V_\alpha$, the set of all sets of rank at most $\alpha$. Now re-adjust the definition of equivalence class by defining it to be $[x]_E = [x]'_E \cap V_\alpha$. This way $[x]_E$ is set-sized and we have not relied on choice (but we did rely on regularity). The quotient $C/E$ may be defined as the class of all the set-sized equivalence classes $[x]_E$, for $x \in C$.

However, from a category-theoretic perspective, relying too heavily on particularities of a set-theoretic foundation is not such a good idea. One should look for definitions that are natural from the point of view of category theory, and then see how they play out in various settings.

The natural notion of equality in category theory is equivalence. Thus for many purposes it suffices to relax the condition of well-poweredness to the following. Given a category $C$ and an object $X$ in $C$, let $\mathrm{Mono}_C(X)$ be the (possibly large) preorder of all monos into $X$, seen as a category. Say that $C$ is essentially well-powered when for every $X$ the preorder $\mathrm{Mono}_C(X)$ is equivalent to a small category (in which case it is in fact equivalent to a small poset).

We are in familiar category-theoretic territory here. Analogously to the difference between "there existing products" and "having chosen products", we may further require there to be "chosen well-poweredness" by requiring a mapping $\mathrm{Sub} : \mathrm{ob}(C) \to \mathrm{Poset}$ which assigns to each object $X$ a (small) poset $\mathrm{Sub}(X)$ together with an equivalence $\mathrm{Set}(X) \simeq \mathrm{Mono}_C(X)$. (If $C$ has pullbacks one should think about turning $\mathrm{Sub}$ into a contravariant functor equivalent to the pullback (pseudo)functor.)

Notions of smallness and largeness appear outside traditional set theory, for instance in type theory and algebraic set theory. So the above definitions are not limited to set theory. It is "just a technicality" to figure out how one might get $\mathrm{Sub}$ in this or that setting. Maybe Scott's trick will save the day, or having some (large) choice, or Univalence axiom. As a category theorist one would just be used to looking around to see what's available. If some setting thinks that groups are not well-powered, well, tough luck. But most set theories will be able to accommodate moderate wishes for well-poweredness. (An interesting exception would be constructive set theory CZF.)

Answer 3

One simple way is to read the traditional definitions (à la Grothendieck, etc) but replacing existence conditions with chosen structure:

• A category $C$ is $U$-locally-small if it is equipped with a $U$-valued map $h : C_0 \times C_0 \to U$ and isomorphisms $h(x,y) \cong C(x,y)$. (Equivalently, a $U$-valued functor naturally isomorphic to the original hom-functor.)

• A category $C$ is $U$-well-powered if it is equipped with a map $S : C_0 \to U$, and isomorphisms $S(x) \cong \mathrm{Sub}(x)$. (Equivalently, a $U$-valued functor naturally iso to the original shbobject functor.)

• Both of these can be recovered just by reading the traditional definitions, but with a “$U$-small set” take to mean a set equipped with an isomorphism to some chosen element of $U$.

These are a fairly minimal tweak to the traditional definitions to make them non-choicy. They are easily seen to respect equivalence of categories, and also equivalence of universes (suitably defined); in this way, they are considerably more robust than the Borceux-style definition and similar ones. While these definitions do involve a choice of extra structure, this structure is in each case unique up to canonical isomorphism. This approach works analogously completely off-the-shelf for every smallness condition I know.