Timeline for What's the point of a point-free locale?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 27 at 8:07 | history | edited | Gro-Tsen |
edited tags
|
|
| Jan 21, 2022 at 18:42 | vote | accept | Student | ||
| Jan 21, 2022 at 18:02 | comment | added | Ingo Blechschmidt | Regarding applications of topos theory, what about the classical examples such as crystalline cohomology or elucidating realizability and studying higher-order computability via the effective topos? For a recent and minor example, what about the proof of Grothendieck's generic freeness theorem using topos-theoretic methods (Section 3.5 in the linked notes)? Perhaps you can clarify your questions a bit so we can give more directed answers :-) | |
| Jan 21, 2022 at 15:14 | comment | added | Ingo Blechschmidt | Parts of your questions are answered in Sections 1.1f. of this note of mine. Briefly: Allowing locales without points streamlines the theory, helps massively in constructive mathematics (including relative mathematics over a base space) and is crucial for certain representation theorems in topos theory (for instance for showing that for any object $X$ of any topos $E$, there is a surjection $f:F\to E$ such that $f^*(X)$ is countable, namely the classifying $E$-locale of surjections $\mathbb{N}\to X$. This locale doesn't have any points if $X$ is uncountable) | |
| Jan 21, 2022 at 9:49 | history | became hot network question | |||
| Jan 21, 2022 at 0:13 | answer | added | Dmitri Pavlov | timeline score: 17 | |
| Jan 20, 2022 at 20:14 | comment | added | Andreas Blass | The first sentence of the question already contains an answer. If you identify the locale $Y$ there with the trivial locale (as you suggest), then you have a trivial locale dense in a nontrivial space $X$. That conflicts rather badly with the usual meaning of "trivial". | |
| Jan 20, 2022 at 20:09 | comment | added | Simon Henry | Just to clarify my previous comment : not considering locales without points is perfectly fine, there is no deep reason why you "can't" do it. It justs mean you are no longer working with locales but with (sober) topological spaces. As far as I'm concerned, there is no significant distinction between your question and "what's the point of locales over topological spaces" | |
| Jan 20, 2022 at 20:01 | comment | added | Simon Henry | If I remember correctly [2] already contains a lot of examples answering your question. For example I assume you have read about the closed subgroup theorem, or the smallest dense sublocales and how an intersection of dense sublocales is dense, or how pointfree locales are tied to set theoretic forcing ? or maybe I'm misunderstanding your question | |
| Jan 20, 2022 at 19:46 | history | asked | Student | CC BY-SA 4.0 |