Spectrum of Locale as Completely Prime Filters is Sober Space

== Theorem ==
Let $\struct{L, \preceq}$ be a locale.
Let $\map {\operatorname{Sp}} L$ denote the spectrum as completely prime filters of $L$.
Then:
:$\map {\operatorname{Sp}} L$ is a sober space.
== Proof ==
By definition of spectrum as completely prime filters:
:$\map {\operatorname{Sp}} L = \struct{\map {\operatorname{pt}} L, \set{\Sigma_a : a \in L}}$
where:
:$\map {\operatorname{pt}} L$ denotes the set of points as completely prime filters of $L$
:$\forall a \in L : \Sigma_a = \set{p \in \map {\operatorname{pt}} L : a \in p}$
Let $\Sigma_L = \set{\Sigma_a : a \in L}$.
Let $\Sigma : L \to \powerset {\map {\operatorname{pt}} L}$ be the mapping defined by:
:$\forall a \in L : \map \Sigma a = \Sigma_a$
where $\powerset {\map {\operatorname{pt}} L}$ denotes the powerset of $\map {\operatorname{pt}} L$.
From Canonical Mapping of Locale to Powerset of Points is Frame Homomorphism:
:$\Sigma: \struct{L, \preceq} \to \struct{\powerset {\map {\operatorname{pt}} L}, \subseteq}$ is a frame homomorphism.
=== $\Sigma_L$ satisfies Open Set Axiom $(\text O 1)$ ===
Let $\set{\Sigma_{a_i} : i \in I}$ be an indexed family of subsets of $\Sigma_L$.
Let $\ds \bigvee_{i \in I} a_i$ denote the supremum of $\set{a_i : i \in I}$.
We have:
Hence:
:$\ds \bigcup_{i \in I} \Sigma_{a_i} \in \Sigma_L$
It follows that $\Sigma_L$ satisfies . 
=== $\Sigma_L$ satisfies Open Set Axiom $(\text O 2)$ ===
Let $\Sigma_{a_1}, \Sigma_{a_2} \in \Sigma_L$.
We have:
Hence:
:$\Sigma_{a_1} \cap \Sigma_{a_2} \in \Sigma$
It follows that $\Sigma$ satisfies . 
=== $\Sigma_L$ satisfies Open Set Axiom $(\text O 3)$ ===
By definition of locale:
:$\struct{L, \preceq}$ has a greatest element $\top$
From Supremum of Power Set:
:$\map {\operatorname{pt}} L$ is the greatest element of $\struct{\powerset {\map {\operatorname{pt}} L}, \subseteq}$ 
We have:
Hence:
:$\map {\operatorname{pt}} L \in \Sigma_L$
It follows that $\Sigma$ satisfies . 
=== $\map {\operatorname{Sp}} L$ is a Topological Space ===
We have shown that $\Sigma_L$ satisfies the open set axioms.
Hence $\map {\operatorname{Sp}} L$ is a topological space by definition.
=== $\map {\operatorname{Sp}} L$ is a Sober Space ===
Let $\FF$ be a completely prime filter in $\struct{\Sigma_L, \subseteq}$.
Let:
:$p = \set{a \in L : \Sigma_a \in \FF}$.
==== $p$ is a Completely Prime Filter of $L$ ====
It follows that $p$ is a completely prime filter of $L$ by definition.
By definition of point of locale:
:$p$ is a point of $L$
==== $\FF$ is System of Open Neighborhoods $\map \UU p$ ====
Let $\map \UU p$ denote the system of open neighborhoods of $p$ in $\map {\operatorname{Sp}} L$.
We have:
By definition of set equality:
:$\FF = \map \UU p$
Let $\map \UU p = \map \UU q$ for some $p, q \in \map {\operatorname{pt}} L$.
We have:
By definition of set equality:
:$p = q$
Hence $\FF$ is a system of open neighborhoods for some unique $p \in \map {\operatorname{pt}} L$.
It follows that every completely prime filter in $\struct{\Sigma_L, \subseteq}$ is a system of open neighborhoods for some unique $p \in \map {\operatorname{pt}} L$.
From Sober Space iff Completely Prime Filter is Unique System of Open Neighborhoods:
:$\map {\operatorname{Sp}} L$ is a sober space
== Sources ==
* : Chapter $\text {II}$: Frames and Locales. Spectra, $\S 4$ Spectra, Definition $4.1$ and $\S 6$ The unit $\lambda$ and sobriety, Proposition $6.1$
Category:Spectra of Locales