Are all unions in a topos with complete subobject lattices secretly colimits? On a logical analogue of the AB5 axiom

Question

To clarify, here “topos” always means an elementary topos; I do not assume sheaves on a site, where I already knew my question to have a positive answer.

It is known but not so immediate from the axioms of a topos that if $X$ is an object and $A,B$ two subobjects, then their union exists and equals the pushout of $A\leftarrow A\cap B\rightarrow B$. I've recently had cause to wonder if this is true for general unions. Assume your topos satisfies that all objects $X$, the subobject lattice of $X$ is complete (there could well be an internalisation of this w.r.t the subobject classifier, I'm not sure). Must it follow that if $(A_i)_{i\in I}$ is a set of subobjects of $X$ then the union $\bigcup_{i\in I}A_i$ is the colimit of the diagram on all spans $A_i\leftarrow A_i\cap A_j\rightarrow A_j$?

It's worth noting the dual statement is true; the intersection, if it exists, $\bigcap_i A_i$ is necessarily a true limit (even if a priori that limit might not exist either!), the wide pullback of all $A_i\hookrightarrow X$. I proved this by using the image factorisation theorem. However there is no suitable dual to the image factorisation theorem that I know which can give me what I want for the colimits.

This came up when reading Mac Lane and Moerdijk's proof of proposition $6.1.8$, that:

If a Boolean topos with complete subobject lattices is generated by the open objects, it satisfies the axiom of choice.

Taking a few things on faith, this seems to give the fun corollary, that a localic topos is Boolean iff. it satisfies the internal choice axiom iff. it satisfies the external choice axiom.

Everything is fine except for the very first step, where Zorn's lemma is invoked. Given an epimorphism $X\twoheadrightarrow Y$ we are to use Zorn to conclude there is a maximal subobject $M$ of $Y$ which admits a section $M\hookrightarrow X$ of the above epimorphism; this is almost obvious except for the part where we must doubt ! our usual intuition that, if $(M_\alpha)_{\alpha\in\lambda}$ ($\lambda$ an ordinal) is some chain, we can define maps $\bigcup_\alpha M_\alpha\to X$ just by giving maps on each of the $M_\alpha$; we also, to find the resultant map(s) are sections, like to say they are uniquely determined by their values on each $M_\alpha$. That is, we would like to express the union as a colimit. Without that, I think their proof is flawed; maybe it follows always, but I am really not sure. It is plausible this was overlooked by the authors, especially since what we want is true in their intended use case (corollary $6.1.9$).

I know we could use the two-sided adjointness of the pullback functor (on the subobject lattices) to say, ok, the preimage of $M\subset Y$ would be the union of all preimages of the $M_\alpha$, which by existence of a section are really just the subobjects $M_\alpha\hookrightarrow X$. Ok... but their union in $X$ really not yield an object isomorphic with the union of the $M_\alpha$ along different arrows, in $Y$.

Any ideas? This kind of annoyance comes up with some homological algebra and spectral sequence concerns specifically; really, I want Grothendieck's AB5 axiom (and indeed what I want is true in any sheaf topos).

Answer 1

Yes, in a topos with complete subobject lattices, the union of a family $(A_i)_{i:I}$ of subobjects of $X$ indexed by a small set $I$ is the colimit of the diagram $A_i \cap A_j \rightrightarrows A_i$.

To see this, we may assume that $\bigcup_{i:I} A_i = X$. Suppose we have morphisms $f_i : A_i \to Y$ such that $f_i |_{A_i \cap A_j} = f_j |_{A_i \cap A_j}$. Then we consider the subobjects $\Gamma_i$ of $X \times Y$ given by the monomorphisms $(\operatorname{inc}_{A_i}, f_i)$, and let $\Gamma := \bigcup_{i:I} \Gamma_i$. We then claim that $\pi_1 \circ \operatorname{inc} : \Gamma \to X$ is an isomorphism.

To see this, first the image of $\Gamma_i$ contains $A_i$, so $\pi_1 \circ \operatorname{inc}$ must be an epimorphism. To see it is a monomorphism, we will consider the subobject $\{ (x, y) : \Gamma \times \Gamma \mid (\pi_1 \circ \operatorname{inc})(x) = (\pi_1 \circ \operatorname{inc})(y) \rightarrow x = y \}$, which we want to show is all of $\Gamma \times \Gamma$. Now, since $B \times {-} : \operatorname{Sub}(X) \to \operatorname{Sub}(Y\times X)$ has a right adjoint $\forall_B$ for $B$ a subobject of $Y$, we have the $I$-indexed distributive law $B \times \bigcup_{i:I} \Gamma_i = \bigcup_{i:I} (B \times \Gamma_i)$ as subobjects. Applying this twice, we see $\Gamma \times \Gamma = \bigcup_{i,j:I} (\Gamma_i \times \Gamma_j)$. Therefore, it suffices to show that each $\Gamma_i \times \Gamma_j$ is contained in $\{ (x, y) : \Gamma\times \Gamma \mid (\pi_1 \circ \operatorname{inc})(x) = (\pi_1 \circ \operatorname{inc})(y) \rightarrow x = y \}$. But from here, it is a simple application of the Kripke-Joyal semantics to show that this follows from the assumption $f_i |_{A_i \cap A_j} = f_j |_{A_i \cap A_j}$.

Now, $f := (\pi_2 \circ \operatorname{inc}) \circ (\pi_1 \circ \operatorname{inc})^{-1}$ will be a morphism $X \to Y$ in the required cocone of the diagram $A_i \cap A_j \rightrightarrows A_i$. The uniqueness of the morphism is easy to show.