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: CH in a topos

Fawzi Hreiki (Feb 11 2021 at 19:12):

A topos with NNO satisfies the continuum hypothesis iff for any object $X$ and monomorphisms $\mathbb{N} \hookrightarrow X \hookrightarrow \mathcal{P}\mathbb{N}$, one of them has to be an isomorphism. Does this imply anything about the logic of the topos? For example, is a CH topos always Boolean?

Morgan Rogers (he/him) (Feb 11 2021 at 20:23):

I was well into a long answer to this by the time I realised that statement of CH is wrong :relieved:

Morgan Rogers (he/him) (Feb 11 2021 at 20:24):

To be fair to you, this is also wrong on the nlab!!! (I'll change it tomorrow if someone hasn't already)

Morgan Rogers (he/him) (Feb 11 2021 at 20:29):

Suppose we work in a category $\mathbf{Set}$ of ZFC sets satisfying the continuum hypothesis (because Gödel says we can). The canonical map $\mathbb{N} \hookrightarrow 2^{\mathbb{N}}$ sends each element to the classifying map for the singleton. But even ignoring that, consider ANY injective function $\mathbb{N} \hookrightarrow 2^{\mathbb{N}}$, and let $x \in 2^{\mathbb{N}}$ be any element not in the image. Then we have inclusions $\mathbb{N} \hookrightarrow \mathbb{N} \cup \{x\} \hookrightarrow 2^{\mathbb{N}}$, and neither is an isomorphism... Oops!

Fawzi Hreiki (Feb 11 2021 at 21:41):

Yup you're right. Ok so a topos satisfies CH iff there does not exist an object $X$ with monomorphisms $\mathbb{N} \hookrightarrow X \hookrightarrow \mathcal{P}\mathbb{N}$ such that $X$ is not isomorphic to either.

Todd Trimble (Feb 12 2021 at 01:13):

Anyway, I think the answer is no, it's not necessarily Boolean. I'm no expert, but I think the idea is that already CH fails on presheaves on the Cohen poset, because the Cohen poset is tailored to make that happen, and this presheaf topos is not Boolean. Most of the rest of the development from there is technical (pass to double negation sheaves to enforce Booleanness, pass to a filterquotient to enforce 2-valuedness).

I can't think of specific propositional properties of $\Omega$ that would be entailed by violation of CH. I should think that such violation would be "the norm".

Jens Hemelaer (Feb 12 2021 at 10:56):

For a hyperconnected Grothendieck topos, we get the following situation:

Let $f : \mathcal{E} \to \mathbf{Sets}$ be the unique geometric morphism. Since this is hyperconnected, we have that the inverse image functor $f^*$ is fully faithful, and the image of $f^*$ is closed under subobjects. The sheaves in the image of $f^*$ are the "discrete sheaves" and the full subcategory of discrete sheaves is equivalent to the category of sets. The natural number object is $f^*\mathbb{N}$, so this is a discrete sheaf as well. On the other hand, $\mathcal{P}\mathbb{N}$ does not have to be discrete. But I think the inclusion $f^*(2) \subseteq \Omega$ will induce an inclusion $f^*(2^\mathbb{N}) \subseteq \mathcal{P}\mathbb{N}$.

Now there are two cases:

• The sheaf $\mathcal{P}\mathbb{N}$ is not discrete. In this case, $f^*(2^\mathbb{N})$ is a counterexample to CH: it is not isomorphic to $f^*(\mathbb{N})$ and because it is discrete it is also not isomorphic to $\mathcal{P}\mathbb{N}$.
• The sheaf $\mathcal{P}\mathbb{N}$ is discrete. Then because subsheaves of discrete sheaves are again discrete, we get that any counterexample to CH must be of the form $f^*(X)$ for some set $X$. So in this case, CH holds in $\mathcal{E}$ if and only if CH holds in $\mathbf{Sets}$.

So I agree with @Fawzi Hreiki and @Todd Trimble that failure of CH seems to be the norm.

For hyperconnected Grothendieck toposes, we have the necessary condition that if CH holds, then $\mathcal{P}\mathbb{N}$ is discrete. I think $\mathcal{P}\mathbb{N} = \prod_{n \in \mathbb{N}} \Omega$, so if this is discrete then also the subobject classifier $\Omega$ must be discrete, since we have the diagonal embedding $\Omega \to \prod_{n \in \mathbb{N}} \Omega$. But if $\Omega$ is discrete, then necessarily $\Omega = f^*(2)$ (by checking the universal property against other discrete sheaves), in other words $\mathcal{E}$ is boolean.

So this shows that in this case CH implies booleanness, as you suspected. Unfortunately, this proof only works for hyperconnected Grothendieck toposes, maybe it can be extended to other cases as well.

Morgan Rogers (he/him) (Feb 12 2021 at 11:44):

Here's a sketch of how I think one could complete Jens' analysis: let $\mathcal{E}$ be a topos over a topos of ZFC sets, $\mathbf{Set}$, and consider a subterminal object $U$ distinct from $0$. I claim that if $\mathbb{N}+U \cong \mathbb{N}$, then $U \cong 1$. This relies on countable extensivity, to the effect that the coproduct decomposition of $\mathbb{N}$ pulls back along the isomorphism, and one of the pieces must be (part of) $U$, and hence this must be isomorphic to $1$.
If that all works out, then since we always have $\mathbb{N} \hookrightarrow \mathbb{N}+U \hookrightarrow \mathbb{N} + 1 \cong \mathbb{N}$, we conclude that CH implies two-valuedness, and hence that $\mathcal{E}$ is hyperconnected over $\mathbf{Set}$, so we can apply Jens' argument to deduce Booleanness.

Morgan Rogers (he/him) (Feb 12 2021 at 11:49):

Personally, I find this dissatisfying, and would prefer a formulation of CH that produces some more interesting cases. For example, we could demand that whenever $\mathbb{N} \hookrightarrow X \hookrightarrow \Omega^{\mathbb{N}}$, there exists either a monomorphism $X \hookrightarrow \mathbb{N}$ or $\Omega^{\mathbb{N}} \hookrightarrow X$. This recovers the usual notion of cardinality in terms of injections in $\mathbf{Set}$, but avoids the cheap trick for localic toposes I describe above.

Morgan Rogers (he/him) (Feb 12 2021 at 12:02):

Incidentally, I just checked in Sheaves in Geometry and Logic, and the version that Mac Lane and Moerdijk go for is to show that in the Cohen topos there is an object $K$ with monomorphisms $\mathbb{N} \hookrightarrow K \hookrightarrow \Omega^{\mathbb{N}}$ but no epimorphisms $\mathbb{N} \twoheadrightarrow K$ or $K \twoheadrightarrow \Omega^{\mathbb{N}}$. Assuming choice (to make all the sets decidable), for non-empty sets this is equivalent to saying there are no monomorphisms in the other direction, but if we're considering CH without choice, I prefer a formulation which makes things more interesting!

Jens Hemelaer (Feb 12 2021 at 12:16):

Interesting that the stronger formulation of CH even forces a Grothendieck topos to be both two-valued/hyperconnected and boolean!

There is probably no single formulation of CH that is seen as the "standard" in topos theory. Another formulation closer to the original one would be to ask whether $\mathbb{N} \subseteq X \subseteq \mathbb{R}$ implies $X \cong \mathbb{N}$ or $X \cong \mathbb{R}$, where $\mathbb{N}$ is a natural number object and $\mathbb{R}$ is e.g. the Dedekind real numbers.

Morgan Rogers (he/him) (Feb 12 2021 at 12:19):

Right, but again that falls into the same issue that I pointed out involving subterminals. I still think it should be presented with monomorphisms rather than isomorphisms

Matteo Capucci (he/him) (Feb 12 2021 at 12:24):

Morgan Rogers (he/him) said:

Here's a sketch of how I think one could complete Jens' analysis: let $\mathcal{E}$ be a topos over a topos of ZFC sets, $\mathbf{Set}$, and consider a subterminal object $U$ distinct from $0$. I claim that if $\mathbb{N}+U \cong \mathbb{N}$, then $U \cong 1$. This relies on countable extensivity, to the effect that the coproduct decomposition of $\mathbb{N}$ pulls back along the isomorphism, and one of the pieces must be (part of) $U$, and hence this must be isomorphic to $1$.
If that all works out, then since we always have $\mathbb{N} \hookrightarrow \mathbb{N}+U \hookrightarrow \mathbb{N} + 1 \cong \mathbb{N}$, we conclude that CH implies two-valuedness, and hence that $\mathcal{E}$ is hyperconnected over $\mathbf{Set}$, so we can apply Jens' argument to deduce Booleanness.

Which form of CH are you using for the last implication?

Matteo Capucci (he/him) (Feb 12 2021 at 12:27):

Morgan Rogers (he/him) said:

Personally, I find this dissatisfying, and would prefer a formulation of CH that produces some more interesting cases. For example, we could demand that whenever $\mathbb{N} \hookrightarrow X \hookrightarrow \Omega^{\mathbb{N}}$, there exists either a monomorphism $X \hookrightarrow \mathbb{N}$ or $\Omega^{\mathbb{N}} \hookrightarrow X$. This recovers the usual notion of cardinality in terms of injections in $\mathbf{Set}$, but avoids the cheap trick for localic toposes I describe above.

This feels like the right formulation. As you point out after, it's the 'constructive version' of SGL 'no epi' version.

Morgan Rogers (he/him) (Feb 12 2021 at 12:34):

Matteo Capucci (he/him) said:

Morgan Rogers (he/him) said:

... since we always have $\mathbb{N} \hookrightarrow \mathbb{N}+U \hookrightarrow \mathbb{N} + 1 \cong \mathbb{N}$, we conclude that CH implies two-valuedness...

Which form of CH are you using for the last implication?

I'm saying we can extend the sequence with $\mathbb{N} \hookrightarrow \Omega^{\mathbb{N}}$ and argue that we don't have an isomorphism $\mathbb{N}+U \cong \Omega^{\mathbb{N}}$ to conclude that we must have an isom with $\mathbb{N}$, to apply the preceding argument to.

David Michael Roberts (Feb 12 2021 at 23:34):

So I guess the iso vs mono issue is secretly hiding some Cantor–Schröder–Bernstein issues. Since CSB only holds in Boolean toposes, one doesn't want to secretly force (hah) Booleanness in this way.

Matteo Capucci (he/him) (Feb 13 2021 at 08:31):

Yeah exactly

Morgan Rogers (he/him) (Feb 13 2021 at 15:25):

Edited, including @David Michael Roberts' connection to CSB. Now someone needs to write a paper with me characterising CH Grothendieck toposes!

David Michael Roberts (Feb 14 2021 at 01:06):

Amusingly, the recent formal proof of independence of CH from ZFC used the following weak formulation:

$CH := \forall x,\ Ord(x)\Rightarrow x \leq \omega \vee P(\omega)\leq x$

where $x\leq y$ means $x$ is a subquotient of $y$. Clearly it relies on the well-ordering principle (so all sets are in bijection with an ordinal) and the fact the (classical) ordinals are linearly ordered, but I've never seen it stated like this before. One could ask what a similar formulation would look like in a general topos:

for all sets $x$, $x\leq \mathbb{N}$ or $P(\mathbb{N}) \leq x$,

using $\leq$ for subquotient again. Here one would have to interpret this in the internal logic, and I suspect that being a subquotient in the internal logic is not too far from being a subquotient in the external logic.

David Michael Roberts (Feb 14 2021 at 02:03):

Now added this to the nLab page as well.

Jacques Carette (Feb 14 2021 at 14:25):

I think the link isn't what you wanted to link to?

David Michael Roberts (Feb 14 2021 at 21:34):

Oops! Fixed. Thanks for letting me know.

Martti Karvonen (Feb 15 2021 at 14:04):

Bit of an aside, but since @David Michael Roberts alluded that CSB implies Booleannes, how about requiring that the monomorphism preorder is total? I.e. for any two objects, there is a mono one way or the other?

David Michael Roberts (Feb 15 2021 at 14:15):

I should give a source for my claim: Pierre Pradic and Chad E. Brown, Cantor-Bernstein implies Excluded Middle arXiv:1904.09193

Keith Elliott Peterson (Feb 16 2021 at 00:53):

Sorry for coming into this late. If I understand correctly, we're coming up with a new relation $\subset':: \mathbb{N}\nrightarrow {2^{2^\mathbb{N}}}$ or $\widehat{\subset'}: \mathbb{N}\to {2^{2^{2^\mathbb{N}}}}$, and then using that as a notion of subset?

Can this be generalized to a whole universe $U$?

David Michael Roberts (Feb 16 2021 at 09:30):

I'm not sure what you mean, are you referring to what I wrote or others earlier in the conversation?

Keith Elliott Peterson (Feb 16 2021 at 20:16):

To be fair, I'm coming at this as an outsider, so I may not even be sure what I mean.

David Michael Roberts (Feb 16 2021 at 21:28):

I just mean, to whom are you replying, or is a general comment? I can explain what I meant, if it was me, but otherwise I don't want to presume.

Keith Elliott Peterson (Feb 17 2021 at 01:57):

David Michael Roberts said:

I just mean, to whom are you replying, or is a general comment? I can explain what I meant, if it was me, but otherwise I don't want to presume.

Oh, it's just a general comment where I'm just talking (writing?) out loud.

David Michael Roberts (Feb 17 2021 at 03:41):

OK. The only think I can think of to sensibly say in response is that it's not really a 'subset', given the tower of exponents like that, though it's not clear to me what the 'subset' is supposed be a 'subset' of. (the natural numbers? The power set? The iterated power set?).

The only thing that might be unfamiliar from what I wrote is the notion of subquotient. Given a set $X$, then $Y$ is a subquotient of $X$ if there is a subset $X' \subseteq X$ and an onto function $X' \to Y$. Using classical logic, this is equivalent to either $Y$ being the empty set, or there being an onto function $X\to Y$ (via a choice retraction $X\to X'$). Any subset is a subquotient, too. So it's a measure of relative size, but one that makes a little more sense using non-classical logic. Particularly, for instance if $X'$ is recursively enumerable, but its complement is not, so then you cannot cook up a computable function $X \to X'$ in order to get a surjective function $X\to Y$.

Todd Trimble (Feb 17 2021 at 14:32):

It's been noted at the nForum that a substantial anonymous edit had been made on CH in predicative mathematics. The custom is normally to report big edits to the nForum, something made automatic by the "describe your changes" box that appears whenever you edit at the nLab. I expect the edit came from someone here.

Morgan Rogers (he/him) (Feb 17 2021 at 14:46):

It's easy to verify that no one here was responsible, given the dates: David Corfield's comment is from 7 days ago (so the 10th), and the anonymous changes were made on the 9th, while this thread was only started on the 11th. @David Michael Roberts did make an edit to that page on the same day, though.

Morgan Rogers (he/him) (Feb 17 2021 at 14:47):

It's a good thing "the custom" happens automatically, since it's the first I'm hearing of it, and @John Baez and others are frequently encourage updating the nLab without mentioning the nForum.

Morgan Rogers (he/him) (Feb 17 2021 at 14:50):

A third thing: "a substantial anonymous edit had been made on CH in predicative mathematics" is inaccurate, since looking at the history of the page, that edit was responsible for introducing the section on CH in predicative mathematics :joy:

Todd Trimble (Feb 17 2021 at 15:56):

Morgan Rogers (he/him) said:

It's a good thing "the custom" happens automatically, since it's the first I'm hearing of it, and John Baez and others are frequently encourage updating the nLab without mentioning the nForum.

It's the reporting (of edits to nLab entries) to the nForum that happens automatically when one uses that box. (Was it unclear that's what I meant?)

To say more about "custom", or at any rate about good practice (which may have been more customary in the past than it is now): not only should one report substantial edits in this way, but one should keep an eye out for any nForum responses made to the edit and be willing to engage with them. For a little while after the edit, anyway.

I wish it were automatic that people making nLab edits would be subscribed to the nForum, but I think it's still the case that that requires a separate action. Fortunately, it's really easy to subscribe.

Morgan Rogers (he/him) (Feb 17 2021 at 16:11):

That's valuable to know, thank you! I wasn't being disingenuous by the way; this really is the first time I'm hearing about the nForum in association with making edits on the nLab, besides its mention on the edit page itself, which I've only used twice. I'll be sure to mention it when people suggest making edits to nLab pages in future!

Todd Trimble (Feb 17 2021 at 16:26):

Okay, great; thanks. To add further clarity: I wasn't trying to wag my finger at anyone -- I was only pointing out that a substantial edit had been noticed over there, and was reporting that back here in case someone here had made the edit. (I guess it was sheer coincidence that the timing between that edit and this discussion was so close.)

Also, I want to say that tiny edits (like fixing typos) need not be reported at the nForum (and in my opinion, shouldn't be).