User:Leigh.Samphier/Topology/Equivalence of Definitions of Spatial Locale

This page needs proofreading. Please check it for mathematical errors. If you believe there are none, please remove {{Proofread}} from the code. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Proofread}} from the code.

Therorem

Let $L = \struct{S, \preceq}$ be a locale.

The following definitions of the concept of Spatial Locale are equivalent:

Definition 1

$L$ is called a spatial locale if and only if $L$ is isomorphic to the locale of a topological space in the category of locales.

Definition 2

$L$ is called a spatial locale if and only if:

$\forall a, b \in L : a \npreceq b \implies \exists$ a frame homomorphism $p: L \to \mathbf 2 : \map p a = \top, \map p b = \bot$

where $\mathbf 2$ denotes the Boolean Latice $\struct{\mathbf 2, \lor, \land, \neg, \preceq}$.

Proof

$\blacksquare$