Timeline for What is the status of Jordan's theorem in constructive mathematics in the language of locales?
Current License: CC BY-SA 4.0
34 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 3, 2021 at 12:58 | comment | added | Simon Henry | After more thought : If $(-\infty,0]$ and $[0,\infty)$ denotes the closed sublocales of the topological space $\mathbb{R}$ then their union as sublocale is indeed $\mathbb{R}$. What I can't quite figure out is whether these two closed sublocales are spatial or not. If they are it indeed means that any sublocale containing their points is $\mathbb{R}$ so that the set $(-\infty,0] \cup [0,\infty)$ can't be sober as a subspace. But, If they are not spatial, then you can interpret $[0,\infty)$ differently (as a spatial subpace) and I don't know if the union is $\mathbb{R}$ in this case. | |
| Nov 3, 2021 at 4:35 | comment | added | Mike Shulman | I believe I have heard that Hausdorff=>sober is indeed nonconstructive. | |
| Nov 2, 2021 at 18:53 | vote | accept | Arshak Aivazian | ||
| Nov 2, 2021 at 15:57 | comment | added | Simon Henry | @FrançoisG.Dorais If you define the union as the pushout over singleton ${0}$ or as supremum of sublocales then yes : union of closed sublocale corresponds to the (closed complement) intersection of their open complements, and here it is clear that the intersection of the open complement is empty. I guess the problem is that as a subset $(-\infty,0] \cup [0,+ \infty) $ it is not sober ? (or rather that assuming it is sober least to the conlusion that it contains all reals...) I had never pushed that line of thought this far... Maybe Haussdorf $\Rightarrow$ sober is non-constructive ? | |
| Nov 2, 2021 at 15:47 | comment | added | François G. Dorais | @SimonHenry I'm still confused here. Are you saying that $(-\infty,0]\cup[0,\infty) = \mathbb{R}$ is always true as locales? That seems to contradict that the map from subspaces to sublocales is injective, which I imagined was always true. | |
| Nov 2, 2021 at 14:29 | answer | added | Simon Henry | timeline score: 4 | |
| Nov 2, 2021 at 13:32 | comment | added | Simon Henry | @FrançoisG.Dorais The claim in your comment is correct but start from the assumption that the map $t \mapsto (cos(t),sin(t) ) $ ( $t \in [0,2 \pi ]$) is surjective "on points" (I.e. real numbers), while the claim I was making (and mike was answering too) is about this map being a proper surjection of locales (and hence the coequalizer of its kernel pair). Proper surjection of locales or coequalizer of locales don't have to be surjective on points. | |
| Nov 2, 2021 at 7:54 | comment | added | François G. Dorais | @SimonHenry I didn't say anything about points. What am I missing? | |
| Nov 1, 2021 at 23:52 | comment | added | Simon Henry | @FrançoisG.Dorais what you are talking about is for topological space, not for locales ( an equalizer of locales don't have to be surjective on points) | |
| Nov 1, 2021 at 22:39 | history | edited | Arshak Aivazian | CC BY-SA 4.0 |
added 106 characters in body
|
| Nov 1, 2021 at 20:08 | comment | added | Andrej Bauer | @MikeShulman: In the effective topos every map $S^1 \to \mathbb{R}^2$ is pointwise continuous, and there is an embedding $f : S^1 \to \mathbb{R}^2$ whose image is unbounded. So at least one part of Jordan's curve theorem fails (namely that one of the regions is bounded). There is a paper about The constructive Jordan curve theorem. It might be translatable to the localic version. | |
| Nov 1, 2021 at 20:01 | comment | added | François G. Dorais | @MikeShulman is correct. To see more concretely, the circle $x^2+y^2=1$ is not the image of the classical parametrization $(\cos t, \sin t)$ for $t \in [0,2\pi]$ unless real numbers are dichotomous: $\forall x,y(x \ge y \lor x \le y)$. | |
| Nov 1, 2021 at 19:46 | comment | added | François G. Dorais | I'm also a bit puzzled, but my main concern is that you don't state the conclusion of the theorem. This is important since there are usually several choices when reinterpreting a classical theorem intuitionistically. | |
| Nov 1, 2021 at 19:44 | comment | added | Simon Henry | @MikeShulman : Maybe it is only true when using the formal locale and not the topological spaces and that's what you are refering too ? (I'm not sure about the non-pointfree statement) But as locale it is true : The map $[0,1] \to S^1$ is a proper surjection so it is an effective epimorphism ( even an effective descent map), and the kernel just identify the end points. | |
| Nov 1, 2021 at 19:34 | comment | added | Mike Shulman | @AndrejBauer I'm curious whether anything is known about the point-ful version of this theorem too (with uniform continuity etc.)? | |
| Nov 1, 2021 at 19:32 | comment | added | Mike Shulman | @SimonHenry Are you sure about that? I thought that $[0,1]/(0\sim 1)$ was not constructively the same as $S^1$, because it has a "bump" at the point of joining. E.g. in a topological model, the continuous paths in the quotient have to stop momentarily when passing through the join point. I thought to get $S^1$ you have to do glue along an open neighborhood rather than a point. | |
| Nov 1, 2021 at 19:24 | comment | added | Simon Henry | Regarding the question it self. This is definitely not something that I have ever seen done, so I would be suprised if there was a constructive proof available. But it might be something we can reach using a Barr covering argument.... That won't prove the result constructively, but it could at least show it is possible. | |
| Nov 1, 2021 at 19:21 | comment | added | Simon Henry | Some comments : Yes map from I to anything such that $f(0) = f(1)$ are the same as maps from $S^1$. Embeddings and Mono are the same when the domain is compact and the target is Haussdroff (because a proper mono is the sane as a closed embeddings). Finally, when talking about $I$, $S^1$ and $ \mathbb{R}$ you should make sure you talk about the "formale locale" (and not the spatial locale), OR that you restrict to uniformly continuous map, but there is no need to do both ( the formal locale are compact and continuous functions on compact are uniformly continuous). | |
| Nov 1, 2021 at 17:52 | history | edited | Arshak Aivazian | CC BY-SA 4.0 |
added 2 characters in body
|
| Nov 1, 2021 at 17:51 | comment | added | Arshak Aivazian | @AndrejBauer Oh, but in order not to talk about points, it is better to change of course to a circle, yes, sorry. Thanks! | |
| Nov 1, 2021 at 17:48 | comment | added | Arshak Aivazian | @AndrejBauer In constructive mathematics, there is still a natural bijection between continuous mappings from the segment $[0, 1]$ such that $f (0) = f (1)$ and continuous mappings from the circle $S ^ 1$. Right? | |
| Nov 1, 2021 at 17:48 | comment | added | Arshak Aivazian | @AndrejBauer And in constructive mathematics it is not possible to prove that for functions from $I$ to $\mathbb{R}^2$ this is the same thing? (this is true in the classical for mappings from a compactum to a Hausdorff space). | |
| Nov 1, 2021 at 17:36 | comment | added | Andrej Bauer | Let's clear up whether we want an injection (mono) or an embedding (regular mono), and should we not use the circle $S^1$ as the domain? | |
| Nov 1, 2021 at 17:33 | history | edited | Arshak Aivazian | CC BY-SA 4.0 |
added 74 characters in body
|
| Nov 1, 2021 at 17:10 | comment | added | Peter LeFanu Lumsdaine | @EschatumVerus: Yes, sorry if I was a little nitpicky — I’ve just seen misunderstandings about locales and points happen slightly too often before! | |
| Nov 1, 2021 at 15:41 | comment | added | Arshak Aivazian | @PeterLeFanuLumsdaine I meant "in general, locales do not have points." I know that points are naturally defined in terms of locales, but didn't think about it, yes. Indeed, for morphisms from the $I$ to the $\mathbb{R}^2$, we can speak simply of "injections". | |
| Nov 1, 2021 at 10:12 | comment | added | Peter LeFanu Lumsdaine | @EschatumVerus: Be careful with the statement “locales have no points”. They’re not defined in terms of their points, but many locales have points — i.e. locale maps from the terminal locale — and they’re a very useful notion in locale theory. (Nice question, by the way!) | |
| Nov 1, 2021 at 9:38 | comment | added | Andrej Bauer | What are dots? Do you mean points? I am familiar with locales, my remarks about weird things happening was about the non-localic version. | |
| Nov 1, 2021 at 9:37 | comment | added | Arshak Aivazian | @AndrejBauer Yes, I did not know that LEM follows from the ZF axioms for some classes of formulas, thanks. | |
| Nov 1, 2021 at 9:36 | comment | added | Arshak Aivazian | @AndrejBauer Locales have no points (added a link to the corresponding page in nlab) | |
| Nov 1, 2021 at 9:35 | history | edited | Arshak Aivazian | CC BY-SA 4.0 |
added 40 characters in body
|
| Nov 1, 2021 at 8:41 | comment | added | Andrej Bauer | You could also just say that a Jordan curve is a regular mono $S^1 \to \mathbb{R}^2$, couldn't you? I don't know about the local version, but you would certainly want the map to be uniformly continuous, or else some really strange things can happen (a pointwise continuous image of an embedding $S^1 \to \mathbb{R}^2$ may be unbounded, for instance). | |
| Nov 1, 2021 at 8:38 | comment | added | Andrej Bauer | You probably mean Intuitionistic ZF by "ZF without excluded middle"? One has to be a bit careful how these things are phrased. | |
| Nov 1, 2021 at 1:54 | history | asked | Arshak Aivazian | CC BY-SA 4.0 |