Could not include topos theory - contents
In category theory and specifically in topos theory, the notion of inhabited object in a general topos is a generalization of the notion of inhabited set from the archetypal topos Set. It is the semantics of an inhabited type in type theory.
An object $X$ in a topos $\mathcal{T}$ (or more generally, any regular category) is said to be internally inhabited if in the internal logic of the topos it is true that
This is equivalent to saying that the unique map $X \to 1$ is an epimorphism. In a topos this is equivalent to it being a regular epimorphism and this is the condition for inhabited in any regular category).
The term well-supported is also used for this notion (in general, the support of $X$ is the image of $X\to 1$).
In terms of (â,1)-category theory, inhabited means (-1)-connected.
On the other hand, $X$ is said to be externally or globally inhabited if there exists a morphism $1\to X$, i.e. a global element. Every globally inhabited object is internally inhabited, since every split epimorphism is a regular epimorphism. The converse is true if $1$ is projective, as is the case in a well-pointed topos (such as Set).
Some sources use â$X$ is inhabitedâ in the global sense, which is not expressible in the internal language. Others use the term âinhabitedâ only internally. Regardless, a pointed object always means one equipped with a global element $1\to X$, whether interpreted internally or externally.
For sheaf toposes with enough points, in which epimorphisms are stalkwise epimorphisms, an object is (internally) inhabited if the germ of $X$ over every stalk is an inhabited set.
One situation where this plays a role is in the study of certain smooth toposes with objects $\mathbb{I}$ of invertible infinitesimals . There is an immediate definition of such a topos, the topos called $\mathcal{Z}$ at Models for Smooth Infinitesimal Analysis, for which this object exists, but is not inhabited. Only the weaker internal statement $\not \not \exists x \in \mathbb{I}$ is true.
But for some useful constructions in these toposes, such as for giving an internal definition of distributions as genuine functions (internally), it is desirable to have $\mathbb{I}$ be inhabited. In the above situation this is achieved by forcing the existence of invertible infinitesimal elements. The result is the refined topos denoted $\mathcal{B}$ at Models for Smooth Infinitesimal Analysis.
While writing this page, we had the following discussion about whether or not â$X$ is inhabitedâ in a topos should be interpreted internally or externally, before deciding that we should mention both.
Mike: I strongly disagree that âinhabitedâ means âhas a global elementâ in a topos. Intuitionistically, â$X$ is inhabitedâ means âthere exists an $x\in X$â which when interpreted in the internal logic of a topos means that $X$ is well-supported. By contrast, the property of having a global element is not expressible in the internal language at all. âInhabitedâ is also universally used in the topos-theoretic literature to mean well-supported.
Toby: Then what is the term for what I have called âinhabitedâ? At least one reference uses the term that way; I see (through Google) that it's used in the Elephant, but it's not in the index and I haven't managed to tell what the definition is. Certainly I'm not in the position to make a good literature search.
Mike: On p618 of the Elephant he uses âinhabitedâ to mean âthere exists an $x\in X$â in the internal language. What do you think about the change I made above?
Toby: I certainly can't disagree with any of the statements there.
I would like us to be a bit bolder with the terminology if it's safe and useful (neither of which condition has been established, of course). The Elephant has its share of terminological changes (like âcartesian categoryâ and âcartesian morphismâ, which I remember got a lot of complaints on the categories mailing list), so I'd want to check its references (which I can do later).
The wiki saved a previous version of your comments; since you changed it, I won't hold you to it. But having read it does inspire me to say that the terminology that comes naturally to me is indeed âinhabitedâ for having a global element and âinternally inhabitedâ for being well supported; the latter seems at least as well justified as âinternal axiom of choiceâ (as used in, say, Mac Lane \& Moerdijk). That's just me, of course.
Mike: Yeah, I wasnât sure if it would (there seems to be a certain timeout within which multiple edits by the same person overwrite each other?). I also wasnât sure if it was kosher to remove/change my comment; perhaps I shouldnât have. The reason I changed it was that âinhabitedâ and âinternally inhabitedâ did start to make a little sense. My current feeling is that âinhabitedâ is a set-theoretic term, and as such should only be used in set-theoretic-like situations. This includes (1) constructive set theory, (2) IHOL and hence the internal language of a topos, and (3) a well-pointed topos. If we are talking about an arbitrary topos, and it is not clear that our statements are to be interpreted in the internal logic, I would rather use âhas a global elementâ and âis well-supportedâ since they are both unambiguous.
You are certainly right about the Elephant and terminology. âCartesian category,â âprone morphism,â and âeffective regular categoryâ are the ones that come to mind that seem to have been rejected by much of the categorical community.
Mike: Another thought: one could argue that just as a âringâ in a topos means a model of the theory of rings, and likewise for many other concepts, so should an âinhabited objectâ mean a model of the theory of inhabited objects, which is the same as a well-supported object. Of course this fails for âprojective object,â but I donât think there is a âtheory of projective objects,â at least not one interpetable in the usual internal logic of a topos. And I suppose maybe it fails for âchoice objectâ too, although that probably depends on whether you formulate the theory of choice objects to be equipped with a choice function or merely assert that one exists. Perhaps the literature is not very consistent in its use of âinternallyâ or lack thereof.
Toby: I see âinhabitedâ as just a convenient abbreviation of âthat has an elementâ (convenient enough that âis inhabitedâ is still nicer than âhas an elementâ). So an inhabited object should naturally be an object with an element (a global element, that is; every object has a generalised element, and we must at least reproduce the situation in $\Set$). And after all, âinhabitedâ is hardly more of a set-theoretic term than âaxiom of choiceâ! (^_^)
Maybe life would be simpler if we always internalised using the internal language, but there's a lot of precedent that we don't, probably because it's a lot easier not to. And anyway, that's what the word âinternalisedâ is for!
As for the timeout, I think that it's an hour, although I haven't timed it carefully. (It definitely exists.) I think that it's fine to remove or change old comments, certainly if they haven't been replied to, but one should be aware that they can still be read. (And if you're not sure if they can still be read, try âSee changesâ or âBack in timeâ below.)
Mike: Well, I think that I will continue using âhas a global elementâ myself for clarity, but youâve convinced me that itâs not entirely unreasonable to use âis inhabitedâ to mean the same thing. Though I reserve the right to reopen the discussion if we discover precendent to the contrary. (-:
A different question, as you mentioned earlier, is whether it is useful. How often do we want to talk about objects that have a global element? We may frequently care about pointed objects, which are equipped with a global element, but there isnât any dispute about what to call those.
Toby: You've got a good point there. Probably âpointed objectâ and âwell-supported objectâ are the only really useful notions. Actually, I think that a lot of constructivists (the ones that are really think that mathematics should talk about constructions, like Bishop and Coquand) would say that an inhabited set and a pointed set are really the same thing. We can distinguish them, of course, by their morphisms (or even isomorphisms), but that doesn't mean that we need two words (just as we don't use two different words for metric spaces with, say, continuous maps between them and uniformly continuous maps bewteen them). So as you move towards my position, I move towards yours âŠ.
Mike: Does that mean you might be satisfied with the way itâs written now? (I added a note about pointed objects.)
Toby: Yes, I'm happy now for now.