Finite objects and automorphisms

Abstract

We show that every K-finite decidable object X of an elementary topos E is Dedekind-finite, i.e., that every monic endomorphism of X is an automorphism. As an easy corollary, every epic endomorphism of X is likewise an automorphism. The proof depends in part on an analysis of the finite cardinals of E and in part on the equivalence, in any Boolean tbpos, of Kfiniteness and Tarski-finiteness (Theorem 6). Here X is Tarski-finite iff every inhabited collection of arbitrary elements of ω ^X (subobjects of X ) contains a ¨—minimal element.