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: reading & references

Topic: Reference for Brouwer's Principle in Johnstone's Topos

Chris Grossack (they/them) (Apr 10 2024 at 06:31):

It seems to be folklore that Johnstone's topological topos validates Brouwer's "continuity principle" that every function $\mathbb{R} \to \mathbb{R}$ is continuous. In fact, it might validate more: that for every pair of spaces, all maps between them are continuous.

Does anyone have a reference for this? Maybe it's not hard to prove directly, in which case I'd also be interested in just seeing a proof here.

Thanks in advance ^_^

Chris Grossack (they/them) (Apr 10 2024 at 06:54):

Actually, it wasn't as annoying as I expected to just prove it... I think, haha. I'll try to remember to post a proof here tomorrow if nobody beats me to it. Of course, I would still be interested in a reference that's already in the literature!

Reid Barton (Apr 11 2024 at 16:24):

Chris Grossack (they/them) said:

for every pair of spaces, all maps between them are continuous.

What do you mean by space, map and continuous?

Reid Barton (Apr 11 2024 at 16:32):

in particular, are you looking for an internal or external statement?

Reid Barton (Apr 11 2024 at 16:36):

If an external statement, this is basically Proposition 4.4 of Johnstone's original paper (together with Lemma 2.1 to identify sequential topological spaces with a full subcategory of the topological topos).

Chris Grossack (they/them) (Apr 11 2024 at 19:20):

I want an internal statement, in the sense of Mac Lane and Moerdijk VI.9, but I'm pretty sure their construction doesn't work for the topological topos. Unless there's another site I'm unaware of (there could easily be)

Chris Grossack (they/them) (Apr 11 2024 at 19:21):

I was able to prove it for functions from the reals to the reals (and I've written it in full. It'll be in an upcoming blog post) but I'm still curious if you can say something for other spaces

Mike Shulman (Apr 11 2024 at 20:14):

If you want an internal statement, then you have to say what you mean by "other spaces". It's certainly not true internally in any topos that "every function between two topological spaces is continuous" if "topological space" is also defined internally in an ordinary explicit way, e.g. using open sets.

Reid Barton (Apr 11 2024 at 20:18):

Right, there is also the internal statement that every function from the reals to the reals is continuous in the $\epsilon$-$\delta$ sense, and we can make up some analogous statements for e.g. $2^\mathbb{N}$, but it's not clear what "continuity" would mean for a general object.

Chris Grossack (they/them) (Apr 11 2024 at 20:20):

Understanding what one might mean by this is part of what I'm looking for

Chris Grossack (they/them) (Apr 11 2024 at 20:22):

For instance, if $\Sigma$ is the sierpinski space, then $\Sigma^X$ is an internal representation of the lattice of opens. But this is "too easy" because then just pullback gives you the claim. In fact, maybe that's what people mean. It's certainly simple enough to not require a proof

Mike Shulman (Apr 11 2024 at 20:26):

Who are the "people"?

Reid Barton (Apr 11 2024 at 20:42):

There is a subject called synthetic topology where you postulate an "open subobject/proposition classifier" $\Sigma$ and this induces a sort of internal topology on each object with respect to which all functions are automatically continuous, just like you say.

But this is a different thing from Brouwer's Principle about functions from the reals to the reals, which doesn't depend on any extra postulated constants like $\Sigma$, but instead is based on the traditional definition of the topology of the real numbers (in terms of open intervals).

Chris Grossack (they/them) (Apr 11 2024 at 20:43):

The reference I'm able to find quickly is Jem's answer here, which is only for complete metric spaces. I understand this case since we can ask for the $\delta$-$\epsilon$ definition to be true, and probably some version of the $\mathbb{R} \to \mathbb{R}$ argument works in this setting.

Chris Grossack (they/them) (Apr 11 2024 at 20:44):

That said, I'm sure that I've seen the claim made for "spaces" more broadly, but I don't have a reference on hand. Maybe someone was speaking imprecisely, or maybe they were just mistaken. Or maybe some statement of this form is true, but I don't know what that statement is. I'm not sure

Mike Shulman (Apr 11 2024 at 20:50):

I would guess that the only statements like this that are going to be true are those that use a synthetic notion of space, as Reid mentioned, and those with some completeness and separation conditions, as in the answer you linked to.

Benedikt Peterseim (Apr 11 2024 at 21:42):

@Chris Grossack (they/them) Are you aware of Davorin Lešnik‘s thesis (https://arxiv.org/pdf/2104.10399.pdf). It shows what you are looking for, for "other spaces" = complete metric spaces, and for different topoi.