\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{sober topological space}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{topology}{}\paragraph*{{Topology}}\label{topology}

[[!include topology - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{separation}{Separation}\dotfill \pageref*{separation} \linebreak
\noindent\hyperlink{AsLocalesWithEnoughPoints}{As locales with enough points}\dotfill \pageref*{AsLocalesWithEnoughPoints} \linebreak
\noindent\hyperlink{Reflection}{Soberification reflection}\dotfill \pageref*{Reflection} \linebreak
\noindent\hyperlink{enough_points}{Enough points}\dotfill \pageref*{enough_points} \linebreak
\noindent\hyperlink{examples_and_nonexamples}{Examples and Non-examples}\dotfill \pageref*{examples_and_nonexamples} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

If $\mathcal{O}(X)$ is the topology on a [[topological space]] $X$ (i.e. its [[frame of opens]]), and if a map $\mathcal{O}(X) \to \mathcal{O}(1)$ that preserves finite [[meets]] and arbitrary [[joins]] (a [[homomorphism]] of [[frames]]) is considered an instance of ``seeing a point $1 \to X$'', then $X$ is \emph{sober} precisely if every point we see is really there (i.e., is induced from a [[continuous function]] $1 \to X$), and if we never see double.

The condition that a [[topological space]] be \emph{sober} is an extra condition akin to a [[separation axiom]]. In fact with [[classical logic]] it is a condition implied by the $T_2$ [[separation axiom]] ([[Hausdorff implies sober]]) and implying $T_0$.

\begin{tabular}{l}
[[separation axioms]]\\
\hline 
$\itexarray{\\ &&& T_2 = \text{Hausdorff}  \\ && \swArrow && \seArrow \\ \, & T_1 && && \text{sober} & \, \\ && \seArrow && \swArrow \\ &&& T_0 = \text{Kolmogorov} \\ }$\\
\end{tabular}

(Note that this diagram is not a pullback -- there are [[Hausdorff implies sober|$T_1$ sober spaces which are not Hausdorff]].)

But the sobriety condition on a topological space has deeper meaning. It means that [[continuous functions]] betwen sober topolgical spaces are entirely determined by their [[inverse image]] functions on the [[frames of opens]], disregarding the underlying sets of points. Technically this means that the sober topological spaces are precisely the [[locales]] among the topological spaces.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

A [[topological space]] $X$ is \textbf{sober} if its [[points]] are exactly determined by its [[lattice of open subsets]]. Different equivalent ways to say this are:

\begin{itemize}%
\item The [[continuous map]] from $X$ to the space of points of the [[locale]] that it gives rise to (see there for details) is a [[homeomorphism]].


\item The [[function]] from points of $X$ to the \emph{[[completely prime filter|completely prime filters]]} of its open-set lattice is a [[bijection]].


\item (Assuming classical logic) every [[irreducible closed set]] (non-empty closed set that is not the [[union]] of any two proper closed subsets) is the [[topological closure|closure]] of a unique point.



\end{itemize}
In each case, half of the definition is that $X$ is [[T0]], the other half states that $X$ has \textbf{enough points}:

\begin{defn}
\label{EnoughPointsOfATopologicalSpace}\hypertarget{EnoughPointsOfATopologicalSpace}{}
A [[topological space]] $X$ has \emph{enough points} if the following equivalent conditions hold:

\begin{itemize}%
\item The [[continuous map]] from $X$ to the space of points of the [[locale]] that it gives rise to (see there for details) is a [[quotient space|quotient map]].


\item The [[function]] from points of $X$ to the \emph{[[completely prime filter|completely prime filters]] of its [[lattice of open subsets|open-set lattice]] is a [[surjection]].}


\item (Assuming classical logic) every [[irreducible closed set]] (non-empty closed set that is not the [[union]] of any two proper closed subsets) is the [[topological closure|closure]] of a point.



\end{itemize}
\end{defn}
\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{separation}{}\subsubsection*{{Separation}}\label{separation}

\begin{itemize}%
\item Sobriety is a [[separation property]] that is stronger than [[T0]], but incomparable with [[T1]]. With [[classical logic]], every [[Hausdorff space]] is sober (see at \emph{[[Hausdorff implies sober]]}), but this can fail [[constructive mathematics|constructively]].

\end{itemize}
\begin{displaymath}
Hausdorff = T_2 \Rightarrow sober \Rightarrow T_0
\end{displaymath}
\hypertarget{AsLocalesWithEnoughPoints}{}\subsubsection*{{As locales with enough points}}\label{AsLocalesWithEnoughPoints}

What makes the concept of sober topological spaces special is that for them the concept of [[continuous functions]] may be expressed entirely in terms of the relations between their [[open subsets]], disregarding the underlying set of points of which these open are in fact subsets. In order to express this property (proposition \ref{FrameMorphismsBetweenOpensOfSoberSpaces} below), we first introduce the following terminology:

\begin{defn}
\label{HomomorphismOfFramesOfOpens}\hypertarget{HomomorphismOfFramesOfOpens}{}
Let $(X,\tau_X)$ and $(Y,\tau_Y)$ be [[topological spaces]]. Then a function

\begin{displaymath}
\tau_X \longleftarrow \tau_Y \;\colon\; \phi
\end{displaymath}
between their [[frame of opens|sets of open subsets]] is called a \emph{[[frame]] [[homomorphism]]} if it preserves

\begin{enumerate}%
\item arbitrary [[unions]];


\item [[finite number|finite]] [[intersections]].



\end{enumerate}
In other words, $\phi$ is a frame homomorphism if

\begin{enumerate}%
\item for every [[set]] $I$ and every $I$-indexed set $\{U_i \in \tau_Y\}_{i \in I}$ of elements of $\tau_Y$, then

\begin{displaymath}
\phi\left(\underset{i \in I}{\cup} U_i\right) \;=\; \underset{i \in I}{\cup} \phi(U_i)\;\;\;\;\in \tau_X
  \,,
\end{displaymath}

\item for every [[finite set]] $J$ and every $J$-indexed set $\{U_j \in \tau_Y\}$ of elements in $\tau_Y$, then

\begin{displaymath}
\phi\left(\underset{j \in J}{\cap} U_j\right)
    \;=\;
  \underset{j \in J}{\cap} \phi(U_j)
  \;\;\;\;\in \tau_X
  \,.
\end{displaymath}


\end{enumerate}
\end{defn}
\begin{remark}
\label{PreservationOfInclusionsByFrameHomomorphism}\hypertarget{PreservationOfInclusionsByFrameHomomorphism}{}
A [[frame]] [[homomorphism]] $\phi$ as in def. \ref{HomomorphismOfFramesOfOpens} necessarily also preserves inclusions in that

\begin{itemize}%
\item for every inclusion $U_1 \subset U_2$ with $U_1, U_2 \in \tau_Y \subset P(Y)$ then

\begin{displaymath}
\phi(U_1) \subset \phi(U_2) \;\;\;\;\;\;\; \in \tau_X
  \,.
\end{displaymath}


\end{itemize}
This is because inclusions are witnessed by unions

\begin{displaymath}
(U_1 \subset U_2)
    \;\Leftrightarrow\;
  \left( U_1 \cup U_2 = U_2 \right)
\end{displaymath}
and by finite intersections:

\begin{displaymath}
(U_1 \subset U_2)
    \;\Leftrightarrow\;
  \left(
    U_1 \cap U_2 = U_1
  \right)
  \,.
\end{displaymath}
\end{remark}
\begin{example}
\label{}\hypertarget{}{}
For

\begin{displaymath}
f \;\colon\; (X,\tau_X) \longrightarrow (Y, \tau_Y)
\end{displaymath}
a [[continuous function]], then its function of [[pre-images]]

\begin{displaymath}
\tau_X \longleftarrow \tau_Y \;\colon\; f^{-1}
\end{displaymath}
is a frame homomorphism according to def. \ref{HomomorphismOfFramesOfOpens}.

\end{example}
For sober topological spaces the converse holds:

\begin{prop}
\label{FrameMorphismsBetweenOpensOfSoberSpaces}\hypertarget{FrameMorphismsBetweenOpensOfSoberSpaces}{}
If $(X,\tau_X)$ and $(Y,\tau_Y)$ are [[sober topological spaces]], then for every frame homomorphism (def. \ref{HomomorphismOfFramesOfOpens})

\begin{displaymath}
\tau_X \longleftarrow \tau_Y \;\colon\; \phi
\end{displaymath}
there is a unique [[continuous function]] $f \colon X \to Y$ such that $\phi$ is the function of forming [[pre-images]] under $f$:

\begin{displaymath}
\phi = f^{-1}
  \,.
\end{displaymath}
\end{prop}
We prove this \hyperlink{ProofOfFrameMorphismsBetweenOpensOfSoberSpaces}{below}, after the following lemma.

Let $\ast = (\{1\}, \tau_\ast = \left\{\emptyset, \{1\}\right\})$ be the [[point]] [[topological space]].

\begin{lemma}
\label{FrameHomomorphismsToPointAreIrrClSub}\hypertarget{FrameHomomorphismsToPointAreIrrClSub}{}
For $(X,\tau)$ a [[topological space]], then there is a [[bijection]] between the [[irreducible closed subspaces]] of $(X,\tau)$ and the [[frame]] [[homomorphisms]] from $\tau_X$ to $\tau_\ast$, given bys

\begin{displaymath}
\itexarray{
    Hom_{Frame}(\tau_X, \tau_\ast) 
      &\underoverset{\simeq}{}{\longrightarrow}&
    IrrClSub(X)
    \\
    \phi 
      &\mapsto& 
    X \backslash U_\emptyset(\phi)
  }
\end{displaymath}
where $U_\emptyset(\phi)$ is the [[union]] of all elements $U \in \tau_x$ such that $\phi(U) = \emptyset$:

\begin{displaymath}
U_{\emptyset}(\phi)
    \coloneqq
  \underset{{U \in \tau_X} \atop {\phi(U) = \emptyset} }{\cup}
   U
  \,.
\end{displaymath}
\end{lemma}
See also ([[Stone Spaces|Johnstone 82, II 1.3]]).

\begin{proof}
First we need to show that the function is well defined in that given a frame homomorphism $\phi \colon \tau_X \to \tau_\ast$ then $X \backslash U_\emptyset(\phi)$ is indeed an irreducible closed subspace.

To that end observe that:

$(\ast)$ \emph{If there are two elements $U_1, U_2 \in \tau_X$ with $U_1 \cap U_2 \subset U_{\emptyset}(\phi)$ then $U_1 \subset U_{\emptyset}(\phi)$ or $U_2 \subset U_{\emptyset}(\phi)$.}

This is because

\begin{displaymath}
\begin{aligned}
    \phi(U_1) \cap \phi(U_2)
    & =
    \phi(U_1 \cap U_2)
    \\
    & \subset \phi(U_{\emptyset}(\phi))
    \\
    & =
    \emptyset
  \end{aligned}
  \,,
\end{displaymath}
where the first equality holds because $\phi$ preserves finite intersections by def. \ref{HomomorphismOfFramesOfOpens}, the inclusion holds because $\phi$ respects inclusions by remark \ref{PreservationOfInclusionsByFrameHomomorphism}, and the second equality holds because $\phi$ preserves arbitrary unions by def. \ref{HomomorphismOfFramesOfOpens}. But in $\tau_\ast = \{\emptyset, \{1\}\}$ the intersection of two open subsets is empty precisely if at least one of them is empty, hence $\phi(U_1) = \emptyset$ or $\phi(U_2) = \emptyset$. But this means that $U_1 \subset U_{\emptyset}(\phi)$ or $U_2 \subset U_{\emptyset}(\phi)$, as claimed.

Now according to \href{irreducible+closed+subspace#OpenSubsetVersionOfClosedIrreducible}{this prop.}, the condition $(\ast)$ identifies the [[complement]] $X \backslash U_{\emptyset}(\phi)$ as an [[irreducible closed subspace]] of $(X,\tau)$.

Conversely, given an irreducible closed subset $X \backslash U_0$, define $\phi$ by

\begin{displaymath}
\phi
    \;\colon\;
  U
    \mapsto
  \left\{
    \itexarray{
      \emptyset & \vert \, \text{if} \, U \subset U_0
      \\
      \{1\} & \vert \, \text{otherwise}
    }
  \right.
  \,.
\end{displaymath}
This does preserve

\begin{enumerate}%
\item arbitrary unions

because $\phi(\underset{i}{\cup} U_i) = \{\emptyset\}$ precisely if $\underset{i}{\cup}U_i \subset U_0$ which is the case precisely if all $U_i \subset U_0$, which means that all $\phi(U_i) = \emptyset$ and because $\underset{i}{\cup}\emptyset = \emptyset$;

while $\phi(\underset{i}{\cup}U_1) = \{1\}$ as soon as one of the $U_i$ is not contained in $U_0$, which means that one of the $\phi(U_i) = \{1\}$ which means that $\underset{i}{\cup} \phi(U_i) = \{1\}$;


\item finite intersections

because if $U_1 \cap U_2 \subset U_0$, then by $(\ast)$ $U_1 \in U_0$ or $U_2 \in U_0$, whence $\phi(U_1) = \emptyset$ or $\phi(U_2) = \emptyset$, whence with $\phi(U_1 \cap U_2) = \emptyset$ also $\phi(U_1) \cap \phi(U_2) = \emptyset$;

while if $U_1 \cap U_2$ is not contained in $U_0$ then neither $U_1$ nor $U_2$ is contained in $U_0$ and hence with $\phi(U_1 \cap U_2) = \{1\}$ also $\phi(U_1) \cap \phi(U_2) = \{1\} \cap \{1\} = \{1\}$.



\end{enumerate}
Hence this is indeed a frame homomorphism $\tau_X \to \tau_\ast$.

Finally, it is clear that these two operations are inverse to each other.

\end{proof}
\begin{proof}
of prop. \ref{FrameMorphismsBetweenOpensOfSoberSpaces}

We first consider the special case of frame homomorphisms of the form

\begin{displaymath}
\tau_\ast \longleftarrow \tau_X \;\colon\; \phi
\end{displaymath}
and show that these are in bijection to the underlying set $X$, identified with the continuous functions $\ast \to (X,\tau)$.

By lemma \ref{FrameHomomorphismsToPointAreIrrClSub}, the frame homomorphisms $\phi \colon \tau_X \to \tau_\ast$ are identified with the irreducible closed subspaces $X \backslash U_\emptyset(\phi)$ of $(X,\tau_X)$. Therefore by assumption of [[sober topological space|sobriety]] of $(X,\tau)$ there is a unique point $x \in X$ with $X \backslash U_{\emptyset} = Cl(\{x\})$. In particular this means that for $U_x$ an open neighbourhood of $x$, then $U_x$ is not a subset of $U_\emptyset(\phi)$, and so it follows that $\phi(U_x) = \{1\}$. In conclusion we have found a unique $x \in X$ such that

\begin{displaymath}
\phi
    \;\colon\;
  U \mapsto
  \left\{
    \itexarray{
      \{1\} & \vert \,\text{if}\, x \in U
      \\
      \emptyset & \vert \, \text{otherwise}
    }
  \right.
  \,.
\end{displaymath}
This is precisely the [[inverse image]] function of the continuous function $\ast \to X$ which sends $1 \mapsto x$.

Hence this establishes the bijection between frame homomorphisms of the form $\tau_\ast \longleftarrow \tau_X$ and continuous functions of the form $\ast \to (X,\tau)$.

With this it follows that a general frame homomorphism of the form $\tau_X \overset{\phi}{\longleftarrow} \tau_Y$ defines a function of sets $X \overset{f}{\longrightarrow} Y$ by [[composition]]:

\begin{displaymath}
\itexarray{
    X &\overset{f}{\longrightarrow}& Y
    \\
    (\tau_\ast \leftarrow \tau_X)
    &\mapsto&
    (\tau_\ast \leftarrow \tau_X \overset{\phi}{\longleftarrow} \tau_Y)
  }
  \,.
\end{displaymath}
By the previous analysis, an element $U_Y \in \tau_Y$ is sent to $\{1\}$ under this composite precisely if the corresponding point $\ast \to X \overset{f}{\longrightarrow} Y$ is in $U_Y$, and similarly for an element $U_X \in \tau_X$. It follows that $\phi(U_Y) \in \tau_X$ is precisely that subset of points in $X$ which are sent by $f$ to elements of $U_Y$, hence that $\phi = f^{-1}$ is the [[pre-image]] function of $f$. Since $\phi$ by definition sends open subsets of $Y$ to open subsets of $X$, it follows that $f$ is indeed a continuous function. This proves the claim in generality.

\end{proof}
\hypertarget{Reflection}{}\subsubsection*{{Soberification reflection}}\label{Reflection}

The [[category]] of sober spaces is [[reflective subcategory|reflective]] in the category of all topological spaces; the [[left adjoint]] is called the \textbf{soberification}.

This reflection is also induced by the [[idempotent adjunction]] between spaces and [[locales]]; thus sober spaces are precisely those spaces that are the spaces of points of some [[locale]], and the [[category]] of sober spaces is [[equivalence of categories|equivalent]] to the category of [[locales with enough points]].

We now say this in detail.

Recall again the [[point]] topological space $\ast \coloneqq ( \{1\}, \tau_\ast = \left\{ \emptyset, \{1\}\right\} )$.

\begin{defn}
\label{SoberificationConstruction}\hypertarget{SoberificationConstruction}{}
Let $(X,\tau)$ be a [[topological space]].

Define $S X$ to be the set

\begin{displaymath}
S X \coloneqq Hom_{Frame}( \tau_X, \tau_\ast )
\end{displaymath}
of [[frame]] [[homomorphisms]] from the [[frame of opens]] of $X$ to that of the point. Define a [[topological space|topology]] $\tau_{S X} \subset P(S X)$ on this set by declaring it to have one element $\tilde U$ for each element $U \in \tau_X$ and given by

\begin{displaymath}
\tilde U
    \;\coloneqq\;
  \left\{
    \phi \in S X
    \,\vert\,
    \phi(U) = \{1\}
  \right\}
  \,.
\end{displaymath}
Consider the function

\begin{displaymath}
\itexarray{
    X &\overset{s_X}{\longrightarrow}& S X
    \\
    x &\mapsto& (const_x)^{-1}
  }
\end{displaymath}
which sends an element $x \in X$ to the function which assigns [[inverse images]] of the [[constant function]] $const_x \;\colon\; \{1\} \to X$ on that element.

\end{defn}
\begin{lemma}
\label{SoberificationConstructionWellDefined}\hypertarget{SoberificationConstructionWellDefined}{}
The construction $(S X, \tau_{S X})$ in def. \ref{SoberificationConstruction} is a [[topological space]], and the function $s_X \colon X \to S X$ is a [[continuous function]]

\begin{displaymath}
s_X \colon (X, \tau_X) \longrightarrow (S X, \tau_{S X})
\end{displaymath}
\end{lemma}
\begin{proof}
To see that $\tau_{S X} \subset P(S X)$ is closed under arbitrary unions and finite intersections, observe that the function

\begin{displaymath}
\itexarray{
    \tau_X &\overset{\widetilde{(-)}}{\longrightarrow}& \tau_{S X}
    \\
    U &\mapsto& \tilde U
  }
\end{displaymath}
in fact preserves arbitrary unions and finite intersections. Whith this the statement follows by the fact that $\tau_X$ is closed under these operations.

To see that $\widetilde{(-)}$ indeed preserves unions, observe that (e.g. \hyperlink{Johnstone82}{Johnstone 82, II 1.3 Lemma})

\begin{displaymath}
\begin{aligned}
    p \in \underset{i \in I}{\cup} \widetilde{U_i} \;
    & \Leftrightarrow
    \underset{i \in I}{\exists} p(U_i) = \{1\}
    \\
    & \Leftrightarrow \underset{i \in I}{\cup} p(U_i) = \{1\}
    \\
    & \Leftrightarrow p\left(\underset{i \in I}{\cup} U_i\right) = \{1\}
    \\
    & \Leftrightarrow p \in \widetilde{ \underset{i \in I}{\cup} U_i }
  \end{aligned}
  \,,
\end{displaymath}
where we used that the frame homomorphism $p \colon \tau_X \to \tau_\ast$ preserves unions. Similarly for intersections, now with $I$ a [[finite set]]:

\begin{displaymath}
\begin{aligned}
    p \in \underset{i \in I}{\cap} \widetilde{U_i} \;
    & \Leftrightarrow
    \underset{i \in I}{\forall} p(U_i) = \{1\}
    \\
    & \Leftrightarrow \underset{i \in I}{\cap} p(U_i) = \{1\}
    \\
    & \Leftrightarrow p\left(\underset{i \in I}{\cap} U_i\right) = \{1\}
    \\
    & \Leftrightarrow p \in \widetilde{ \underset{i \in I}{\cap} U_i }
  \end{aligned}
  \,,
\end{displaymath}
where now we used that the frame homomorphism $p$ preserves finite intersections.

To see that $s_X$ is continuous, observe that $s_X^{-1}(\tilde U) = U$, by construction.

\end{proof}
\begin{lemma}
\label{UnitIntoSXDetectsT0AndSoberity}\hypertarget{UnitIntoSXDetectsT0AndSoberity}{}
For $(X, \tau_X)$ a [[topological space]], the function $s_X \colon X \to S X$ from def. \ref{SoberificationConstruction} is

\begin{enumerate}%
\item an [[injection]] precisely if $X$ is [[separation axiom|T0]];


\item a [[bijection]] precisely if $X$ is sober.

In this case $s_X$ is in fact a [[homeomorphism]].



\end{enumerate}
\end{lemma}
\begin{proof}
By lemma \ref{FrameHomomorphismsToPointAreIrrClSub} there is an identification $S X \simeq IrrClSub(X)$ and via this $s_X$ is identified with the map $x \mapsto Cl(\{x\})$.

Hence the second statement follows by definition, and the first statement by \href{separation+axioms#T0InTermsOfClosureOfPoints}{this prop.}.

That in the second case $s_X$ is in fact a homeomorphism follows from the definition of the opens $\tilde U$: they are identified with the opens $U$ in this case (\ldots{}expand\ldots{}).

\end{proof}
\begin{lemma}
\label{SoberificationIsIndeedSober}\hypertarget{SoberificationIsIndeedSober}{}
For $(X,\tau)$ a [[topological space]], then the topological space $(S X, \tau_{S X})$ from def. \ref{SoberificationConstruction}, lemma \ref{SoberificationConstructionWellDefined} is sober.

\end{lemma}
(e.g. \hyperlink{Johnstone82}{Johnstone 82, lemma II 1.7})

\begin{proof}
Let $S X \backslash \tilde U$ be an [[irreducible closed subspace]] of $(S X, \tau_{S X})$. We need to show that it is the [[topological closure]] of a unique element $\phi \in S X$.

Observe first that also $X \backslash U$ is irreducible.

To see this use \href{irreducible+closed+subspace#OpenSubsetVersionOfClosedIrreducible}{this prop.}, saying that irreducibility of $X \backslash U$ is equivalent to $U_1 \cap U_2 \subset U \Rightarrow (U_1 \subset U) or (U_2 \subset U)$. But if $U_1 \cap U_2 \subset U$ then also $\tilde U_1 \cap \tilde U_2 \subset \tilde U$ (as in the \hyperlink{ProofOfSoberificationConstructionWellDefined}{proof} of lemma \ref{SoberificationConstructionWellDefined}) and hence by assumption on $\tilde U$ it follows that $\tilde U_1 \subset \tilde U$ or $\tilde U_2 \subset \tilde U$. By lemma \ref{FrameHomomorphismsToPointAreIrrClSub} this in turn implies $U_1 \subset U$ or $U_2 \subset U$. In conclusion, this shows that also $X \backslash U$ is irreducible .

By lemma \ref{FrameHomomorphismsToPointAreIrrClSub} this irreducible closed subspace corresponds to a point $p \in S X$. By that same lemma, this frame homomorphism $p \colon \tau_X \to \tau_\ast$ takes the value $\emptyset$ on all those opens which are inside $U$. This means that the [[topological closure]] of this point is just $S X \backslash \tilde U$.

This shows that there exists at least one point of which $X \backslash \tilde U$ is the topological closure. It remains to see that there is no other such point.

So let $p_1 \neq p_2 \in S X$ be two distinct points. This means that there exists $U \in \tau_X$ with $p_1(U) \neq p_2(U)$. Equivalently this says that $\tilde U$ contains one of the two points, but not the other. This means that $(S X, \tau_{S X})$ is [[separation axiom|T0]]. By \href{separation+axioms#T0InTermsOfClosureOfPoints}{this prop.} this is equivalent to there being no two points with the same topological closure.

\end{proof}
\begin{prop}
\label{}\hypertarget{}{}
For $(X, \tau_X)$ any [[topological space]], for $(Y,\tau_Y^{sob})$ a sober topological space, and for $f \colon (X, \tau_X) \longrightarrow (Y, \tau_Y)$ a [[continuous function]], then it factors uniquely through the soberification $s_X \colon (X, \tau_X) \longrightarrow(S X, \tau_{S X})$ from def. \ref{SoberificationConstruction}, lemma \ref{SoberificationConstructionWellDefined}

\begin{displaymath}
\itexarray{
    (X, \tau_X) &\overset{f}{\longrightarrow}& (Y, \tau_Y^{sob})
    \\
    {}^{\mathllap{s_X}}\downarrow & \nearrow_{\exists !}
    \\
    (S X , \tau_{S X})
  }
  \,.
\end{displaymath}
\end{prop}
\begin{proof}
By the construction in def. \ref{SoberificationConstruction}, we find that the outer part of the following square [[commuting square|commutes]]:

\begin{displaymath}
\itexarray{
    (X, \tau_X) &\overset{f}{\longrightarrow}& (Y, \tau^{sob}_Y)
    \\
    {}^{\mathllap{s_X}}\downarrow & \nearrow& \downarrow^{\mathrlap{s_{S X}}}
    \\
    (S X, \tau_{S X})
     &\underset{S f}{\longrightarrow}&
    (S S X, \tau_{S S X})
  }
  \,.
\end{displaymath}
By lemma \ref{SoberificationIsIndeedSober} and lemma \ref{UnitIntoSXDetectsT0AndSoberity}, the right vertical morphism $s_{S X}$ is an isomorphism (a [[homeomorphism]]), hence has an [[inverse morphism]]. This defines the diagonal morphism, which is the desired factorization.

To see that this factorization is unique, consider two factorizations $\tilde f, \overline{f} \colon \colon (S X, \tau_{S X}) \to (Y, \tau_Y^{sob})$ and apply the soberification construction once more to the triangles

\begin{displaymath}
\itexarray{
    (X, \tau_X) &\overset{f}{\longrightarrow}& (Y, \tau_Y^{sob})
    \\
    {}^{\mathllap{s_X}}\downarrow & \nearrow_{ \tilde f, \overline{f}}
    \\
    (S X , \tau_{S X})
  }
  \phantom{AAA}
    \mapsto
  \phantom{AAA}
  \itexarray{
    (S X, \tau_{S X}) &\overset{S f}{\longrightarrow}& (Y, \tau_Y^{sob})
    \\
    {}^{\simeq}\downarrow & \nearrow_{ \tilde f, \overline{f}}
    \\
    (S X , \tau_{S X})
  }
  \,.
\end{displaymath}
Here on the right we used again lemma \ref{UnitIntoSXDetectsT0AndSoberity} to find that the vertical morphism is an isomorphism, and that $\tilde f$ and $\overline{f}$ do not change under soberification, as they already map between sober spaces. But now that the left vertical morphism is an isomorphism, the commutativity of this triangle for both $\tilde f$ and $\overline{f}$ implies that $\tilde f = \overline{f}$.

\end{proof}
\hypertarget{enough_points}{}\subsubsection*{{Enough points}}\label{enough_points}

A topological space has enough points in the sense of def. \ref{EnoughPointsOfATopologicalSpace} if and only if its $T_0$ quotient is sober. The category of topological spaces with enough points is a [[reflective subcategory]] of the category [[Top]] of all topological spaces, and a topological space is [[T0]] iff this reflection is sober.

\hypertarget{examples_and_nonexamples}{}\subsection*{{Examples and Non-examples}}\label{examples_and_nonexamples}

\begin{itemize}%
\item With [[classical logic]], every [[Hausdorff space]] is sober, but this can fail [[constructive mathematics|constructively]]. See at \emph{[[Hausdorff implies sober]]}.

 Since the Hausdorff condition implies the $T_1$ [[separation axiom]], this means that ([[classical logic|classically]]) there is a large [[intersection]] of the [[classes]] of $T_1$-topological spaces and sober topological spaces. But neither class is contained in the other, as the following counter-examples show:

\begin{itemize}%
\item The [[Sierpinski space]] is sober, but not $T_1$.


\item The [[cofinite topology]] on a non-[[finite set]] is $T_1$ but not sober.



\end{itemize}

\item The topological space underlying any [[scheme]] is sober. See at \emph{[[schemes are sober]]}.



\end{itemize}
Further examples of spaces that are \emph{not} sober includes the following:

\begin{itemize}%
\item Any nontrivial [[indiscrete space]] is not sober, since it is not $T_0$.

\end{itemize}
More interestingly:

\begin{itemize}%
\item For $R$ a [[commutative ring]], then the space $R^2$ with the [[Zariski topology]] is $T_1$ but not sober, since every subvariety is an irreducible closed set which is not the [[topological closure|closure]] of a point. Its \emph{soberification} is, unsurprisingly, the [[scheme]] $Spec(R[x,y])$, which contains ``generic points'' whose closures are the subvarieties.

\end{itemize}
The following non-example shows that sobriety is not a hereditary separation property, i.e., [[topological subspaces]] of sober spaces need not be sober:

\begin{itemize}%
\item The [[Alexandroff topology]] on a [[poset]] is also not, in general, sober. For instance, if $P$ is the infinite binary tree (the set of finite $\{0,1\}$-words ([[lists]]) with the ``extends'' preorder), then the soberification of its Alexandroff topology is [[Wilson space]], the space of finite or infinite $\{0,1\}$-words ([[streams]]).

\end{itemize}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[nice topological space]]

\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item [[Francis Borceux]], volume 3, section 1.9 of \emph{[[Handbook of Categorical Algebra]]}, Cambridge University Press (1994)


\item [[Peter Johnstone]], section II.1, from II.1 on in \emph{[[Stone Spaces]]}, Cambridge Studies in Advanced Mathematics \textbf{3}, Cambridge University Press 1982. xxi+370 pp. \href{http://www.ams.org/mathscinet-getitem?mr=698074}{MR85f:54002}, reprinted 1986.


\item [[Saunders MacLane]], [[Ieke Moerdijk]], around definition IX.3.2 in \emph{[[Sheaves in Geometry and Logic]]}


\item Sober spaces in the \href{http://topology.jdabbs.com/properties/73}{$\pi$-base}.



\end{itemize}
[[!redirects sober]] [[!redirects sober topological space]] [[!redirects sober topological spaces]] [[!redirects sober topology]] [[!redirects sober topologies]] [[!redirects sober space]] [[!redirects sober spaces]]

[[!redirects sobrification]] [[!redirects sobrifications]]

[[!redirects soberification]] [[!redirects soberifications]]

[[!redirects sober reflection]] [[!redirects sober reflections]]

[[!redirects soberification reflection]] [[!redirects soberification reflections]]

[[!redirects topological space with enough points]] [[!redirects topological spaces with enough points]]



\end{document}