5
$\begingroup$

Is there an example of a locale/formal space which is not spatial (i.e., one can prove it is not spatial, rather than something like $\mathbb{R}$, where spatiality is independent in a constructive metatheory), but can be presented as an inductively generated formal topology (i.e., set-presented formal space)?

Some examples of interest are:

  • For many locales, the sublocale consisting of only the regular opens, i.e., opens such that $U = \neg \neg U$. Giovanni Curi's On some peculiar aspects of the constructive theory of point-free spaces proves that if such a locale (a Boolean locale) can be set-presented, then it must be the trivial locale (i.e., the one-point space). Such sublocales are generated by the nucleus $ U \mapsto \neg \neg U$. However, there are non-trivial spaces which are classically equivalent to Boolean locales which are inductively generated: the discrete spaces. But what about the double negation sublocales of $\mathbb{R}$ or the Cantor space $\mathbb{B}^\mathbb{N}$? These sublocales have no points, and so are not spatial (even classically); is there an inductively generated formal space which is classically equivalent to $\mathbb{R}_{\neg\neg}$ or ${\mathbb{B}^\mathbb{N}}_{\neg\neg}$?

  • Following Alex Simpsons's Measure, Randomness and Sublocales: For a probability distribution $\mu$ over a locale $A$, there is the sublocale $\text{Ran}(\mu)$ generated by the nucleus $$ U \mapsto \bigvee \{ V \ | U \le V, \mu(U) = \mu(V) \}$$ which (under some weak assumptions on $A$) is the smallest probability-1 sublocale of $A$. If $\mu$ is a non-atomic measure, then $\text{Ran}(\mu)$ has no points. For the "stream of coinflips" distribution on $\mathbb{B}^\mathbb{N}$, or any normal distribution on $\mathbb{R}$, is either of these sublocales classically equivalent to some inductively generated formal space?

My intuition is that at least some of these are not inductively generated. For instance, consider the random sublocale of $\mathbb{B}^\mathbb{N}$ for the "stream of coinflips" probability distribution. Then for any point $x : \text{Pt}(\mathbb{B}^\mathbb{N})$, there is the cover $$ \top \le (\cdot \neq x),$$ i.e., the whole space is covered by everything excluding a single point. There must be a similar cover for each point of the Cantor space, but (predicatively) the points of the Cantor space don't form a set (though I think they should in some sense be isomorphic to the set $\mathbb{N} \to \mathbb{B}$).

Improve this question
$\endgroup$
4
  • 3
    $\begingroup$ I'm not very familiar with the predicative settings and inductively generated formal topology so I'm not sure I can help, but are you familiar with this paper : jstor.org/stable/27588462?seq=1#page_scan_tab_contents (by Silvio Valentini "Every Countably Presented Formal Topology Is Spatial, Classically" ). It shows that if your inductively generated topology can be proved to be non-spatial then it cannot be countably generated ad depending on where you put the bar for "predicative" it can be impossible to produce set that not going to be countable classically. $\endgroup$
    – Simon Henry
    Commented Dec 14, 2016 at 12:00
  • 2
    $\begingroup$ I'm too not very familiar with formal topology. Is the pointless locale of surjections $\mathbb{N} \to \mathbb{R}$ an example of the kind you are looking for? It is freely generated by opens $U_{n,x}$ for $n \in \mathbb{N}$ and $x \in \mathbb{R}$ (intended reading: open subset of those surjections $f$ with $f(n) = x$) modulo three sets of relations: $\top = \bigvee_x U_{n,x}$ for all $n$ (read as: "$f(n)$ is defined"); $U_{n,x} \wedge U_{n,y} \leq \sup\{\top\,|\,x=y\}$ for all $n$, $x$, $y$ ("$f(n)$ has only a single value"); and $\top = \bigvee_n U_{n,x}$ for all $x$ ("$f$ is surjective"). $\endgroup$
    – Ingo Blechschmidt
    Commented Dec 14, 2016 at 20:42
  • $\begingroup$ @SimonHenry: Thanks so much for referring me to that paper! I was not previously aware of it, and basically answers my question. There was also an error in my question: though the points of $\mathbb{N}^\mathbb{B}$ do not form a set, they "essentially" do (Curi calls this "smallness"), and hence the covers in my example at the end could be inductively generated, hence giving a non-spatial inductively generated formal space. $\endgroup$
    – Ben
    Commented Dec 15, 2016 at 2:55
  • $\begingroup$ @IngoBlechschmidt: Yes, I think that example works; thanks! I was previously confused as to whether the points of $\mathbb{R}$ formed a set, and thus whether the example you have is indeed inductively generated, since it has $\mathbb{R}$-many axioms, and also joins over all of $\mathbb{R}$. But I now believe that these can be made predicatively acceptable because points of $\mathbb{R}$ "essentially" form a set. $\endgroup$
    – Ben
    Commented Dec 15, 2016 at 3:02

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .