A finite object in a category is a generalisation of the notion of finite set in the category of sets.
As there are already at least five distinct notions of finite set in constructive mathematics, so there must be at least five distinct notions of finite object internal to a topos. Additionally, the definitions may also be interpreted in an ‘external’ sense, giving even further notions. Only some are mentioned below.
The external version of a “finite set” in the strictest sense is usually called a finite cardinal. This is an object which is the pullback of along some global element . Here is a natural numbers object and is its strict order relation. We can then consider subobjects, quotient objects, and subquotient objects of finite cardinals to obtain external versions of subfinite, finitely indexed, and subfinitely indexed sets.
The full subcategory of finite cardinals in any topos is again a topos, and it is Boolean. Its subobject classifier is , which in the ambient topos is the classifier only of decidable subobjects. This means that classically valid arguments, including all of finitary combinatorics, can generally be applied easily to finite cardinals, as long as we always interpret “subset” to mean “decidable subset.”
The internal version of a “finite set” is an object such that ” is a finite cardinal” is true in the internal logic. This is equivalent to saying that is locally isomorphic to a finite cardinal, i.e. there is an epimorphism and a generalized element such that over . Equivalently, there is a such that is a finite cardinal in the slice topos .
Likewise, the internal version of “finitely indexed set” is one which is locally a quotient of a finite cardinal, and so on. An “internally finitely indexed” object is generally called a -finite object, and an “internally subfinitely indexed” one is called a -finite object. Since it is still provable in the internal logic that any decidable finitely indexed set is finite, the “internally finite” objects can be characterized as the decidable -finite objects.
The decidable -finite objects in any topos also form a Boolean topos whose subobject classifier is ; it can be regarded as the “stack completion” of the topos of finite cardinals. The category of -finite objects is a topos if and only if every -finite object is decidable, and the category of -finite objects is a topos if (but not only if) the subobject classifier is -finite.
In any Boolean topos, all four internal notions coincide. In a well-pointed topos, each internal notion coincides with its external notion. Therefore, in a well-pointed Boolean topos, including the topos Set as usually conceived, all notions of finiteness coincide.
In a presheaf topos , the finite cardinals are the finite-set-valued functors which are constant on each connected component. In particular, if is a group, then the topos of finite cardinals is equivalent to FinSet.
Likewise, in the Grothendieck topos of sheaves on a space , the finite cardinals are the locally constant functions . So if is connected, the topos of finite cardinals in is also equivalent to .
Examples of such are tiny objects and infinitesimal objects in sheaf toposes.
By contrast, the -finite objects in are the finite-set-valued functors each of whose transition functions is surjective, and the decidable K-finite objects are the finite-set-valued functors each of whose transition functions is bijective.
In particular, if is a groupoid, the topos of decidable -finite objects is equivalent to . Since the topos of presheaves on a groupoid is Boolean, this gives an example of a Boolean topos in which the finite cardinals (“externally finite objects”) and the (decidable) -finite objects (“internally finite objects”) fail to coincide.
In , the decidable K-finite objects are those that are “locally finite;” i.e. there is an open cover of such that over each open in the cover, the sheaf is a locally constant function to . These are essentially the same as covering spaces of .
Toby: I think that I'll move the internal stuff to finite object, to keep each page relatively short.
By the way, do I understand you correctly that ‘finite object’ in topos theory by default means ‘decidable K-finite object’?
Mike: Okay (to the move). To the question, I’m realizing more and more that I don’t really have the background to be able to say what “topos theorists” say. My only source for this material is the Elephant (and what I’ve been able to deduce on my own, which of course tells us nothing about terminology). The Elephant never says “finite object” unqualified; only “finite cardinal” or “K-finite object” or “decidable K-finite object” or ”-finite object.” If “projective” means “externally projective,” and likewise for “choice” and (maybe) “inhabited,” then “finite object” should mean “finite cardinal,” but I wouldn’t use it that way myself out of fear of ambiguity and since “finite cardinal” means the same thing. I don’t see any objection to “internally finite object” meaning “decidable K-finite object,” though.