Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Sheaves in Geometry and Logic

Soichiro Fujii (May 28 2020 at 08:54):

Hi, I have a question on Proposition VI.1.8 of SGL; I cannot follow the proof.

The proposition says that if $\mathcal{E}$ is an (elementary) topos such that all subterminal objects in it form a generating/separating family, and such that each subobject lattice $\mathrm{Sub}_\mathcal{E}(E)$ is a complete Boolean algebra, then $\mathcal{E}$ satisfies the axiom of choice (i.e., every epimorphism in $\mathcal{E}$ splits).

The proof in SGL first takes an arbitrary epimorphism $p\colon X\twoheadrightarrow I$, and tries to find its section. To do so, the authors consider the poset $\mathcal{S}\subseteq \mathrm{Sub}_\mathcal{E}(I)$ of all subobjects $m\colon M\rightarrowtail I$ of $I$ such that there exists a “partial section” on it, i.e., $s\colon M\rightarrowtail X$ such that $ps=m$. Then they claim that $\mathcal{S}$ has a maximal element, using completeness of $\mathrm{Sub}_\mathcal{E}(I)$ and (meta) Zorn’s lemma... But is it clear that every chain has an upper bound in $\mathcal{S}$? I think to do so one should consider the poset of partial sections, rather than the poset of domains of partial sections.

The poset of partial sections amounts to $\mathcal{T}\subseteq \mathrm{Sub}_\mathcal{E}(X)$ consisting of all $s\colon M\rightarrowtail X$ such that $ps\colon M\to I$ is a monomorphism. Now consider a chain $(s_j\colon M_j\rightarrowtail X)_{j\in J}$ in $\mathcal{T}$. We can certainly take its union $s\colon M\rightarrowtail X$ in $\mathrm{Sub}_\mathcal{E}(X)$. Then the question is: is it true that $ps$ is mono, provided that each $ps_j$ is?

The rest of the proof looks fine to me.

Paolo Capriotti (May 28 2020 at 10:19):

Soichiro Fujii said:

The poset of partial sections amounts to $\mathcal{T}\subseteq \mathrm{Sub}_\mathcal{E}(X)$ consisting of all $s\colon M\rightarrowtail X$ such that $ps\colon M\to I$ is a monomorphism. Now consider a chain $(s_j\colon M_j\rightarrowtail X)_{j\in J}$ in $\mathcal{T}$. We can certainly take its union $s\colon M\rightarrowtail X$ in $\mathrm{Sub}_\mathcal{E}(X)$. Then the question is: is it true that $ps$ is mono, provided that each $ps_j$ is?

Yes. The union of a chain is a filtered colimit, and since filtered colimits preserve monomorphisms, $s$ is also the colimit of $s_j$ in $\mathcal{E}/X$. Now, composing with $p$ preserves all colimits (it is left adjoint to pullback), hence $ps$ is the colimit of $p s_j$ in $\mathcal{E}/I$, and so it is a monomorphism.

However, I find it slightly more intuitive to just take the union $t: M \to I$ of the chain $p s_j$ directly. Then by the same argument this is a colimit in $\mathcal{E}/I$ as well, which means you can lift it to a map $s: M \to X$ such that $ps = t$.

Morgan Rogers (he/him) (May 28 2020 at 10:57):

Seeing non-constructive results in a text about topos theory is a little bit painful...

Soichiro Fujii (May 28 2020 at 11:07):

@Paolo Capriotti
Thank you very much! Your explanation clarified the situation greatly.

However, if I understand correctly, your argument presupposes that $\mathcal{E}$ has filtered colimits...? Of course the union of a chain in $\mathrm{Sub}_\mathcal{E}(X)$ is a filtered colimit in $\mathrm{Sub}_\mathcal{E}(X)$, and (as you pointed out) it is necessarily given by a filtered colimit in $\mathcal{E}$ if $\mathcal{E}$ has that filtered colimit, but does it still hold even without the a priori assumption that the filtered colimit exists in $\mathcal{E}$?

Anyway, at least the immediate application of the proposition seems to be one in a Grothendieck topos, so I am satisfied for now!

Soichiro Fujii (May 28 2020 at 11:16):

@Morgan Rogers
Incidentally, the previous Proposition VI.1.7 of SGL says that a well-pointed topos is two-valued and Boolean, and is shown by a proof by contradiction...

Morgan Rogers (he/him) (May 28 2020 at 11:29):

Oof... And what a silly definition of well-pointedness too :grimacing:

Soichiro Fujii (May 28 2020 at 11:47):

@Morgan Rogers
Oh, is there any problem with the definition of well-pointedness in SGL?

Morgan Rogers (he/him) (May 28 2020 at 13:12):

Turns out I was confusing it with some other concepts (eg inhabitedness); it does match the definition of well-pointed category. But I still resent its inclusion, for the simple lack of examples; the only ones that present themselves are "inclusions of smaller universes of sets into larger ones"; that's certainly the closest thing to an example that one could get out of SGL.

Morgan Rogers (he/him) (May 28 2020 at 13:15):

What really bugs me is the fact that this result comes in a section about the axiom of choice, which is presented in both external and internal versions, but the internal version of well-pointedness isn't mentioned. :shrug:

Morgan Rogers (he/him) (May 28 2020 at 13:16):

Soichiro Fujii said:

Paolo Capriotti
However, if I understand correctly, your argument presupposes that $\mathcal{E}$ has filtered colimits...? Of course the union of a chain in $\mathrm{Sub}_\mathcal{E}(X)$ is a filtered colimit in $\mathrm{Sub}_\mathcal{E}(X)$, and (as you pointed out) it is necessarily given by a filtered colimit in $\mathcal{E}$ if $\mathcal{E}$ has that filtered colimit, but does it still hold even without the a priori assumption that the filtered colimit exists in $\mathcal{E}$?

Anyway, getting back to your question, Proposition 8 explicitly assumes completeness of Sub(E), circumventing the worry about whether E has filtered colimits.

Soichiro Fujii (May 28 2020 at 13:49):

Morgan Rogers said:

Anyway, getting back to your question, Proposition 8 explicitly assumes completeness of Sub(E), circumventing the worry about whether E has filtered colimits.

Yes, but my concern was whether the filtered colimits of chains in $\mathrm{Sub}_\mathcal{E}(X)$ are necessarily given by the filtered colimits in $\mathcal{E}$. Because I think the argument is like:

• Take any chain $(s_j\colon M_j\rightarrowtail X)_{j\in J}$ in $\mathcal{T}$.
• Take the colimit $M=\mathrm{colim}_{j\in J}M_j$ in $\mathcal{E}$; then the morphism $s\colon M\to X$ induced by $s_j$ is again a mono (*), so $s\in\mathrm{Sub}_\mathcal{E}(X)$.
• Similarly, the morphism $ps\colon M\to I$ induced by $ps_j$ is again a mono, so $s\in\mathcal{T}$.

And to prove the third step, we use that $M=\mathrm{colim}_{j\in J}M_j$ in $\mathcal{E}$.

(*) To be honest, I am not completely sure if (existing) filtered colimits preserve monos in any topos. I know that in a Grothendieck topos, filtered colimits exist and commute with finite limits, and hence preserve monos. Does the argument extend so that in any (elementary) topos, (existing) filtered colimits commute with finite limits?

Reid Barton (May 28 2020 at 14:19):

Since here the targets of your monos are all the same ($X$), I think it follows from the fact that $\mathcal{E}/X$ is cartesian closed.

Soichiro Fujii (May 28 2020 at 23:44):

Reid Barton said:

Since here the targets of your monos are all the same ($X$), I think it follows from the fact that $\mathcal{E}/X$ is cartesian closed.

Sorry, what does “it” refer to?

Reid Barton (May 29 2020 at 00:03):

That the colimit $M \to X$ of a filtered diagram of monos $M_j \to X$ is again a mono.

Soichiro Fujii (May 29 2020 at 00:31):

Reid Barton said:

That the colimit $M \to X$ of a filtered diagram of monos $M_j \to X$ is again a mono.

Hmm, maybe it is an easy thing, but I still cannot see why... Do you mean filtered colimits of subterminal objects in a cartesian closed category are always subterminal?

Paolo Capriotti (May 29 2020 at 09:16):

Soichiro Fujii said:

However, if I understand correctly, your argument presupposes that $\mathcal{E}$ has filtered colimits...? Of course the union of a chain in $\mathrm{Sub}_\mathcal{E}(X)$ is a filtered colimit in $\mathrm{Sub}_\mathcal{E}(X)$, and (as you pointed out) it is necessarily given by a filtered colimit in $\mathcal{E}$ if $\mathcal{E}$ has that filtered colimit, but does it still hold even without the a priori assumption that the filtered colimit exists in $\mathcal{E}$?

Good point, I did assume that $\mathcal E$ had filtered colimits. The missing part is that filtered colimits in $\mathrm{Sub}(X)$ are also colimits in $\mathcal{E}/X$. Here is a direct proof, although I suspect there are more elegant ways. Let $M$ be the filtered colimit of $M_i$ in $\mathrm{Sub}(X)$. It is enough to prove that $M$ is the colimit of $M_i$ in $\mathcal E$. So let $g_i: M_i \to Y$ be a cocone. Our goal is to find an extension $M \to Y$ (uniqueness will follow easily by taking an equaliser). Let $S_i$ be the "graph" of $g_i$, i.e. the subobject of $M_i \times Y$ corresponding to the morphism $g_i': M_i \to Y \to PY$ through the power object adjunction. Since $M_i \times Y \to X \times Y$ is mono, $S_i$ can be regarded as a suboject of $X \times Y$. Take the union $S$ of those subobjects. The key fact, which uses filteredness, is that the pullback of $S$ to $M_i \times Y$ is $S_i$. Therefore, if $g': X \to PY$ is the morphism corresponding to $S$, we get that $g'$ restricts to $g_i'$ for all $i$. Define $g: X_1 \to Y$ by pulling back $g'$ along $Y \to PY$. Now $X_1 \to X$ is a monomorphism, so we get a map $M \to X_1$, and composing with $g$ gives the sought extension.

Reid Barton (May 29 2020 at 10:53):

The argument I had in mind is the following. Suppose $M$ is the filtered colimit of subterminal objects $(M_j)_{j \in J}$; we want to show that $M$ is subterminal. It suffices to show that the projections $M \times M \to M$ are isomorphisms. Now because the category is cartesian closed, we can express $M \times M$ as the colimit over $(j, j') \in J \times J$ of $M_j \times M_{j'}$. Because $J$ is filtered, we can replace $J \times J$ with the cofinal diagonal subcategory $J$, so $M \times M$ is the colimit of $M_j \times M_j$. Since each $M_j$ was subterminal, this is just the colimit of $M_j$, which is indeed $M$.

Reid Barton (May 29 2020 at 10:55):

It's the usual argument that a functor that preserves pullbacks preserves monomorphisms (test a map for being a monomorphism by pulling it back along itself), but with weaker hypotheses because, in the original formulation, the target object $X$ is constant.

Soichiro Fujii (May 29 2020 at 11:08):

@Paolo Capriotti
Cool! I like how you use graphs to construct the mediating morphism. This technique seems to be worth knowing.

Soichiro Fujii (May 29 2020 at 11:09):

@Reid Barton
Okay, I got it. Thank you very much for explaining it in detail! It is also a nice result to know.

Paolo Capriotti (May 29 2020 at 11:56):

@Reid Barton nice argument! This works more generally for sifted colimits with the same proof, right?