Should we relax the definition of a subobject classifier?

[ScriptRaccoon]

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 : C^op → 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 $\top$ must be a terminal object anyway (this is well-known when finite limits exist). Not sure, though. Maybe we should strive for the correct generalization right away.

@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:

• https://mathoverflow.net/questions/55955

Tom Leinster does define subobject classifiers in any category here:

• https://arxiv.org/pdf/1012.5647

[varkor]

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]

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.