Abstract characterisation of spatial frames / spatial locales

general-topologylocales

By definition, a spatial locale is a locale that is isomorphic to the locale of open sets of a topological space. See for example here: https://ncatlab.org/nlab/show/spatial+locale

Question: Is there any more abstract characterisation of the property of being spatial?

By "more abstract" I intend some condition that does not directly reference the existence of a topological space, and is preferably phrased purely in terms of the properties of the locale itself.

Thank you.

Best Answer

A frame $F$ is spatial if and only if for all $U,V\in F$, if $U\not\leq V$, then there exists a completely prime filter $p$ on $F$ such that $U\in p$ and $V\notin p$.

Note that this is characterization 3 on the nLab page you linked to, remembering that a "point" $p$ of $F$ is a completely prime filter on $F$ (equivalently, a frame homomorphism $F\to 2$), and a point $p$ "belongs to" $U$ if and only if $U\in p$.

Proof: Suppose $F$ is spatial. Then there is a topological space $X$ and an isomorphism $i\colon F\cong \mathrm{Open}(X)$, the frame of open sets in $X$. Suppose $U\not\leq V$ in $F$. Then $i(U)\not\subseteq i(V)$, so there is a point $x\in i(U)\setminus i(V)$. Let $p_x = \{W\in F\mid x\in i(W)\}$. Check that $p_x$ is a completely prime filter in $F$ such that $U\in p_x$ and $V\notin p_x$.

Conversely, suppose that for all $U,V\in F$, if $U\not\leq V$, then there exists a completely prime filter $p$ on $F$ such that $U\in p$ and $V\notin p$. Let $X$ be the space of points of $F$, whose points are completely prime filters in $F$ and whose open sets are of the form $[U] = \{p\in X\mid U\in p\}$ for $U\in F$. Check that these sets form a topology on $X$ and the map $i\colon U\mapsto [U]$ is a frame homomorphism $F\to \mathrm{Open}(X)$. This map is surjective by definition of the topology on $X$, so it remains to check that it is injective. If $U\neq V$ in $F$, then without loss of generality $U\not\leq V$. Let $p$ be a completely prime filter such that $U\in p$ and $V\notin p$. Then $p$ is a point of $X$ witnessing that $[U]\neq [V]$, so $i$ is an isomorphism of frames.

Related Question