Do all toposes satisfy the internal Zorn's lemma?

Question

I came up with this question when trying to give a more detailed answer to a question by Tim Campion in a comment to Ingo Blechschmidt's answer to Examples of statements that are valid in every spatial topos.

There is an obvious internalized form of Zorn's lemma for toposes. Basically, you can use the Mitchell-Bénabou language to spell out the following:

given a poset $(P,\leqslant)$, consider the object of pairs $(C,u)$ where $C$ is a chain in $P$ and $u$ is an upper bound of $C$ in $P$. We say that the internal Zorn's lemma IZ holds if whenever the projection $(C,u)\mapsto C$ from this object to all chains of $P$ is epi, the object of maximal elements of $P$ is "as inhabited as $P$ itself", that is, has the same support as $P$.

If you do not care for a more rigorous formulation, skip everything until the questions.

Here is this more rigorous formulation. Given a poset $P$ in a topos $\mathscr S$, we can form the objects $\max(P)\rightarrowtail P$ of maximal elements of $P$ and $\operatorname{chains}(P)\rightarrowtail\Omega^P$ of chains of $P$. We can also form the object of upper-bounded-chains of $P$, call it, say, $\operatorname{ubc}(P)$: it is uniquely determined by saying that $\hom(X,\operatorname{ubc}(P))$ must be in one-to-one correspondence with pairs $(C,u)$, where $C\rightarrowtail X\times P$ is a subobject of $X\times P$ and $u:X\to P$ is a morphism, such that $C$ is a chain and $u$ is an upper bound of $C$, if one considers $u$ as an element of $X^*(P)$ and $C$ as a subobject of $X^*(P)$, in the slice topos $\mathscr S/X$.

Clearly there is a canonical projection $\pi:\operatorname{ubc}(P)\to\operatorname{chains}(P)$, given by sending $(C,u)$ to $C$.

We can then formulate the internal version IZ of the Zorn lemma as follows:

If $\pi:\operatorname{ubc}(P)\to\operatorname{chains}(P)$ is epi, then $\max(P)$ has the same support as $P$; that is, the image of $\max(P)\to1$ is the same as the image of $P\to1$ (where $1$ is the terminal object of $\mathscr S$).

Minimal question: do all toposes satisfy this?

I suspect that, arguing internally, one might deduce from IZ internal choice IC which in turn implies booleannes, but somehow I don't see how to actually do it.

Extended question (again in case the answer to the minimal question is negative): there might be more sophisticated internalizations of the Zorn's lemma. For example, one can consider, for an object $P$, the object $\operatorname{Orders}(P)$ of partial orders on $P$ and then internalize the statement "partial orders with all chains upper-bounded are included in partial orders having a maximal element". Is there a form which would be weaker, in the sense that it holds for some topos which does not satisfy IZ?

Here is a version about which I would like to ask specifically. This actually corresponds on the "classical" side to the variant of the Zorn's lemma with requiring upper bounds for nonempty chains only.

Call an internal poset $(P,\leqslant)$ internally inductive if for any object $X$ and any $C\rightarrowtail X\times P$ which is a chain of $X^*(P)$ in $\mathscr S/X$, the object $U_C\rightarrowtail X^*(P)$ of upper bounds of $C$ has support no less than $C$. That is, the image of the composite $U_C\rightarrowtail X\times P\to X$ contains the image of $C\rightarrowtail X\times P\to X$, where $X\times P\to X$ is the projection.

We then say that IIZ holds in $\mathscr S$ if for every internally inductive poset $P$, the object $\max(P)$ has the same support as $P$, as above.

And the specific instance of my Extended question is,

Which toposes satisfy IIZ? How does it compare to IZ?

Important correction

As Gro-Tsen points out in a comment, this does not make much sense unless I restrict to Grothendieck toposes with Axiom of Choice holding in my set theory. Slightly more generally, one may consider toposes bounded over a topos with AC. Maybe still more generality is possible, but let us stick to this for definiteness.

Answer 1

Assuming the law of excluded middle internally your formulation of Zorn's lemma is equivalent to the axiom of choice by the usual argument. Now there are Boolean Grothendieck topos in which the axiom of choice fails. Hence they don't satisfies Zorn lemma either.

I think the simplest example of this is to take $G$ to be a non-discrete but pro-discrete localic/topological group (typically $G = \mathbb{Z}_p$ the group of p-addic integer) and consider $\mathcal{T}$ the topos of sets endowed with a continuous (hence smooth) action of $G$ (that is the stabilizer of each point is an open subgroup)

Assuming LEM in the base, $\mathcal{T}$ is clearly boolean (sub-object are $G$-stable subsets and set theoretic complement preserve subobject).

But $\mathcal{T}$ doesn't satisfies either internal nor external choice. For exemple for $G = \mathbb{Z}_p$ the infinite product of all the $\mathbb{Z}/p^k\mathbb{Z}$ with their canonical action is the initial object. (more generally, the product of the $G/U$ for $U$ in a fundamental system of open subgroup is empty unless $G$ is discrete).

Edit: However it should be noted that, assuming Zorn lemma in the base topos, an appropriate version of Zorn lemma is known to holds in every Localic Grothendieck topos (but the topos mentioned above is not localic of course). This is proved as Proposition D4.5.14 in Sketches of an elephant.

More precisely, one take the Zorn lemma to be the statement: "every inductie poset has a maximal element" but where "inductive" is defined as the internal statement "every chain as an upper bound". More precisely prop D4.5.14 shows that if P is an (internally) inductive poset in a localic topos, then it has an (internally) maximal element given by a global section. In particular, it proves the internal statement "there exists a maximal element" is valid.

One also have the stronger version of the internal Zorn Lemma where the quantification over "all inductive poset" is interpreted internally using the Stack semantics, because every slice of a localic topos is localic, and we can apply D4.5.14 in each slice.

The paper by Bell linked in Peter Lumsdain comment, also prove a similar result but for an (at least in appearance) weaker version of Zorn lemma where "inductive" is taken as "every chain has a least upper bound" instead of an upper-bound. Bell explicitly says that he doesn't know how to prove the stronger version of Zorn lemma, but looking at the proof of D4.5.14 it seems to me that the whole point is that both version of Zorn lemma are constructively equivalent: given any poset the poset of chains ordered by inclusion is inductive in Bell's stronger sense, so assuming Bell's version of ZL one get a maximal chain in every poset and an upper bound for a maximal chain has to be a maximal element.