Timeline for What does overtness mean for metric spaces?
Current License: CC BY-SA 4.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 13, 2021 at 20:06 | vote | accept | saolof | ||
| Oct 12, 2021 at 12:40 | comment | added | saolof | Ah right, that is a much better question. Thanks for the reformulation | |
| Oct 12, 2021 at 7:36 | history | edited | Paul Taylor | CC BY-SA 4.0 |
added 157 characters in body; edited tags; edited title
|
| Oct 11, 2021 at 19:29 | comment | added | Yemon Choi | @DavidRoberts Rohan has answered the call... | |
| Oct 11, 2021 at 19:25 | answer | added | Paul Taylor | timeline score: 6 | |
| Oct 11, 2021 at 10:25 | answer | added | Andrej Bauer | timeline score: 4 | |
| Oct 11, 2021 at 9:46 | comment | added | Bas Spitters | This depends on your definition of metric space. Proposition 2.16 in our paper here onlinelibrary.wiley.com/doi/10.1002/malq.201010011 says that the localic completion of a metric space is always overt. This is based on the work by Vickers and by Palmgren cited there. Could you refined your question to clarify the notion of metric space you are after? | |
| Oct 11, 2021 at 9:22 | answer | added | Ingo Blechschmidt | timeline score: 5 | |
| Oct 11, 2021 at 5:02 | comment | added | David Roberts♦ | We need to summon Paul Taylor! Also, more constructively (heh), would you be happy with the locale version of metric space or metrizable locales? (see eudml.org/doc/220278) I worry that overtness could become tautological if one makes the theory nice enough, but the risk is small (I have no idea either way) | |
| Oct 10, 2021 at 20:53 | history | edited | LSpice | CC BY-SA 4.0 |
Typo
|
| Oct 10, 2021 at 20:17 | answer | added | Arno | timeline score: 3 | |
| Oct 10, 2021 at 18:48 | comment | added | Andrej Bauer | I can answer the question, but to phrase it appropriately, can you please tell me whether you're familiar with synthetic topology. Non-overt spaces require that we restrict the completeness of the lattice of open sets (irrespective of whether we have excluded middle available). | |
| Oct 10, 2021 at 10:09 | history | edited | YCor | CC BY-SA 4.0 |
removed capitals
|
| Oct 10, 2021 at 10:01 | history | edited | saolof | CC BY-SA 4.0 |
added 5 characters in body; edited title
|
| Oct 10, 2021 at 9:56 | comment | added | saolof | @AlessandroDellaCorte Well, being too specific could also limit the answers too much. On the other hand, it does look like Sober implies Overt in any impredicative constructive setting which includes arbitrary toposes, which leads to an extension of what KPHart commented, and in which case the property may still be trivial constructively for metric spaces | |
| Oct 10, 2021 at 9:32 | history | edited | saolof | CC BY-SA 4.0 |
added 380 characters in body
|
| Oct 10, 2021 at 8:59 | comment | added | KP Hart | Also: in the normal topological setting every space is overt, so all definitions, subtly different or not, yield everything. See ncatlab.org/nlab/show/overt+space | |
| Oct 10, 2021 at 8:55 | history | edited | YCor |
edited tags
|
|
| Oct 10, 2021 at 8:53 | comment | added | Alessandro Della Corte | This may be interesting, but at the moment it’s a bit too vague, I think. Can you at least specify examples concerning compact metric spaces which you want to parallel in overt spaces? | |
| Oct 10, 2021 at 8:28 | history | asked | saolof | CC BY-SA 4.0 |