Is that true that each non-initial object has elements under this definition of ETCS

category-theorytopos-theory

It seems to me that the axioms for ETCS on Lawvere's paper:
http://www.tac.mta.ca/tac/reprints/articles/11/tr11.pdf

and on nlab:

https://ncatlab.org/nlab/show/ETCS

are not such the same.

My confusion is that axiom 6 in the first link states that each non-zero object has elements, whereas the nlab page says the axioms of ETCS is summarized as:

The axioms of ETCS can be summed up in one sentence as:

Definition 2.1. The category of sets is the topos which is a well-pointed topos, has a natural numbers object, and satisfies the axiom of choice.

How does Definition 2.1 imply that every non-zero object has an element? By considering Set$\times$Set, it is obviously not true that every non-zero object in a topos has maps from the terminal object to it.

Best Answer

The definitions are equivalent. Here is the first argument I could come up with. There may well be a simpler one using the full power of the topos assumption; the below works in any well-pointed category with a strict initial object in which every epimorphism is effective.

In a well-pointed topos, if an object $X$ has no points, then we know that $X$ has at most one morphism to any object $Y$. In other words, the unique morphism $q:0\to X$ from the initial object is an epimorphism. The dual property, of $X$ being subterminal, is widely used, but I'm not sure this one has a standard name. "Quot-initial"?

Anyway, in any topos, every epimorphism is effective. The linked nLab article cites Mac Lane-Moerdijk, IV.7.8, for this result. Thus $q$ is the quotient map for some equivalence relation $R\rightarrowtail 0\times 0$ on the initial object $0$. But since toposes have strict initial objects, we find both $0\times 0\cong 0$ and (thus) $R\cong 0$. That is, there is a unique equivalence relation on $0$ and thus $q$ is isomorphic to the identity map in the slice category under $0$.

Related Question