Repository navigation
Should we relax the definition of a subobject classifier? #370
Description
The definition of a subobject classifier apparently makes sense in any category with a terminal object. But the nLab and lots of other sources also assume that finite limits exist; which is why it is assumed in CatDat. Do we want to remove this assumption, and only assume that a terminal object exists? Then we can investigate this property in a more fine-grained way. Namely, the property is currently refuted automatically for every category that does not have finite limits, and I suspect that for some of these categories it will be interesting to find out if they have a subobject classifier with the relaxed definition.
Of course, without finite limits, we cannot phrase the definition in terms of a representable functor Sub : Cop → Set+, since the definition of this functor requires pullbacks. But I do not think that this is a huge problem. In any case, if we want to recover anything that is now in the database, we can speak of "finite limits + subobject classifier".
Actually, I can think of a definition that not even requires a terminal object. After all, it is just a universal monomorphism. But I don't think that this behaves well. Maybe one can also prove that the domain of
@varkor @dschepler @ykawase5048
Similar issues:
- On the definition of "exact filtered colimits" #300
- Preadditive categories are not assumed to be locally small #359
- [not an issue yet] Should we remove "finite limits" from the Malcev property? Without finite limits, it is a bit inconvenient to talk about congruences, but it is possible, and this is also why the properties "effective congruences" and "quotients of congruences" in CatDat do not assume that finite limits exist.
MO discussion about subobject classifiers in categories that are not finitely complete:
Tom Leinster does define subobject classifiers in any category here:
Activity
varkor commentedon Sep 13, 2026
I don't see a reason not to relax the definition. I think it would be reasonable even to drop the existence of a terminal object, as you suggest (though I don't know if I have an example at this level of generality off the top of my head).
dschepler commentedon Sep 14, 2026
So, would this be relaxing just to requiring that pullbacks exist when one of the morphisms is monic? Or more generally, just to requiring that every monomorphism is a pullback of the universal monomorphism$\Omega_0 \hookrightarrow \Omega$ via a unique morphism?
If the latter, then that potentially becomes a bit less useful. In categorical logic, I'm used to seeing a subobject of the test object$U$ being treated as a generalized truth value, and the idea of a subobject classifier is that you can dispense with propositions being an entirely different sort from normal types, and just treat generalized truth values as generalized elements of a first-class type known as $\Omega$ . But if you don't know that all pullbacks of the universal monomorphism exist, then you only know that some subset of $Hom(T, \Omega)$ corresponds to the generalized truth values. (And if all pullbacks of the universal monomorphism do exist, then arbitrary pullbacks easily exist as long as one of the morphisms is monic: take the characteristic morphism of the monic, compose with the other morphism, and then take the pullback of the universal morphism by that composition.)
As far as the question about terminal objects: It's a fairly standard fact that if$\Omega_0 \hookrightarrow \Omega$ is a universal monomorphism of a category, then $\Omega_0$ is automatically a terminal object anyway. So while it does absolutely make sense to formulate the definition in terms of $\Omega_0 \hookrightarrow \Omega$ (and I've certainly seen some sources do that and then quickly replace $\Omega_0$ with $1$ using that observation), it wouldn't really make much difference to the database in the end -- just a question of whether implication of a terminal object is part of the definition, or whether it's an implication with a not very long proof.
vladsotirov commentedon Sep 22, 2026
Two proposals.
First proposal: the current definition of subobject classifier should be changed to regular subobject classifier + mono-regular. Then this discussion of dropping limit conditions should be about doing so for what is currently regular subobject classifier. Such a change would be a minimally disruptive, would make the relationship between topoi and quasitopoi clearer. The downside is perpetuating the notion of a regular subobject classifier as if there is a difference between it and a subobject classifier.
Second proposal (to be applied after the first): in the definition of regular subobject classifier, change "if it has finite limits and a regular monomorphism* ⊤:1↪Ω" to "if it has a morphism ⊤:1↪Ω along which all pullbacks exist..." Then rename "regular subobject classifier" to "subobject classifier" and add a note that in the topos theory literature subobject classifier means subobject classifier + mono-regular in CatDat.
Explanation:
The most general definition of a subobject classifier would be a monomorphism, 1) along which all pullbacks exists, 2) with the property that each of the subobject classifier's pullbacks (i.e. morphisms classified by it) is a pullback of the classifer along a unique morphism (which we may as well call the characteristic morphism of the pullback). These are equivalent to a) the codomain represents a contravariant functor corresponding to a pullback-stable class of monomorphisms considered as a fibration (or however you want to phrase it), and imply b) that the domain is a subterminal object.
But this seems too general to be useful as a property. For example, the unique morphism from a strict initial object to a terminal object is such a subobject classifier, as is the unique morphism from a terminal object to itself.
The following are equivalent for a such a subobject classifier: a) its domain is not just a subterminal object, but a terminal object, and b) all identity morphsms are classified by it. Both conditions imply the subobject classifier is is a split monomorphism and that all monomorphsms classified by it are regular monomorphisms.
This suggests exactly one notion of a subobject classifier that could serve as a useful property: that from the Second proposal above.
ScriptRaccoon commentedon Sep 22, 2026
Thank you for the comments!
@varkor Indeed, after creating the issue I found a preprint by Tom Leinster that includes the definition in a general category (now linked above).
@dschepler Requiring the existence of pullbacks along monomorphisms is a good idea, which sits in between the current assumption that all finite limits exist and the idea to remove all such assumptions. It is also perhaps worth adding as a separate property.
But actually, my idea was to just requiring that there is a monomorphism$1 \hookrightarrow \Omega$ (where $1$ is some object that later turns out to be terminal) such that for every monomorphism $U \hookrightarrow X$ there is a unique pullback square.
It can also be formulated as a terminal object in the category of monomorphisms and pullback squares as morphisms. This is also what Tom Leinster writes in the linked preprint.
But I agree that, since that does not immediately give a description of$Hom(-,\Omega)$ (when pullbacks of monos do not exist), the term "subobject classifier" is misleading. What about adding this as a separate property, called "has a universal monomorphism"? Maybe subobject classifier can then be defined or characterized as "has pullbacks along monomorphisms" + "has a universal monomorphism"?
What you write then is all relevant, but it remains as long as we work in a category with finite limits that has a subobject classifier. It is just a shift of notation.
It is weird to have an implication like this one that says
because grammatically that sentence reads like: if an object with nice properties exists, then all finite limits exist (which is absurd).
@vladsotirov I don't think it's a good idea to change the definition in a such drastic way. It will be confusing for most readers. CatDat wants to be close to existing mathematical literature. Of course, this issue already suggests to deviate from it a little bit, but not by completely exchanging terms, but rather to relax some assumption.
vladsotirov commentedon Sep 23, 2026
@ScriptRaccoon You have already deviated from existing mathematical literature by introducing the property of a regular subobject classifier after my answer on MSE showing those suffice to define quasitopoi. If you were following the literature more closely you would have two other variations instead: extremal subobject classifier (28.11(1) in Joy of Cats, also called a weak subobject classifier in A2.6 in the Elephant) and strong subobject classifier (in nLab and in all but name in 12.4 of Wyler's Quasitopoi).
So the situation is that CatDat has adopted a fourth previously unknown kind of subobject classifier to support a non-standard definition of a quasitopos, thereby increasing the confusion, not decreasing it.
Moreover, the confusion was originally introduced by topos theorists who decided to bake what CatDat calls being mono-regular into the definition of a subobject classifier (if they hadn't, prehaps there would be a standard term for mono-regular). In other words, I find the implication subobject classifier ===> mono-reguar just as absurd as you find the implication subobject classifier ===> finitely complete.
I stand by my first proposal that subobject classifier should be defined as regular subobject classifier + mono-regular, and that the existence of finite limits in the definition of regular subobject classifier should simply be dropped (or made to match whatever relaxation of the definition of subobject classifier is decided here; if not all are dropped, then I think only "has pullbacks along regular monomorphisms" should remain). My second proposal was separate from the first precisely because it is more drastic and contradicts the literature. But the first proposal only serves to clarify the confusion already present in CatDat (and the literature).
Regarding a property of "has universal monomorphisms", the following thought.
Following Leinster, define (for the sake of this discussion) a "morphism classifier" to be a subterminal object in the category of morphisms and pullback-squares between them (i.e. by the property that every pullback of a "morphism classifier" that exists is the pullback of it along a unique morphism).
Such a "morphism classifier" is a then monomorphism, if and only if its domain is a subterminal object. In that case, the objects with a morphism to the subterminal object are the domains of monomorphisms, equivalently identity morphisms, classified by the monomorphism classifier. As a consequence, requiring that every monomorphism be classified, as I think the proposed "univeral monomorphism" definition does, again smuggles in mono-regularity, repeating toposophy's original sin. So you gain nothing over my proposal to simply drop the finite limit conditions from the current definition of regular subobject classifier. If not all limit conditions are to be dropped, then as I said earlier, the remaining condition should be "has pullbacks along regular monomorphisms".
ScriptRaccoon commentedon Sep 23, 2026
@vladsotirov My comment "I don't think it's a good idea to change the definition in a such drastic way" refers to your second proposal. Sorry for the confusion. That's for now – I will need more time to read and understand your comment.