\documentclass{mscs}
\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{enumerate}
\usepackage{tikz}
\usetikzlibrary{arrows}
\newtheorem{theor}{Theorem}[section]
\newtheorem{lemma}[theor]{Lemma}
\newtheorem{propo}[theor]{Proposition}
\newtheorem{corollary}[theor]{Corollary}
\newtheorem{examp}[theor]{Example}
\newtheorem{definition}[theor]{Definition}
\newtheorem{remark}[theor]{Remark}
\newcommand{\powerspace}{\mathcal{P}}
\newcommand{\EM}{\mathrm{EM}}
\newcommand{\TEM}{\mathrm{TEM}}
\newcommand{\reals}{\mathbb{R}}
\DeclareMathOperator{\appr}{approx}
\DeclareMathOperator{\id}{id}
%\DeclareMathOperator{\sat}{sat}
\newcommand{\sqsem}{\sqsubseteq_\EM}
\newcommand{\sqstem}{\sqsubseteq_\TEM}
\newcommand{\cl}[1]{\overline{#1}}
\newcommand{\lens}[1]{\langle #1 \rangle}
\newcommand{\xlens}[2]{\langle #1 \rangle_{#2}}
\DeclareMathOperator{\Lens}{Lens}
%\newcommand{\lens}[1]{\widehat{#1}}
\renewcommand{\L}{\mathcal{L}}
\newcommand{\sat}{{\uparrow}}
%\newcommand{\Lens}[1]{\mathrm{Lens}(#1)}
\newcommand{\Haus}[1]{\mathcal{H}(#1)}
%\newcommand{\satu}[1]{\mathrm{sat}(#1)}
%\newcommand{\clos}[1]{\mathrm{cl}(#1)}
\newcommand{\nats}{\mathbb{N}}
\author[U. Berger, J. Blanck and P. K. K\o ber]
{U\ls L\ls R\ls I\ls C\ls H\ns B\ls E\ls R\ls G\ls E\ls R\(^1\),%
\ns J\ls E\ls N\ls S\ns B\ls L\ls A\ls N\ls C\ls K\(^1\)\ns and%
\ns P\ls E\ls T\ls T\ls E\ls R\ns K\ls R\ls I\ls S\ls T\ls I\ls A\ls N\ns K\ls \O\ls B\ls E\ls R$^2$\thanks{Funded by the Norwegian Research Council}\\
$^1$ Department of Computer Science, Swansea University, Singleton Park,
Swansea, SA2 8PP, Wales\addressbreak
$^2$ Department of Mathematics, University of Oslo, Pb.1053 Blindern, N-0316 Oslo, Norway }
\begin{document}
%\pagenumbering
\title{Domain Representations of Spaces of Compact Subsets}
\maketitle
%%% Abstract and Introduction
\begin{abstract}
We present a method for constructing
%
from a given domain representation
%
of a space $X$,
%
with underlying domain $D$,
%
a domain representation
%
of a subspace of compact subsets of $X$
%
%(with the Vietoris topology),
%
where the underlying domain is the Plotkin powerdomain of $D$.
%
We show that this operation is functorial over a category of domain
representations with a natural choice of morphisms.
%
We study the topological properties of the space of representable
compact sets
and isolate conditions under which all compact subsets of $X$ are
representable.
%
Special attention is paid to admissible representations
and representations of metric spaces.
%
\end{abstract}
\section{Introduction}
Scott domains~\cite{Scott70} provide denotational semantics for a wide
range of programming languages and carry a natural notion of
computability \cite{Ershov77}.
%
Using domain representations~\cite{Blanck00,ST95,ST08}, the domain-theoretic notion of
computability can be extended to a large class of topological
spaces, moreover, important classes of topological spaces can be
characterised by the kind of domain representations they
admit~\cite{Hamrin05}.
%
In addition to modelling computability, domains can be used to model
nondeterminism by means of powerdomains~\cite{GHKLMS}.
%
In this paper we extend Plotkin's powerdomain construction~\cite{Plotkin83}
(also known as the convex powerdomain)
to domain representations. This amounts to implementing an effective
notion of nondeterminism on a large class of topological spaces.
Here is a sketch of the construction:
%
A \emph{domain} in this paper will be a countably based algebraic cpo.
%
A {\em domain representation} of a
topological space $X$ is a pair $ (D,\delta)$ where $D$ is a domain, $D^R$ is
a subset of $D$ regarded as a topological space with the relativised Scott
topology, and $\delta : D^R \to X$ is a quotient map. For simplicity of
the sketch, let us assume that $D^R$ is upwards closed in the domain ordering
and $X$ is Hausdorff.
%
>From such a domain representation we construct the \emph{powerdomain
representation} $(\powerspace(D),\delta_\powerspace)$ where $\powerspace(D)$
is the Plotkin powerdomain. We use a result by Smyth~\cite{Smyth83} according
to which $\powerspace(D)$ can be modelled as the space of \emph{lenses}, i.e.\
nonempty compact subsets of $D$ which are the intersection of a closed and a
saturated set, with the Vietoris topology. The function $\delta_\powerspace :
\powerspace(D)^R \to \powerspace(X)$ is defined on $\powerspace(D)^R =
\{K\in\powerspace(D)| K\subseteq D^R\}$ by $\delta_\powerspace(K) :=
\delta[K]$. The \emph{powerspace} $\powerspace(X)$ is simply the image of
$\powerspace(D)^R$ under $\delta_\powerspace$ with the quotient topology. The
elements of $\powerspace(X)$ are certain non-empty compact subsets of $X$
which we call \emph{representable\/}.
%
Our main results can be summarised as follows:
%
\begin{enumerate}[(1)]
\item The construction of the powerdomain representation defines an
endofunctor on the category of domain representations.
%
\item The representable sets have good closure properties, and in many
interesting cases (e.g.\ retract representations, total continuous
functionals) all non-empty compact sets are representable (modulo $T_0$),
although this does not hold in general.
%
\item For admissible domain representations the powerspace is independent of
the representation and hence defines an operation on the topological spaces
admitting an admissible representation, i.e., on the class of
$qcb_0$-spaces.
%
\item Many properties of spaces and representations are preserved by the
powerdomain representation, for example, density, retract, Hausdorff,
$qcb_0$.
%
\item Representations of metric spaces lift to representations of the
powerspace with the Hausdorff metric. This generalises previous results
in~\cite{Blanck99}.
%
\end{enumerate}
Smyth's characterisation of the Plotkin powerdomain mentioned above
%
%which is in fact the $T_0$-collapse
%of the set of all non-empty compact subsets of $D$ with the Vietoris
%topology~\cite{Smyth83},
is crucial for our work. It allows us to render
most proofs very short and in general topological terms hardly ever
using domain-theoretic arguments. Applying the $T_0$-collapse not
only to the representing domain, but also to the represented space,
allows us to smoothly include non-Hausdorff spaces $X$ in our construction.
Although we do not discuss computability aspects explicitely
it is clear from the constructions and proofs that all
results hold effectively.
%
The closure properties of representable compact sets hold effectively,
and so does the lifting of metric spaces.
%
Furthermore, the Plotkin powerdomain construction preserves
effectivity,
%
and the coincidence of the Scott topology and the Vietoris topology on
the Plotkin powerdomain is given by computable transformations of the
respective basic open sets.
The plan of the paper is as follows:
%
In section~2 we introduce the basic notions of domain theory and
topology which we will use. In section~3 we look at some important
results concerning operations on lenses
which will be useful at a later stage.
Then, in section~4, we present our construction of the
powerdomain representation
and study some basic preservation properties.
The powerdomain representation gives us a natural notion of a
representable compact subset of a topological space, given a domain
representation of it, and more generally a representable lens. We
study this notion in more detail in section~5. In section~6, we investigate
what topological properties of the represented space are preserved
by our construction. Finally, in section~7, we look at the important
case of a domain representation of a complete metric space.
% \section{Introduction}
% Domain representations are used for studying computability on a
% large class of topological spaces. Important classes of topological spaces can
% be characterised by the kind of domain representations they admit.
% In domain theory, non-determinism is modelled by means of powerdomains.
% For a countably based domain, the Plotkin powerdomain has a useful characterisation
% as a partial order of certain compact subsets of the domain and there are similar
% topological characterisations of the Hoare and Smyth powerdomains, see \cite{
% AJ,GHKLMS}. A more general topological account of this is given in \cite{Smyth83}.
% Our initial motivation for this work was to study possible generalisations of the
% powerdomain construction to topological spaces with domain representations, in
% particular the $T_0$ topological quotients of countably based spaces ($ qcb_0$
% spaces). The idea is to represent non-determinism
% using the connection between topological spaces and domain representations.
% Most spaces we encounter in analysis satisfy stronger separation axioms than $T_0$,
% and from this point of view the Plotkin powerdomain is the most useful of the three,
% and the one we will focus on.
% In the case of a standard representation of a complete, separable metric space over
% a domain $ D$, a domain representation of a metric space of non-empty compact subsets
% has been studied previously, see \cite{Blanck99}.
% %Our construction will be a generalisation of this.
% Compact subsets of a topological space play a crucial in the study of powerspaces.
% Of course, compactness is a more general notion once we drop the Hausdorff separation
% axiom, and for $T_0 $ spaces the natural concept turns out to be that of lens. The
% Vietoris topology is a natural topology on a space of lenses.
% In section~2 we introduce the basic notions of domain theory and topology which we will
% use.
% In section~3 we look at some important results concerning lenses, which will be useful
% at a later stage.
% Then, in section~4, we present the construction of a domain representation over the
% Plotkin powerdomain over $D$, given a domain representation over $D$, and study some basic
% preservation properties.
% The powerdomain representation gives us a natural notion of a representable compact subset
% of a Hausdorff space, given a domain representation of it, and more generally a representable
% lens, and we study this notion in more detail in section~5.
% In section~6, we look at what topological properties of the represented space is preserved by
% our construction.
% Finally, in section~7, we look at the important case of a domain representation of a complete
% metric space.
\section{Background}
\subsection{Basic domain theory}
It is well-known that domains (i.e.\ countably based algebraic cpos)
are closed under Plotkin's power domain
construction. Restricting further to the class of sfp-domains would
give Cartesian closure, but this is not used in the paper.
%
The restriction to countably based domains is useful for
characterising the elements of the power domain. For background
material on domains we refer to \cite{AJ,GHKLMS,SHLG}.
\subsection{Domain representations}
Some basic definitions. We refer to \cite{Blanck00,ST08} for more on
domain representations.
A {\em domain with totality} is a pair $ (D , D^{R} ) $, with $ D$ a
domain (with the Scott topology) and $ D^{R} $ a subspace of the
domain (with the subspace topology). A {\em domain representation} is
a pair $ (D, \delta : D^{R} \rightarrow X ) $ such that $ (D, D^{R} )
$ is a domain with totality, $ X $ a topological space and $ \delta $
is a quotient map. The representation $ (D, \delta ) $ is {\em dense}
if $ D^{R} $ is topologically dense in $D$.
Let $ ( D, \delta : D^{R} \to X ) $ and $ ( E, \varepsilon : E^{R} \to Y ) $
be domain representations. A {\em representation morphism} (or a $( \delta ,
\varepsilon )$-total map)
\[ f : ( D, \delta ) \to ( E, \varepsilon ) \] is a continuous map $ f : D \to
E $
%
\begin{equation*}
\begin{tikzpicture}[->,yscale=1.2]
\path (0,0) node (x) {$X$} (2,0) node (y) {$Y$};
\path (0,1) node (dr) {$D^R$} (2,1) node (er) {$E^R$};
\path (0,2) node (d) {$D$} (2,2) node (e) {$E$};
\draw (dr) -- node[left] {$\delta$} (x) ;
\draw[right hook->] (dr) -- node[left] {$\iota$} (d);
\draw (er) -- node[right] {$\epsilon$} (y);
\draw[right hook->] (er) -- node[right] {$\iota$} (e);
\draw (d) -- node[above] {$f$} (e);
\draw (dr) -- node[above] {$f|_{D^R}$} (er);
\draw (x) -- node[above] {$g$} (y);
\end{tikzpicture}
\end{equation*}
such that
\begin{enumerate}[(i)]
\item
$ f [ D^{R} ] \subseteq E^{R} $; and
\item
$ \delta (x) = \delta (y) \Rightarrow \varepsilon (f (x) ) =
\varepsilon (f (y)) $ for all $ x, y \in D^{R} $.
\end{enumerate}
The representation morphism induces a unique continuous function $ g : X \to Y $ which satisfies $ g \circ \delta = \varepsilon \circ f|_{ D^{R}} $.
%
% Domain representations and representation morphisms for a category.
% It is easy to see that if the category of domains used
% is cartesian closed, then so is the corresponding category
% of domain representations.
% {\bf Seems clear to me. Has this been done before? Of course, the
% product and exponential is usually not the ordinary
% topological product on the represented spaces (see e.g.
% the total continuous functionals). Do the admissible representations
% form a cartesian closed subcategery?}
A domain representation $ (D, \delta ) $ is {\em retract} if there
exists a continuous $ s : X \to D^{R} $ such that $ \delta \circ s =
\id_{X} $. A topological space has a dense, retract representation if
and only if it is a second countable $T_{0} $ space~\cite{Blanck00}.
A domain representation $ (E, \varepsilon ) $ of $X$ is {\em
admissible} if for every domain with dense totality $ (D, D^{R} ) $
and continuous function $ \varphi: D^{R} \rightarrow X $, there exists
a continuous map $ \hat{\varphi } : D \to E $ such that $ \hat{\varphi
} [ D^{R} ] \subseteq E^{R} $ and $ \varepsilon ( \hat{\varphi } (x))
= \varphi (x) $ for every $ x \in D^{R} $ \cite{Hamrin05}.
>From a given admissible domain representation of $X$ one can easily
construct an admissible representation over a consistently complete
domain. Moreover, an admissible representation can be chosen to be
dense. A topological space $X$ has a dense admissible representation if and
only if it is a sequential $T_{0} $ space with a countable pseudobase \cite{
Hamrin05}, which again is equivalent to $X$ being a $ qcb_{0} $ space \cite{
Schroder03}.
Let \((D, \delta)\) and \((E, \epsilon)\) be domain representations of a space
\(X\). A \emph{continuous reduction} of \((D, \delta)\) to \((E, \epsilon)\)
is a continuous map \(f : D \to E\) that induces the identity on
\(X\). Continuous reductions induce a preorder on domain representations. The
notion of admissible domain representation is equivalent to being largest
among dense domain representations with respect to the preorder of continuous
reductions. This characterisation of admissibility also holds for other
classes of representations, such as TTE~\cite{Weihrauch00}
representations. The retract property is preserved by continuous
reductions. This means that the retract property also is a notion of largeness
under continuous reductions. Among domain representations, there is a close
but subtle connection between retract representations and admissible
representations~\cite{Blanck08}. Retract domain representations of spaces are
an important and common type of representations, and, as we will see, our
power space construction preserves the retract property.
\subsection{Topology and the specialisation order}
Let $X = (X, \tau)$ be a topological space. The \emph{specialisation order}, \(\le\), on
\(X\) is given by
\begin{equation*}
x \le y \iff (\forall U \in \tau)(x \in U \Rightarrow y \in U).
\end{equation*}
It is easy to see that the specialisation order is a preorder. If \(X\) is
\(T_0\), then the specialisation order is antisymmetric and therefore
a partial order. If \(X\) is \(T_1\), then the
specialisation order is discrete, i.e., \(x \le y \Rightarrow x = y\). For a
domain the specialisation order, \(\le\), coincides with the domain ordering,
\(\sqsubseteq\).
Let \(A \subseteq X\). We define the \emph{upper} and \emph{lower set}
with respect to the specialisation order by
\begin{align*}
{\uparrow}A &= \{x \in X : (\exists a \in A) (a \le x)\}, \mbox{ and}\\
{\downarrow}A &= \{x \in X : (\exists a \in A) (x \le a)\}.
\end{align*}
Note that an open set must be an upper set and a closed set must be a
lower set, with respect to the specialisation order.
The \emph{topological saturation} of $A$, i.e., the
intersection of all open neighbourhoods of $A$, coincides with \(\sat A\). The
\emph{topological closure}, i.e., the intersection of all closed sets
containing \(A\), is denoted by $ \cl{A } $. We have \({\downarrow} A
\subseteq \cl A\), but this may, in general, be a strict inclusion.
By \(\mathcal{H}(X)\) we denote the set of non-empty compact subsets of \(X\).
A {\em lens} is a non-empty subset of $ X$ which can be written as the
intersection of a closed set and a compact saturated set. A lens $ L
\subseteq X $ is itself compact and has a canonical representation of the form
$ L = \cl{L} \cap \sat L $. Let $ \Lens (X) $ be the set of lenses in
$X$. Clearly, \(\Lens(X) \subseteq \mathcal{H}(X)\), and equality
holds if $ X$ is a $T_1$ space.
For a non-empty compact $K \subseteq X $, we define the {\em lens closure} of
$K $ as the set $ \cl{K} \cap \sat K $, and we denote it by $ \xlens{K}X
$. Clearly, lens closure is an operator \(\xlens\cdot X : \mathcal{H}(X) \to
\Lens(X)\). The lens closure $ \xlens{K}X $ is the smallest lens containing
$K$, and in particular $ \xlens{\xlens{K}X}X = \xlens{K}X $. If $X$ is $T_1$,
then $\xlens{K}X = K$.
%
For a non-empty finite (and hence compact) set $A$ we have
$\xlens{A}X={\downarrow}A \cap {\uparrow} A =$ the least convex
set containing $A$.
%
%A set \(A \subseteq X\) is {\em convex} if $ A = {\downarrow}
%A \cap {\uparrow} A $. The {\em convex closure} of $ A $ is the smallest
%convex set containing $A$, and if $A$ is finite it coincides with $ \xlens{A}X
%$. Lenses are always convex.
Let \(A\) and \(B\) be non-empty subsets of \(X\).
The {\em Egli-Milner (pre)ordering} is defined by
\[ A \sqsem B \Leftrightarrow A \subseteq {\downarrow} B \wedge B \subseteq
{\uparrow} A .\] Finite sets $ A$ and $ B$ are equivalent w.r.t. $ \sqsem $
if and only if $\xlens{A}X = \xlens{B}X $.
The {\em topological Egli-Milner (pre)ordering} is defined by
\[ A \sqstem B \Leftrightarrow A \subseteq \cl{ B} \wedge B \subseteq \sat A
.\] Arbitrary non-empty compact sets $ A$ and $ B $ are equivalent w.r.t. $ \sqstem $ if
and only if $\xlens{A}X = \xlens{B}X $.
\subsection{Vietoris topology}
% Let $ D $ be a countably based domain with the Scott topology.
% The {\em Plotkin powerdomain} over $ D$, denoted by $\powerspace (D) $, is the
% ideal completion of $ (\wp^\ast_{\mathrm f} (D_{c} ) ,\allowbreak \sqsem) $.
% The compact elements of $\powerspace (D) $ can be identified with the equivalence classes of finite sets of $ D_{c} $.
% As with all domains, when a powerdomain is considered as a topological space
% the topology is assumed to be the Scott topology.
Let \(X\) be a topological space. If $ U \subseteq X $ is open, let $ U_{
\cap} $ be the set of compacts $ K \subseteq X $ with $ K \cap U \neq
\emptyset $ and let $ U_{ \supseteq} $ be the set of non-empty compacts $ K
\subseteq X $ with $ K \subseteq U $. The {\em Vietoris topology} on $
\mathcal{H} (X) $ is the topology generated by subbasic open sets $ U_{ \cap}
$ and $ U_{ \supseteq} $ for all open $ U \subseteq X $.
We consider $\Haus{X}$ as a topological space with the Vietoris topology, and
$\Lens(X)$ as a subspace of $\Haus{X}$.
\begin{lemma}\label{lemma-lens}
The space $\Lens(X)$ is the $T_0$-collapse of $\Haus{X}$
via the collapsing map $\xlens{\cdot}X$.
\end{lemma}
\begin{proof}
If \(K_1\) and \(K_2\) have the same set of subbasic neighbourhoods of the
form \(U_\cap\), then \(\cl{K_1} = \cl{K_2}\). If \(K_1\) and \(K_2\) have
the same subbasic neighbourhoods of the form \(U_\supseteq\), then \(\sat
K_1 = \sat K_2\). Thus, if \(K_1\) and \(K_2\) are indistinguishable in the
Vietoris topology, then \(\xlens{K_1}X= \xlens{K_2}X\).
We have \(\xlens{K}X \in U_\cap \iff K \in U_\cap\) since \(\xlens{K}X \subseteq
\cl{K}\), furthermore \(\xlens{K}X \in U_\supseteq \iff K \in U_\supseteq\)
since \(\xlens{K}X \subseteq \sat K\). So \(K\) and \(\xlens{K}X\) are
indistinguishable in the Vietoris topology. Thus, if \(\xlens{K_1}X =
\xlens{K_2}X\) then \(K_1\) and \(K_2\) are indistinguishable since they are
both indistinguishable from their common lens closure.
\end{proof}
\begin{lemma} \label{lemma-lenshaus}
Let $ X $ be a Hausdorff space.
Then $ \Haus{X} = \Lens(X) $ is a Hausdorff space.
\end{lemma}
\begin{proof}
Choose non-empty compact subsets $ K_1, K_2 \subseteq X $ and
assume $ K_2 \setminus K_1 \neq \emptyset$.
Choose $ x \in K_2 \setminus K_1 $. Since $ X$ satisfies
the Hausdorff separation axiom, there are
disjoint open neighbourhoods $ U $ and $ V$ of $
x $ and $K_1$, respectively. Then $ K_2 \in U_\cap $ and $ K_1 \in
V_\supseteq $, and $ U_\cap $ and $ V_\supseteq $ are disjoint
since $ U $ and $V$ are disjoint.
\end{proof}
\section{More on lenses}
Our interest in spaces of lenses is the following characterisation of the
Plotkin powerdomain as a space of lenses.
Let \(D\) be a domain, and recall that we have assumed that our domains are
countably based. Hence, by a result of Smyth~\cite[Theorem 3]{Smyth83} we may
identify the Plotkin powerdomain \(\powerspace(D)\) with the topological space
\(\Lens(D)\). We will use both notations depending on context. The
specialisation order on \(\Lens(D)\) is \(\sqstem\). The compact elements of
the powerdomain are lenses generated by finite sets.
Although we will apply the results of this section to domains only, we have
chosen to present the fully general situation here.
\subsection{Functoriality of $\mathcal{H}(\cdot)$ and $\Lens(\cdot)$}
If $ f :X \to Y $ is continuous, let $ f_{\mathcal{H}} $ be the map which
sends a non-empty compact set $K \subseteq X $ to the non-empty compact set $ f[K] \subseteq Y $.
\begin{lemma} \label{lemma-fhmon}
\begin{enumerate}[(i)]
\item The function $ f_{\mathcal{H}} : ( \mathcal{H} (X) ; \sqstem) \to (
\mathcal{H} (Y) ; \sqstem) $ is monotone.
\item In particular, for every $ K \in \mathcal{H} (K) $, we have $
\xlens{f[K] }Y = \xlens{ f[\xlens{K}X] }Y $.
\end{enumerate}
\end{lemma}
\begin{proof}
(ii) follows from the (i) since $\xlens{K}X \equiv_{\TEM} K$.
Assume \(K \sqstem K'\). Let \(U \subseteq Y\) be an open set containing
\(f(x)\) for some \(x \in K\). By assumption, \(K \subseteq \cl{K'}\), so
\(f^{-1}[U]\) intersects the closure \(\cl{K'}\) and therefore also
\(K'\). Hence, \(f[K] \subseteq \cl{f[K']}\). To show that \(f[K'] \subseteq
\sat f[K] \) we show that every open neighbourhood of $ f[K] $
contains $f[K'] $. Let $ U \supseteq f[K] $ be open. Then $ f^{-1} [U]
\supseteq K $ is open, and therefore $ f^{-1} [U] \supseteq K' $. Thus, $ U \supseteq
f[K'] $. We have shown \(f[K] \sqstem f[K']\).
\end{proof}
%
% $K \subseteq \cl (K') \Rightarrow f[K] \subseteq \cl (f [K'] ) $: Assume $K
% \subseteq \cl (K') $ and let $ y = f(x) $ for some $ x \in K$. We show that
% every open neighbourhood of $ y $ intersects $ f[K'] $. If $ U $
% is open and $ y \in U $, then $ f^{-1} [U] $ is an open neighbourhood
% of $x$ and therefore intersects $ K'$. Hence $U$ intersects $f[K']$.
% $K' \subseteq \sat (K) \Rightarrow f[K'] \subseteq \sat (f [K] ) $: Assume
% $K' \subseteq \sat (K) $. We show that every open neighbourhood of $ f[K] $
% contains $f[K'] $. Let $ U \supseteq f[K] $ be open. Then $ f^{-1} [U]
% \supseteq K $ is open, and $ f^{-1} [U] \supseteq K' $. Thus, $ U \supseteq
% f[K'] $.
Let \(f : X \to Y\) be a continuous map. We define the lifting of \(f\) to the
lens spaces, $ f_\L : \Lens(X)\to \Lens(Y) $, by $ f_\L (L) = \xlens{ f[L] }Y $.
\begin{lemma} \label{lemma-fpcomp}
%
$ \id_\L = \id $ and $ (g \circ f)_\L = g_\L \circ f_\L $, where \(f : X \to
Y\) and \(g : Y \to Z\).
%
\end{lemma}
\begin{proof}
%
The first assertion is obvious.
%
For the second, let $L\in\Lens(X)$. By Lemma~\ref{lemma-fhmon}(ii) we have
%
$ (g \circ f)_\L(L) = \xlens{g[f[L]]}Z = \xlens{g[\xlens{f[L]}Y]}Z =
(g_\L \circ f_\L)(L)$.
%
\end{proof}
The next two results imply that $f_\L$ is continuous.
\begin{propo} \label{proposition-fhcont}
%
$f_{\mathcal{H}} : \mathcal{H}(X)\to\mathcal{H}(Y)$ is continuous.
%
\end{propo}
\begin{proof}
%
We show that $(f_{\mathcal{H}})^{-1}$ maps Vietoris basic opens in $Y$
to Vietoris basic opens in $X$.
Let $U\subseteq Y$ be open. Clearly,
$U\cap f[K]\neq\emptyset$ iff $f^{-1}[U]\cap K\neq\emptyset$,
and $U\supseteq f[K]$ iff $f^{-1}[U]\supseteq K$. Therefore,
$(f_{\mathcal{H}})^{-1}[U_{\cap}] = (f^{-1}[U])_{\cap}$
and $(f_{\mathcal{H}})^{-1}[U_{\supseteq}] = (f^{-1}[U])_{\supseteq}$.
%
\end{proof}
We consider $\Lens(X)$ as a subspace of the topological space
$\mathcal{H}(X)$ with the Vietoris topology.
% \begin{lemma} \label{lemma-lenscont}
% %
% $\xlens{\cdot}X : \mathcal{H}(X)\to\Lens(X)$ is continuous.
% %
% \end{lemma}
% \begin{proof}
% %
% It suffices to show that $\xlens{\cdot}X^{-1}$ preserves the
% property of being Vietoris basic open.
% Let $U\subseteq X$ be open. Clearly, it suffices to show that
% for compact $K\subseteq X$,
% %
% $U\cap \xlens{K}X \neq\emptyset$ implies $U\cap K\neq\emptyset$, and $U\supseteq
% K$ implies $U\supseteq \xlens{K}X$. The first implication holds since
% $\xlens{K}X \subseteq\cl{K}$, the second holds since $\xlens{K}X \subseteq\sat K$.
% %
% \end{proof}
\begin{propo} \label{proposition-fpcont}
%
$f_\L : \Lens(X) \to \Lens(Y)$ is continuous.
%
\end{propo}
\begin{proof}
Recall that \(f_\L = \xlens\cdot Y \circ f_{\mathcal{H}}|_{\Lens(X)}\), which
is a composition of continuous maps, by Lemma~\ref{lemma-lens} and
Proposition~\ref{proposition-fhcont}.
\end{proof}
Specialising Proposition~\ref{proposition-fpcont} to domains we obtain that
the Plotkin powerdomain operation defines an endofunctor over the category of
domains with continuous functions as morphisms, as shown in \cite{AJ,GHKLMS}.
\begin{corollary}
%
Let $ D, E $ be domains and $ f:D \to E $ continuous. Then $ f_\L :
\powerspace (D) \to \powerspace (E) $ is continuous.
%
\end{corollary}
\subsection{Lenses over a subspace}
Here we will look at the lenses over a subspace and identify these as a subset
of the lenses over the full space. The motivation for this is the subset
\(D^R\) of representing elements of a domain representation \((D, \delta : D^R
\to X)\). However, since the results are purely topological the exposition will
use general topological spaces.
Let \(X\) be a topological space and \(Y\) be a non-empty subspace of \(X\)
with the relative topology. Recall that the lens spaces \(\Lens(X)\) and
\(\Lens(Y)\) are considered as topological spaces with the Vietoris topology.
\begin{lemma} \label{lemma-lensclosure}
Let \(K \subseteq Y\) be non-empty and compact.
\begin{enumerate}[(i)]
\item \(\xlens{K}Y = \xlens{K}X \cap Y\).
\item \(\xlens KX = \xlens{\xlens KY}X\)
\end{enumerate}
\end{lemma}
\begin{proof}
\begin{enumerate}[(i)]
\item
A straightforward exercise for the reader using that open sets in \(Y\)
are relativised open sets in \(X\).
\item
Clearly, \(K \subseteq \xlens KY\) and by (i) \(\xlens KY \subseteq \xlens KX\). Applying the
monotone lens operator we get \(\xlens KX \subseteq \xlens{\xlens KY}X
\subseteq \xlens{\xlens KX}X = \xlens KX\).
%
The statement can also be viewed as a special case of Lemma~\ref{lemma-fhmon}~(ii).
%
\end{enumerate}
\end{proof}
The inclusion function \(\iota : Y \to X\) is continuous so the map \(\iota_\L
: \Lens(Y) \to \Lens(X)\) is continuous by
Proposition~\ref{proposition-fpcont}. We say that the subspace
\(\iota_\L[\Lens(Y)]\) of lenses in \(\Lens(X)\) are the \emph{\(Y\)-generated
lenses} and denote them by \(Y\mbox{-}\Lens(X)\).
\begin{lemma} \label{lemma-ygenerated}
Let \(L\) be a \(Y\)-generated lens, i.e., \(L = \xlens MX\) for some lens
\(M \subseteq Y\). Then \(L \cap Y = M \in \Lens(Y)\) and $ L = \xlens{L \cap Y }X $.
\end{lemma}
\begin{proof}
Clearly, \(M \subseteq L \cap Y\). Suppose \(y \in Y\) belongs to \(\xlens
MX\). Then \(y\) belongs to the saturation and the closure of \(M\) in
\(X\), and, a fortiori, \(y\) belongs to the saturation and the closure of
\(M\) in \(Y\), implying that \(y \in M\). Hence, \(L \cap Y = M\). Thus,
\begin{equation*}
L = \xlens{M}X = \xlens{L \cap Y}X \subseteq \xlens{L}X = L.
\end{equation*}
\end{proof}
\begin{theor} \label{thm-lens-subspace}
Let \(Y\) be a non-empty subspace of \(X\). Then \(Y\mbox{-}\Lens(X) \cong \Lens(Y)\).
\end{theor}
\begin{proof}
Let \(f : Y\mbox{-}\Lens(X) \to \Lens(Y)\) be defined by \(f(L) = L \cap
Y\). The function $f$ is well-defined by Lemma~\ref{lemma-ygenerated}.
By Lemma~\ref{lemma-lensclosure} we have \(f \circ \iota_\L (L) =
\xlens{L}X \cap Y = \xlens{L}Y = L\), for all \(L \in \Lens(Y)\), so \(f
\circ \iota_\L = \id\). By Lemma~\ref{lemma-ygenerated} we have \(\iota_\L
\circ f(L) = \xlens{L \cap Y}X = L\), for all \(L \in Y\mbox{-}\Lens(X)\), so
\(\iota_\L \circ f = \id\).
We have already established the continuity of \(\iota_\L\) so all that
remains to show is the continuity of \(f\). Let \(V\) be an open set in
\(Y\), and let \(U\) be some open set in \(X\) such that \(V = U \cap
Y\). We will show that the inverse image under \(f\) of the subbasic open
sets \(V_\cap\) and \(V_\supseteq\) are \(U_\cap\) and \(U_\supseteq\)
respectively.
Let \(L \in Y\mbox{-}\Lens(X)\). We have
\begin{equation*}
L \in f^{-1}[V_\cap] \iff (L \cap Y) \cap V \ne \emptyset \iff L \cap V
\ne \emptyset \;\Longrightarrow\; L \cap U \ne \emptyset,
\end{equation*}
that is, \(L \in U_\cap\). Going the other way we have \(L \cap U \ne
\emptyset\) implies \((L \cap Y) \cap U \ne \emptyset\) since \(L \subseteq
\cl{L \cap Y}\). But \(L \cap Y \subseteq Y\), so \((L \cap Y) \cap V \ne
\emptyset\). The latter is equivalent to \(L \in f^{-1}[V_\cap]\).
We also have \(L \in f^{-1}[V_\supseteq] \iff L \cap Y \subseteq V\), which
implies \(L \subseteq U\) since \(L \subseteq \sat(L \cap Y)\), that is \(L
\in U_\supseteq\). Going the other way we have \(L \subseteq U
\;\Longrightarrow\; L \cap Y \subseteq U \cap Y = V\), showing that \(L \in
f^{-1}[V_\supseteq]\).
\end{proof}
\begin{lemma} \label{lemma-dense-subspace}
Let \(Y\) be a dense subspace of \(X\). Then \(Y\mbox{-}\Lens(X)\) is a dense subspace
of \(\Lens(X)\).
\end{lemma}
\begin{proof}
Let \(L\) belong to a basic open set. The basic open sets of the Vietoris
topology are finite intersections of the form \(U_{1\cap} \cap \cdots
U_{n\cap} \cap V_\supseteq\). Since \(L \subseteq V\) and \(L \cap U_i \ne
\emptyset\) it must be the case that \(V \cap U_i\) is a non-empty open
set. Since \(Y\) is dense in \(X\) there exists a point \(y_i \in Y\) such
that \(y_i \in V \cap U_i\). The finite set \(S = \{y_1, \ldots, y_n\}\) is a
subset of \(V\) so the \(Y\)-generated lens \(L' = \xlens SX\) is also a
subset of \(V\). The point \(y_i \in L'\) witnesses that \(L' \cap U_i \ne
\emptyset\), so \(L' \in U_{1\cap} \cap \cdots U_{n\cap} \cap V_\supseteq\).
\end{proof}
\section{A powerdomain representation}
Let $ (D, \delta: D^{R} \to X ) $ be a domain representation. Recall that the
Plotkin powerdomain \(\powerspace(D)\) can be identified with \(\Lens(D)\).
\begin{definition}
A lens $ L \in \powerspace(D) $ is {\em total} if it is \(D^R\)-generated. Let
$\powerspace (D)^{R} $ denote the subspace of total lenses, i.e., the space
\(D^R\mbox{-}\Lens(D)\).
\end{definition}
By Theorem~\ref{thm-lens-subspace} we have that
\begin{equation*}
\Lens(D^R) \cong \powerspace(D)^R.
\end{equation*}
Thus, the choice of totality is essentially forced upon us. The map $
\delta_\L : \Lens(D^R) \to \Lens (X) $ is a continuous map by
Proposition~\ref{proposition-fpcont}. Define \(\delta_\powerspace : \powerspace(D)^R \to
\Lens(X)\) by composition of \(\delta_\L\) with the homeomorphism above, i.e.,
\(\delta_\powerspace(L) = \delta_\L(L \cap D^R)\). Being a composition of continuous maps,
\(\delta_\powerspace\) is also continuous.
\begin{definition}
Let \((D, \delta : D^R \to X)\) be a domain representation.
\begin{enumerate}[(i)]
\item Let $ \powerspace_{ (D, \delta)} (X) = \delta_\powerspace[\powerspace (D)^{R}]
$ be the topological quotient with respect to $ \delta_\powerspace $.
\item Let \(\powerspace(D,\delta)\) denote the pair \((\powerspace(D),
\delta_\powerspace : \powerspace(D)^R \to \powerspace_{(D,\delta)}(X))\).
\item A subset \(A \subseteq X\) is \emph{\((D,\delta)\)-representable}, or
simply \emph{representable}, if \(A \in \powerspace_{(D, \delta)}(X)\).
\end{enumerate}
\end{definition}
\begin{propo}
Let \((D, \delta : D^R \to X)\) be a domain representation. Then
\(\powerspace(D,\delta)\) is a domain representation.
\end{propo}
\begin{proof}
As \(\powerspace_{(D, \delta)}(X)\) is given the quotient topology there is
nothing further to be shown.
\end{proof}
Note that the topology on \(\powerspace_{(D, \delta)}(X)\) is finer than the
Vietoris topology since \(\delta_\powerspace : \powerspace(D)^R \to \Lens(X)\) is
continuous and \(\powerspace_{(D, \delta)}(X) \subseteq \Lens(X)\) is given
the quotient topology.
\begin{examp}
The simplest example of a domain representation is the identity map $ \id : D \to D $ on a domain $D$.
Then $ \powerspace_{ (D, \id)} (D) $ is homeomorphic to the Plotkin powerdomain over $D$ via $ \id_\powerspace $.
\end{examp}
The following proposition is the main technical step in showing the
functoriality of the powerspace operator \(\powerspace\).
\begin{propo} \label{proposition-morph}
Let $ f : (D, \delta : D^{R} \to X ) \rightarrow ( E , \varepsilon :E^{R}
\to Y ) $ be a representation morphism. Then $ f_\L : \powerspace (D,
\delta ) \to \powerspace ( E , \varepsilon ) $ is a representation morphism.
\end{propo}
\begin{proof}
By assumption, the left hand diagram commutes.
We will show that the right hand diagram commutes as well.
\begin{equation*}
\begin{tikzpicture}[->,scale=1.2]
\path (0,0) node (x) {$X$} (2,0) node (y) {$Y$};
\path (0,1) node (dr) {$D^R$} (2,1) node (er) {$E^R$};
\path (0,2) node (d) {$D$} (2,2) node (e) {$E$};
\draw (dr) -- node[left] {$\delta$} (x) ;
\draw[right hook->] (dr) -- node[left] {$\iota$} (d);
\draw (er) -- node[right] {$\epsilon$} (y);
\draw[right hook->] (er) -- node[right] {$\iota$} (e);
\draw (d) -- node[above] {$f$} (e);
\draw (dr) -- node[above] {$f|_{D^R}$} (er);
\draw (x) -- node[above] {$g$} (y);
\path (4,0) node (px) {$\powerspace_{(D,\delta)}(X)$} (6,0) node (py) {$\powerspace_{(E,\epsilon)}(Y)$};
\path (4,1) node (pdr) {$\powerspace(D)^R$} (6,1) node (per) {$\powerspace(E)^R$};
\path (4,2) node (pd) {$\powerspace(D)$} (6,2) node (pe) {$\powerspace(E)$};
\draw (pdr) -- node[left] {$\delta_\powerspace$} (px) ;
\draw[right hook->] (pdr) -- node[left] {$\iota$} (pd);
\draw (per) -- node[right] {$\epsilon_\powerspace$} (py);
\draw[right hook->] (per) -- node[right] {$\iota$} (pe);
\draw (pd) -- node[above] {$f_\L$} (pe);
\draw (pdr) -- node[above] {$f_\L|_{\powerspace(D)^R}$} (per);
\draw (px) -- node[above] {$g_\L$} (py);
\end{tikzpicture}
\end{equation*}
The intention is that the lens lifting of the domain function should be the
representation morphism. However, the lens lifting can be applied to two
different but related maps, namely, \(f\) and \(f|_{D^R}\). The different
lens liftings need to be related to show that elements of
\(\powerspace(D)^R\) are mapped to \(\powerspace(E)^R\). Let \(L \in
\powerspace(D)^R\), i.e., there exists \(M \subseteq D^R\) such that \(L =
\xlens MD\).
\begin{align*}
f_\L(L) &= f_\L(\xlens MD)\\
&= \xlens{f[\xlens MD]}E&(\mbox{by definition of }f_\L)\\
&= \xlens{f[M]}E&(\mbox{by Lemma~\ref{lemma-fhmon}(ii)})\\
&= \xlens{f|_{D^R}[M]}E&(M \subseteq D^R)\\
&= \xlens{\xlens{f|_{D^R}[M]}{E^R}}E&(\mbox{by Lemma~\ref{lemma-lensclosure}(ii)})\\
&= \xlens{(f|_{D^R})_\L(M)}E\,.&(\mbox{by definition of }(f|_{D^R})_\L)
\end{align*}
From either of the last two lines it is clear that \(f_\L(L) \in E^R\mbox{-}\Lens(E) = \powerspace(E)^R\).
Let $ g : X \to Y $ be the unique continuous map such that $ g \circ \delta
= \varepsilon \circ f|_{ D^{R}} $. Now, let \(L \in \powerspace(D)^R\),
i.e., there exists \(M \subseteq D^R\) such that \(L = \xlens MD\).
\begin{align*}
g_\L(\delta_\powerspace(L)) &= g_\L ( \delta_\L (M) )\\
&= (g \circ \delta)_\L (M) &\mbox{by Lemma~\ref{lemma-fpcomp}}\\
&= \xlens{g \circ \delta [M]}Y\\
&= \xlens{\epsilon \circ f|_{D^R} [M]}Y&\mbox{by assumption}\\
&= \epsilon_\L(\xlens{f|_{D^R} [M]}{E^R})\\
&= \epsilon_\powerspace(\xlens{\xlens{f|_{D^R} [M]}{E^R}}E)\\
&= \epsilon_\powerspace(f_\L(L))\,.&\mbox{by derivation above}\\
\end{align*}
Showing that \(f_\L : \powerspace(D) \to \powerspace(E)\) represents
\(g_\L : \powerspace_{(D,\delta)}(X) \to \powerspace_{(E,\epsilon)}(Y)\).
\end{proof}
Let \((D,\delta)\) and \((E,\epsilon)\) be domain representations of \(X\).
If $ f : D \to E $ is a continuous reduction and $ \powerspace_{ (D, \delta )}
(X) = \powerspace_{ ( E , \varepsilon ) } (X) $, then $ f_\L : \powerspace(D)
\to \powerspace(E) $ is a continuous reduction.
\begin{theor} \label{thm-endofunctor}
The powerspace operator $ \powerspace $ is an endofunctor over the
category of domain representations with representation morphisms.
\end{theor}
\begin{proof}
If \(f : (D, \delta) \to (E,\epsilon)\) is a representation morphism, then by
Proposition~\ref{proposition-morph} \(\powerspace(f) = f_\L\) is a
representation morphism from \(\powerspace(D, \delta)\) to
\(\powerspace(E, \epsilon)\).
%
Functoriality holds by Lemma~\ref{lemma-fpcomp}.
\end{proof}
%
\section{Representable subsets}
Let \((D, \delta: D^R \to X)\) be a domain representation. We study
which subsets of \(X\) are representable.
The following lemma shows that nothing further would be representable even if
we relaxed our totality to arbitrary non-empty compact subsets of \(D^R\) instead of
\(D^R\)-generated lenses.
\begin{lemma}
If \(A = \xlens{\delta[K]}X\) for some non-empty compact set \(K \subseteq D^R\), then
\(A\) is representable.
\end{lemma}
\begin{proof}
The lens $ \xlens{K}D $ is $D^{R}$-generated. Thus,
\begin{equation*}
\delta_\powerspace ( \xlens{K}D ) = \delta_\L(\xlens{K}D \cap D^R) =
\delta_\L(\xlens{K}{D^R}) = \xlens{\delta[\xlens K{D^R}]}X = \xlens{\delta[K]}X = A.
\end{equation*}
%
The penultimate equation holds by Lemma~\ref{lemma-fhmon}~(ii).
%
\end{proof}
\begin{lemma} \label{lemma-union}
If $A_{1} , \dots , A_{n}$ are representable, then $ \xlens{
\bigcup_{i=1}^{n} A_{i}}X$ is representable.
\end{lemma}
\begin{proof}
Assume that \(L_i \in \powerspace(D)^R\) satisfies \(\delta_\powerspace(L_i) = A_i\),
for $ 1 \leq i \leq n $. Let $ A = \bigcup_{i=1}^{n} A_{i} $, and $ L = \xlens{
\bigcup_{i=1}^{n} L_{i} }D $. Then $ \delta [ {\uparrow} L \cap D^{R} ] \subseteq
\sat A $ by monotonicity of $ \delta $ w.r.t. the specialisation order, and $
\delta [ \cl{L} \cap D^{R} ] \subseteq \cl{A} $ by continuity of $ \delta $.
Hence, $ A \subseteq \delta [ L \cap D^{R} ] \subseteq \xlens{A}X $, i.e., $ \xlens{
A}X = \xlens{ \delta [ L \cap D^{R} ] }X = \delta_\powerspace(L) $.
\end{proof}
\begin{lemma} \label{lemma-finitelygen}
Any finitely generated lens \(A \subseteq X\) is representable.
\end{lemma}
\begin{proof}
Any singleton set \(\{x\}\) is representable since we may choose any \(d \in
\delta^{-1}(x)\), and clearly \(\delta_\powerspace(\{d\}) = \{x\}\). The result now
follows from Lemma~\ref{lemma-union}.
\end{proof}
\begin{examp}
Let $ X$ be a discrete space, so $ \Lens (X) = \wp_{\mathrm f}^{*} (X) $, the set
of finite non-empty subsets of $X$. By
Lemma~\ref{lemma-finitelygen}, every finite non-empty set is representable.
Hence, $ \powerspace_{ (D, \delta)} (X) = \wp_{\mathrm f}^{*} (X) = \Lens(X)$.
\end{examp}
\begin{lemma}
Non-empty relatively closed subsets of representable sets are representable.
\end{lemma}
\begin{proof}
Let $ L \in \powerspace(D)^R $ and $ A = \delta_\powerspace(L) $. Let \(C\) be a
closed set intersecting \(A\). By continuity \(\delta^{-1}[C]\) is closed in
\(D^R\). The lens \(L' = \xlens{L \cap \delta^{-1}[C]}D\) is
\(D^R\)-generated and \(\delta_\powerspace(L') = A \cap C\).
\end{proof}
For the class of retract representations we can show that all lenses are
representable.
\begin{lemma} \label{lemma.allcompacts}
Let $ ( D, \delta :D^{R} \rightarrow X ) $ be a retract representation.
Then $ \powerspace_{ (D, \delta)} (X) = \Lens (X) $, and the topologies
coincide.
\end{lemma}
\begin{proof}
Let $ s : X \to D^{R} $ be a continuous map such that $ \delta \circ s =
\id_{X} $, and let $ A \subseteq X $ be a lens. Then
\[ \delta_\L ( s_\L (A)) = \delta_\L (\xlens{s [A]}D ) = \xlens{ \delta[ s[A]]}X = \xlens{A}X = A .\]
Since \(\delta_\L \circ s_\L : \Lens(X) \to \powerspace_{(D,\delta)}(X)\) is continuous
it follows that the topology on \(\Lens(X)\) is finer than the topology on
\(\powerspace(X)\). But, since the other direction is known in general, we
have that the two topologies must coincide.
\end{proof}
According to \cite{ELS}, a compact $qcb$ space $X$ with the Hausdorff
property is countably based. In this case, there exists a dense, retract
representation $ ( D, \delta :D^{R} \rightarrow X ) $ (see \cite{Blanck00}),
and therefore, by Lemma~\ref{lemma.allcompacts}, all compact subsets of $X$
are $ (D, \delta)$-representable and the induced topology coincides with the
Vietoris topology.
The following example shows that there are domain representations for which
not all lenses are representable. It also shows that representability depends
on the underlying domain representation.
\begin{examp}
Let \(X\) be the natural numbers \(\nats\) with the order topology
(Alexandroff topology) given by the usual ordering on \(\nats\). The open
sets in this topology are the infinite intervals \([n,\infty)\), for \(n \in
\nats\). The lenses over \(X\) are finite or infinite intervals of natural
numbers. We note that \(X\) is \(T_0\), but neither \(T_1\) nor sober; it is
also not a cpo.
We construct a domain representation of \(X\). Let \(D\) be the domain
\begin{equation*}
\begin{tikzpicture}
\fill (3,0) circle (1mm) node[below right] {\(\bot\)};
\foreach \n/\m/\ntext/\mtext in {0/1/0/1, 1/2/1/2, 2/3/2/3, 4/5/n/n+1} {
\draw[thick] (\n,2) node[above right] {\(b_{\mtext}\)}
-- (\n,1) node[above right] {\(a_{\ntext}\)} -- (3,0);
\fill (\n,2) circle (1mm);
\fill (\n,1) circle (1mm);
}
\draw (3,1.3) node {\(\ldots\)};
\draw (5,1.3) node {\(\ldots\)};
\end{tikzpicture}
\end{equation*}
Let \(D^R = D \setminus \{\bot\}\), and define the representation map
\(\delta : D^R \to X\) by
\begin{equation*}
\delta(a_i) = \delta(b_i) = i.
\end{equation*}
It is easy to see that \(\delta\) is continuous. We need to verify that it
is a quotient map. Let \(A \subseteq X\) be such that its pre-image
\(U = \delta^{-1}[A]\) is open in \(D^R\). If \(n \in A\) then \(a_n \in
U\), and since \(U\) is open \(b_{n+1} \in U\), and hence, \(n+1
\in A\). Thus, \(A\) must be an interval \([n,\infty)\) for some \(n\),
showing that \(\delta\) is a quotient map.
Clearly, there cannot exist a continuous section \(s : X \to D^R\), so
\((D,\delta)\) is not a retract domain representation.
Let \(K \subseteq D^R\) be compact. Then \(K\) must be finite. The lens
closure \(\xlens{K}D\) is also finite. Thus, all total lenses in
\(\powerspace(D,\delta)\) are finite. The image of \(\xlens{K}D\) under
\(\delta_\powerspace\) will be a finite interval. That is, the space
\(\powerspace_{(D,\delta)}(X)\) only consists of finite intervals.
As a contrast we construct a retract domain representation such that all
lenses over \(X\) are representable. Let \(E\) be the ideal completion of
\((\nats, \le)\). Let \(E^R\) be the set of compact elements. Let the
representing map \(\epsilon : E^R \to X\) be the identity. This is a retract
domain representation of \(X\), where the section is again the identity. By
Lemma~\ref{lemma.allcompacts} \(\powerspace_{(E,\epsilon)}(X) \cong \Lens(X)\).
These two domain representations of \(X\) show that the powerspace depends
on the chosen domain representation, and that for some domain
representations there may exist lenses that are not representable.
\end{examp}
Given an admissible representation of $X$, we do not know whether all lenses in
$ X$ are representable, but we can say something about the lenses generated by
continuous images of the Cantor space $ \mathbf{C} $.
\begin{lemma}
\label{lemma-cantor}
Let $ ( D, \delta :D^{R} \rightarrow X ) $ be an admissible representation.
If $ f: \mathbf{C} \rightarrow X $ is a continuous function, then $ \xlens{ f[
\mathbf{C} ] }X $ is $ (D, \delta ) $-representable.
\end{lemma}
\begin{proof}
We represent $ \mathbf{C} $ as a dense totality in the Cantor domain. Since
$ (D, \delta ) $ is admissible, the continuous map $ f: \mathbf{C}
\rightarrow X $ lifts to a continuous $ \hat{f} $ from the Cantor domain
into $D$. Then $ \hat{f} [ \mathbf{C} ] \subseteq D^{R} $ is a non-empty compact set
and
%
\[ \delta_\powerspace ( \xlens{\hat{f} [ \mathbf{C} ]}D )
% = \delta_\L ( \xlens{\hat{f} [ \mathbf{C} ]}{D}\cap D^{R} )
= \delta_\L ( \xlens{\hat{f} [ \mathbf{C} ]}{D^{R}} )
= \xlens{\delta[ \xlens{\hat{f} [ \mathbf{C} ]}{D^{R}} ]}{X}
= \xlens{\delta[\hat{f} [ \mathbf{C} ] ]}{X}
= \xlens{ f[ \mathbf{C} ] }X\,.
\]
%
The penultimate equation holds by Lemma~\ref{lemma-fhmon}(ii).
%
\end{proof}
\begin{examp}
%
Important instances of this Lemma are
the domain representations of the
total continuous functionals of finite types over the natural
numbers. More precisely, let $D_\iota$ be the flat domain
$\nats_\bot$ and $D_{\rho\to\sigma} = [D_\rho\to D_\sigma]$,
the domain of continuous functions from $D_\rho$ to $D_\sigma$.
Let $D^R_\rho$ be the set of total elements in $D_\rho$, i.e\
$D^R_\iota = \nats$ and
$D^R_{\rho\to\sigma} = \{f \mid f[D^R_{\rho}] \subseteq D^R_\sigma\}$.
%
Two total functionals $f,g$ of the same type are equivalent
if they map equivalent arguments to equivalent results.
Ershov showed that the quotients of these equivalence relations
define the total continuous functionals introduced by Kleene and Kreisel
\cite{Kleene59,Kreisel59,Ershov77}. Let
$\delta_\rho\colon D^R_\rho\to K_\rho$ denote these quotients.
%
The domain representations $(D_\rho,\delta_\rho)$
are admissible, see e.g. \cite[Theorem 7.6]{Hamrin05}.
Furthermore, Normann showed that every compact subset
of $K_\rho$ is the continuous image of a compact subspace of Baire
space, and hence a continuous image of Cantor space
\cite[Theorem 3.45 (iv)]{Normann80}.
%
It follows, by Lemma~\ref{lemma-cantor}, that all non-empty compact subsets
of $K_\rho$ are representable.
%
A more direct proof of this fact was implicitly also given by
Escardó (2008, Lemma 3.3.4.3).
%Escardó \cite[Lemma 3.3.4.3]{Escardo08}.
\end{examp}
An interesting subclass of the $ qcb_{0} $ spaces are the sequential Hausdorff spaces which
admit a countable pseudobase consisting of closed sets \cite{Normann08}. Every such space $X$
has a dense, admissible and upwards-closed domain representation $ ( D, \delta :D^{R} \rightarrow X ) $,
where upwards-closed means that if $ x \in D^{R} $ and $ x \sqsubseteq x' $, then $ x' \in D^{R} $ and
$ \delta (x) = \delta (x') $. Dag Normann has proved (private communication) that in this case, every
non-empty compact subset $ K $ of $ X $ can be represented as a continuous image of Cantor space and is $ (D,
\delta ) $-representable.
\section{Topological properties}
We study what properties, primarily topological,
of a domain representable space are preserved by the powerspace functor.
%
We assume throughout that \((D, \delta: D^R \to X)\) is a domain
representation of \(X\).
%\subsection{Dense representations}
\begin{lemma} \label{lemma-dense-representation}
If $ (D, \delta) $ is a dense domain representation, then $ (\powerspace (D),
\delta_\powerspace)$ is a dense domain representation.
\end{lemma}
\begin{proof}
By Lemma~\ref{lemma-dense-subspace}.
\end{proof}
%\subsection{Topological separation}
\begin{propo} \label{proposition_tzero}
If \(X\) is \(T_0\) then $ \powerspace_{ (D, \delta)} (X)$ is $T_{0} $
and therefore a $qcb_0$-space.
\end{propo}
\begin{proof}
The Vietoris topology on $ \Lens (X) $ is $ T_{0} $, and so is any finer topology on the subspace $ \powerspace_{ (D, \delta)} (X)$.
By construction, $ \powerspace_{ (D, \delta)} (X)$ is a topological quotient of
$\powerspace(D)^R$, a countably based space.
\end{proof}
%\subsection{Admissible representations and $qcb_{0} $ spaces}
A $qcb_{0} $ space $X$ is characterised by the existence of a dense, admissible
representation $ ( D, \delta :D^{R} \rightarrow X ) $. We now prove that the
powerspace $ \powerspace_{ (D, \delta ) } (X) $ is independent of the specific
choice of a dense admissible representation.
\begin{lemma}
Let $ ( D, \delta :D^{R} \rightarrow X ) $ and $ ( E , \varepsilon: E^{R} \to
X ) $ be dense, admissible representations of \(X\).
Then $ \powerspace_{ (D, \delta ) } (X) = \powerspace_{ ( E , \varepsilon) } (X) $.
Moreover, the powerspace representations $ \powerspace (D, \delta ) $ and
$ \powerspace ( E , \varepsilon) $ reduce to each other.
\end{lemma}
\begin{proof}
Since $ ( D, \delta ) $ is dense and $ ( E , \varepsilon ) $ is
admissible, there exists a continuous reduction $ f : (D, \delta ) \to
( E , \varepsilon) $. The representation morphism $ f_\L : \powerspace
(D, \delta ) \to \powerspace ( E , \varepsilon) $ represents the
continuous inclusion map $ \id_\L: \powerspace_{ (D, \delta ) } (X)
\subseteq \powerspace_{ ( E , \varepsilon) } (X) $.
By symmetry, the reverse inclusion map is continuous as well, and
$ \powerspace_{ (D, \delta ) } (X) = \powerspace_{ ( E , \varepsilon) } (X) $.
This means that $ f_\L : \powerspace
(D, \delta ) \to \powerspace ( E , \varepsilon) $ represents the
identity map, thus it is a continuous reduction. Symmetrically, we have a
continuous reduction of $ \powerspace ( E , \varepsilon) $ to
$ \powerspace (D, \delta ) $.
\end{proof}
We denote this representation independent powerspace of $X$ by $
\powerspace (X) $. Note that it cannot be considered as a subspace of $\Lens(X) $,
as the topology in general is finer than the subspace topology.
By proposition~\ref{proposition_tzero} the class
of $ qcb_{0} $ spaces is closed under the powerspace operation $
\powerspace $. We now show that $ \powerspace $ is an endofunctor over
the category of $ qcb_{0} $ spaces and continuous functions.
\begin{lemma}
Let $ X, Y $ be $ qcb_{0} $ spaces and let $ f: X \to Y $ be continuous.
Then $ f_\L: \powerspace (X) \to \powerspace (Y) $ is continuous.
\end{lemma}
\begin{proof}
Choose dense, admissible representations $ ( D, \delta :D^{R} \rightarrow X
) $ and $ (E, \varepsilon: E^{R} \rightarrow Y ) $. Let $ \varphi = f \circ
\delta : D^{R} \rightarrow Y $ which is a continuous map.
Since $ (D, D^{R} ) $ is dense and $ (E, \varepsilon ) $ is admissible,
there exists a continuous $ \hat{ \varphi} : D \to E $ which satisfies
$ \hat{ \varphi} [ D^{R} ] \subseteq E^{R} $ and $ \varepsilon \circ \hat{
\varphi}|_{ D^{R} } = \varphi $. In particular, $ \hat{ \varphi} :
( D, \delta ) \to (E, \varepsilon ) $ is a representation morphism of
\(f\).
\begin{equation*}
\begin{tikzpicture}[->,yscale=1.2]
\path (0,0) node (x) {$X$} (2,0) node (y) {$Y$};
\path (0,1) node (dr) {$D^R$} (2,1) node (er) {$E^R$};
\path (0,2) node (d) {$D$} (2,2) node (e) {$E$};
\draw (dr) -- node[left] {$\delta$} (x) ;
\draw[right hook->] (dr) -- node[left] {$\iota$} (d);
\draw (er) -- node[right] {$\epsilon$} (y);
\draw[right hook->] (er) -- node[right] {$\iota$} (e);
\draw (dr) -- node[above] {$\varphi$} (y);
\draw[dashed] (d) -- node[above] {$\hat\varphi$} (e);
\draw[dashed] (dr) -- node[above] {$\hat\varphi|_{D^R}$} (er);
\draw (x) -- node[above] {$f$} (y);
\end{tikzpicture}
\end{equation*}
The representation morphism $ \hat{ \varphi}_\L: \powerspace
( D, \delta )\to \powerspace (E, \varepsilon ) $ induces a unique continuous
map $ g: \powerspace (X) \to \powerspace (Y) $ which satisfies $ g \circ
\delta_\powerspace = \varepsilon_\powerspace \circ \hat{ \varphi}_\L |_{\powerspace( D)^{R} } $.
On the other hand, if $L \in \powerspace(D)^R$, then $ f_\L (\delta_\powerspace(
L))= \varphi_\L (L\cap D^R) = ( \varepsilon
\circ \hat{ \varphi}|_{ D^{R} })_\L (L\cap D^R) = \varepsilon_\powerspace ( \hat{
\varphi }_\L (L)) $, which shows that $ f_\L \circ \delta_\powerspace =
\varepsilon_\powerspace \circ \hat{ \varphi }_\L |_{\powerspace( D)^{R} }$. Since
$ \delta_\powerspace $ is a representation map, this implies
$ g = f_\L $, showing that $ f_\L $ is continuous.
\end{proof}
It is an open problem whether $ \powerspace (D, \delta ) $ is admissible when $
(D, \delta :D^{R} \rightarrow X ) $ is. Every other domain representation of
$ \powerspace (X) $ of type $ \powerspace ( E , \varepsilon) $, where $ ( E ,
\varepsilon) $ is some dense domain representation, will be continuously
reducible to $ \powerspace (D, \delta ) $. It is, however, conceivable that
there are dense domain representations of $ \powerspace (X) $ which are not,
and in that case, $ \powerspace (D, \delta ) $ need not be admissible.
Clearly, there is some dense, admissible domain representation of the $
qcb_{0} $ space $ \powerspace (X) $, but not necessarily over a powerdomain $
\powerspace (D) $.
%\subsection{Retract representations}
A strictly smaller class of topological spaces are the second countable $T_0$
spaces, characterised by the existence of a dense, retract representation.
For retract representations, we do obtain the preservation property which we
lack for admissible representations.
\begin{propo} \label{prop-retract}
Let \((D, \delta: D^R \to X)\) be a retract domain representation of \(X\).
Then $ \powerspace (D, \delta ) $ is a retract domain representation of \(\Lens(X)\).
\end{propo}
\begin{proof}
Let \(s : X \to D^R\) be a continuous maps which satisfies \(\delta \circ
s = \id_X\).
From proposition~\ref{proposition-fpcont}, we know that $ s_\L: \Lens(X) \to
\Lens(D^R) $ is continuous. Moreover, $\powerspace (D)^R $ is homeomorphic
to $ \Lens(D^R) $, so it is sufficient to show that $ \delta_\L \circ s_\L =
\id_{\Lens(X) } $, which follows from the proof of
Lemma~\ref{lemma.allcompacts}.
\end{proof}
In combination with lemma~\ref{lemma-dense-representation}, this shows that
second countable $T_0$ spaces are closed under $ \powerspace $. Moreover,
the powerspace $ \powerspace (X) $ is defined independently of the particular
choice of retract $ (D, \delta ) $, regardless of density.
Finally, we observe that the Hausdorff separation axiom is preserved by our
powerspace construction.
\begin{propo} \label{proposition-powerhaus}
If $ X$ is a Hausdorff space, then $ \powerspace_{ (D, \delta)} (X)$ is Hausdorff.
\end{propo}
\begin{proof}
The topology on $ \powerspace_{ (D, \delta)} (X)$ is finer than the subspace topology
from $ \Haus{X} $, which is Hausdorff by lemma~\ref{lemma-lenshaus}.
\end{proof}
\section{The powerspace of a metric space}
Let $(X,d)$ be a metric space. The \emph{Hausdorff distance} of two
non-empty compact subsets $K$, $K'$ is defined by.
%
\begin{equation*}
d_H(K,K') = \max \{\sup_{x\in K}d(x,K'), \sup_{x\in K'}d(x,K)\}
\end{equation*}
%
where $d(x,K) = \inf_{y \in K} d(x,y)$.
%
The following is well-known and easy to prove:
%
\begin{lemma}
\label{lemma-hausdorff-vietoris}
%
The Hausdorff distance defines a metric on $\mathcal{H}(X)$.
Its topology coincides with the Vietoris topology.
%
\end{lemma}
Let $D_{\reals}$ be the interval domain, i.e.\ the ideal completion of the
closed rational intervals in $\mathbb{Q}\cup\{{+}\infty,{-}\infty\}$ ordered
by reverse inclusion. Let $D^R_{\reals}$ be the set of ideals whose
intersection is a singleton, and let $\delta_{\reals} : D_{\reals}^{R} \to
\reals$ be the map that selects the unique element.
%
Then $(D_{\reals}, \delta_{\reals})$ is a dense retract, and hence admissible,
representation of the reals.
%
In the development below any admissible domain representation of the reals
could be taken instead, but the interval representation is particularly
convenient to work with.
In ~\cite{Blanck99} it is shown that it is possible to build a domain
representation of \(\mathcal{H}(X)\) by taking the powerdomain of the standard
domain representation of \(X\) constructed in~\cite{Blanck97}. We aim to
generalise this result by applying our powerfunctor to general domain
representations of metric spaces. However, for this to go through we need the
domain representation of the metric space to be considered as a topological
algebra, and not just as a topological space. Hence, we will require that the
metric also is representable.
\begin{definition}
\label{def-metric}
%
% Let \((D_{\reals}, \delta_{\reals} : D_{\reals}^{R} \to \reals)\) be an
% admissible domain representation of \(\reals\).
A \emph{domain
representation} of a metric space \((X, d)\) is a pair
\begin{equation*}
((D, \delta : D^{R} \to X), \bar d : D^2 \to D_{\reals})\,,
\end{equation*}
%
% where \((D, \delta : D^{R} \to X)\) is a domain representation of \(X\),
where \((D, \delta)\) is a retract domain representation of \(X\),
%
%
and
% \(\bar d : D^2 \to D_{\reals}\)
\(\bar d\)
satisfies \(\bar d[(D^{R})^2] \subseteq D_{\reals}^{R}\), and
\begin{equation*}
d(\delta(x), \delta(x')) = \delta_{\reals}\bar d(x, x')\,,
%
\end{equation*}
%
for all \(x, x' \in D^{R}\).
\end{definition}
The restriction to retract domain representations is justified since it
follows from the results and constructions in \cite{Blanck97} that all
separable metric spaces have retract domain representations in the sense
above.
In the following, let \(((D, \delta), \bar d : D^2 \to
D_{\reals})\) be a domain representation of a metric space \((X, d)\).
Consider the powerfunctor on a domain representation of a metric space. That
is, the domain representation \(\powerspace(D,\delta)\). We aim to show that
this representation can be extended to a domain representation of the space
\(\mathcal{H}(X)\) with the Hausdorff metric. From
Proposition~\ref{prop-retract} and Lemma~\ref{lemma-hausdorff-vietoris} it
follows that the space \(\mathcal{H}(X)\) is the same as the space
$\powerspace(X)$ and carries the topology induced by the Hausdorff metric.
Hence, all that is left to show is that the Hausdorff metric can be tracked by
a continuous function \(\bar d_H : (\powerspace{D})^2 \to D_{\reals} \) such
that \(\bar d_H[(\powerspace(D)^{R})^2] \subseteq
D_{\reals}^{R}\), and \( d_H(\delta_\powerspace(K),
\delta_\powerspace(K')) = \delta_{\reals}\bar d_H(K, K')\).
We now carry out the construction of $\bar d_H$.
\begin{lemma}\label{lemma.p2p}
Let \(x, y\) be elements of \(D^R\). For any \(\varepsilon > 0\) there exist
\(a \in \appr(x)\) and \(b \in \appr(y)\) such that \(\bar d(a,b)\) is an
interval of length less than \(\varepsilon\) containing
\(d(\delta(x),\delta(y))\).
\end{lemma}
\begin{proof}
Let \((r,s)\) be an open interval containing \(\delta\bar d(x,y) =
d(\delta(x),\delta(y))\). The set \(U\) of subintervals of \((r,s)\) is open
in the interval domain. The set \(\bar d^{-1}[U]\) is an open subset of \(D^2\)
containing \((x,y)\). Thus, there exist compact \(a\) and \(b\) in
\(\bar d^{-1}[U]\) below \(x\) and \(y\) respectively.
\end{proof}
Consider the powerfunctor on a domain representation of a metric space. That
is, the domain representation \((\powerspace(D), \delta_\powerspace : \powerspace(D)^R
\to \powerspace(X))\). We aim to show that the Hausdorff metric
is a continuous function from \(\powerspace(X)^2\) to \(D_\reals\).
The compact elements of \(\powerspace(D)\) can be identified as the equivalence classes
of finite sets of compact elements in \(D\). A canonical choice in each
equivalence class is the convex closure of the finite set, but this set need
not be finite. We will tacitly assume that \(A\) and \(B\) range over
\(\wp^\ast_{\mathrm{f}}(D_c)\), the set of finite non-empty subsets of \(D_c\). We will
also tacitly assume that \(a\) and \(b\) range over \(D_c\).
We will need to take minimums and maximums over non-empty sets of
intervals. These are defined as
\begin{equation*}
\min \{ [s_i, t_i] : i \in I \} = [ \min \{s_i : i \in I\}, \min \{t_i : i
\in I\} ]\,,
\end{equation*}
and analogously for \(\max\). Note that if the operators are viewed as
\(n\)-ary operators on the interval domain, for \(n \ge 1\), then they are
monotone in each argument.
It is common and often useful to define distances in metric spaces between
objects other than points in the space. It is also customary to abuse the
notation and retain the letter \(d\) for distance functions derived from
the metric \(d\). We will follow this tradition.
Define the distance \(d : X \times \powerspace(X) \to \reals\) by
\begin{equation*}
d(x,K) = \inf_{y \in K} d(x,y)\,.
\end{equation*}
We mimic this definition by defining \(\bar d : D_c \times \powerspace(D)_c \to
D_\reals\) by
\begin{equation*}
\bar d(a,B) = \min_{b \in B} \bar d(a,b)\,.
\end{equation*}
Assume that \(a \sqsubseteq a'\). Then the minimum taken in \(\bar d(a',B)\)
is over smaller intervals, as the original \(\bar d\) is monotone. Since the
minimum operation is monotone the resulting interval is smaller, i.e., \(\bar
d\) is monotone in the first argument.
To see that \(\bar d\) is monotone in its second argument, we need to consider
the upper and lower bounds on the intervals separately. Assume that \(B \sqsem
B'\). Let \(S = \{\bar d(a,b) : b \in B\}\) and \(S' = \{\bar d(a,b') : b' \in
B'\}\). For each \(b \in B\) there exists \(b' \in B'\) such that \(b
\sqsubseteq b'\). Since \(\bar d(a,b) \sqsubseteq \bar d(a,b')\) we have that
any upper bound of an interval in \(S\) will have a better (smaller) upper
bound in \(S'\), and hence \(\min S'\) will have a better upper bound than
\(\min S\). For the lower bounds we have that for each \(b' \in B'\) there
exists \(b \in B\) such that \(b \sqsubseteq b'\). Again, since \(\bar d(a,b)
\sqsubseteq \bar d(a,b')\) we have that any lower bound of an interval in
\(S'\) will have a worse (smaller) lower bound in \(S\), and hence \(\min S'\)
will have a better (larger) lower bound than \(\min S\). Thus, \(\bar d\) is
monotone in its second argument as well. Note that the above argument actually
required both directions of the Egli-Milner ordering.
The monotonicity of \(\bar d\) with respect to the Egli-Milner ordering is
enough to show that \(\bar d\) is well-defined on \(\powerspace(D)_c\). Moreover, it
allows us to extend it to a continuous function \(\bar d : D \times \powerspace(D) \to
D_{\reals}\).
Consider an \(x \in D\) and a non-empty compact \(K \subseteq D^R\). We will show that
\(d(\delta(x), \delta_\powerspace(K))\) is represented by \(\bar d(x,K)\). The value
\begin{equation*}
d(\delta(x),\delta_\powerspace(K)) = \inf_{y \in K} d(\delta(x),\delta(y))
\end{equation*}
will, in fact, be obtained for some choice of \(y_0 \in K\) since \(K\) is
compact.
\begin{lemma}\label{lemma.p2c}
Let \(x \in D^R\) and \(K \subseteq D^R\) be compact. For any \(\varepsilon
> 0\) there exist \(a \sqsubseteq x\) and \(B \sqsem K\) such that, for all
\(b \in B\), \(\bar d(a,b)\) is an interval of length less than
\(\varepsilon\).
\end{lemma}
\begin{proof}
For any \(y \in K\) there exists by Lemma~\ref{lemma.p2p} \(a_y \sqsubseteq
x\) and \(b_y \sqsubseteq y\) such that \(\bar d(a_y,b_y)\) has length less
than \(\varepsilon\). Clearly, \(\{{\uparrow}b_y : y \in K\}\) is an open
covering of \(K\) so there exists a finite subcovering
\begin{equation*}
\{{\uparrow}b_{y_1}, \ldots, {\uparrow}b_{y_n}\}\,.
\end{equation*}
Let
\begin{align*}
a &= \bigsqcup \{a_{y_1}, \ldots, a_{y_n}\}, \mbox{ and}\\
B &= \{b_{y_1}, \ldots, b_{y_n}\}\,.
\end{align*}
We have \(B \sqsem K\), and by monotonicity of \(\bar d\) we have \(\bar d(a,
b_{y_i})\) has length less than \(\varepsilon\).
\end{proof}
For an \(\varepsilon > 0\), let \(a\) and \(B\) be as in the above
lemma. Let \(b \in B\) such that \(y_0\in{\uparrow}b\), where \(y_0 \in K\) satisfies
\(d(\delta(x),\delta(y_0)) = \inf_{y \in K} d(\delta(x),\delta(y))\). Then \(\bar
d(a,b)\) is an interval of length less than \(\varepsilon\) containing
\(d(\delta(x),\delta(y_0))\) since \(\bar d\) represents \(d\). The intervals
\(\bar d(a,b')\) for all other \(b' \in B\) will have upper bounds greater
than or equal to \(d(\delta(x), \delta(y_0))\) and will have length less than
\(\varepsilon\). The minimum of all these intervals will be an interval of
length less than \(\varepsilon\) approximating the distance. Since
\(\varepsilon\) was arbitrary we have that \(\bar d(x,K)\) will be a total
element in \(D_{\reals}\). We have shown the following result.
\begin{propo}\label{prop.p2c}
The function \(\bar d : D \times \powerspace(D) \to D_{\reals}\) induces the function
\(d: X \times \powerspace(X) \to \reals\).
\end{propo}
Consider now the distance function \(d : \powerspace(X)^2 \to \reals\) defined by
\begin{equation*}
d(K,K') = \sup_{x \in K} d(x,K'),
\end{equation*}
so that \(d_H(K,K') = \max \{d(K,K'), d(K',K)\}\).
Note that in general $d(K,K')\neq d(K',K)$. Define \(\bar d : \powerspace(D)_c^2 \to
D_{\reals}\) by
\begin{equation*}
\bar d(A,B) = \max_{a \in A} \bar d(a,B).
\end{equation*}
Clearly, \(\bar d\) is monotone in its second argument since the point-to-set
version is monotone in its second argument. That \(\bar d\) also is monotone in its
first argument follows from an argument similar to the monotonicity of the
second argument of the point-to-set version of \(\bar d\). Thus, \(\bar d\) is
well-defined and may be extended to a continuous function \(\bar d : \powerspace(D)^2
\to D_{\reals}\).
We may repeat the development above to prove the following result.
\begin{propo}\label{prop.c2c}
The function \(\bar d : \powerspace(D)^2 \to D_{\reals}\) induces the function \(d :
\powerspace(X)^2 \to \reals\).
\end{propo}
Now we mimic the Hausdorff metric by defining \(\bar d_H: \powerspace(D)_c^2 \to D_{\reals}\) by
\begin{equation*}
\bar d_H(A,B) = \max \{\bar d(A,B), \bar d(B,A)\}.
\end{equation*}
This is clearly monotone and therefore well-defined and extendable to a
continuous function.
\begin{propo}\label{prop.metric}
\(\bar d_H : \powerspace(D)^2 \to D_{\reals}\) represents \(d_H :
\powerspace(X)^2 \to \reals\).
\end{propo}
\begin{proof}
Immediate.
\end{proof}
\begin{theor}
Let \(((D, \delta), \bar d : D^2 \to D_{\reals})\) be a retract domain
representation of a metric space \((X, d)\). Then \((\powerspace(D, \delta),
\bar d_H : \powerspace(D)^2 \to D_{\reals})\) is a retract domain
representation of the metric space \((\mathcal{H}(X), d_H)\).
\end{theor}
\begin{proof}
By Lemma~\ref{lemma-hausdorff-vietoris} and Propositions~\ref{prop.metric} and~\ref{prop-retract}.
\end{proof}
\section{Conclusion and further work}
The main motivation for the powerspace construction presented here is its natural
characterisation as a space of certain compact subsets. In the important example
of a separable metric space, it gives the expected result, the set of non-empty compact
subsets with the Hausdorff metric, thus generalising the result of \cite{Blanck99}.
A countable domain is a domain representation of itself with the identity as
the representation map. Our powerspace construction will in this case yield
the Plotkin powerdomain. Thus, our construction is conservative with respect
to usual powerdomains.
The powerdomain is the space of lenses with the Vietoris
topology~\cite{Smyth83}. As we have seen, our construction will give a space
of lenses with the Vietoris topology in many cases. It is not clear whether
this is always true in general. That is, there may exist topological spaces
for which our powerspace will have a topology that is strictly finer than the
Vietoris topology. Even if this turns out to be the case, there is still scope
to provide further classes of spaces for which the induced topology is the
Vietoris topology, possible candidates here would be cpos or sober spaces.
% In the case of a dense, retract representation $ (D, \delta) $ of a
% topological space, every lens is $ (D, \delta) $-representable, but if we
% consider a representation of the same topological space, but without the
% retract property, this need not remain true. In the more general case of a
% dense, admissible representation $ (D, \delta) $, it is not clear whether
% there might exist lenses that are not $ (D, \delta) $-representable
The notion of an admissible representation plays an important role, as the
existence of such a representation ensures that the powerspace construction is
functorial (w.r.t.\ continuous functions). However, we do not know that the
powerspace of an admissible domain representation will again be admissible.
This is the most central open problem in this paper. For the easier situation
of retract representations, we know that the powerspace will again be a
retract representation.
There is an alternative characterisation of the Plotkin powerdomain as the
free algebra w.r.t. the Plotkin powertheory (see \cite{AJ,GHKLMS} for
details), and a similar free algebra construction has been studied for $
qcb_{0} $ spaces \cite{Battenfeld06}. A clear advantage of such an algebraic
definition is that it points out the necessity of considering the space constructed
for representing non-determinism. An interesting project would be to compare this
construction to ours, as they both preserve the property of being $qcb_0$. We claim
that the connection with the topological characterisation of the Plotkin powerdomain
and the preservation of the Hausdorff separation axiom are weighty arguments for our choice.
\section*{Acknowledgements}
We would like to thank Dag Normann, Dieter Spreen and John V. Tucker
for helpful discussions at various stages of this work.
%
Our gratitude also goes to the anonymous referees for carefully checking the
proofs (in this way spotting several inaccuracies) and giving many useful hints.
\begin{thebibliography}{99}
\bibitem[Abramsky-Jung 1994]{AJ}
S.~Abramsky and A.~Jung,
Domain Theory.
In:
\emph{Handbook of Logic in Computer Science} \textbf{3}, 1-158,
Oxford University Press 1994.
\bibitem[Battenfeld 2006]{Battenfeld06}
I.~Battenfeld,
Computational Effects in Topological Domain Theory.
\emph{Electronic Notes in Theoretical Computer Science} \textbf{158}, 59-80,
Elsevier 2006.
\bibitem[Blanck 1997]
{Blanck97}
J.~Blanck,
\newblock Domain representability of metric spaces.
\newblock {\em Annals of Pure and Applied Logic}, 83:225--247, 1997.
\bibitem[Blanck 1999]{Blanck99}
J.~Blanck,
Effective domain representations of $\mathcal{H} (X) $, the space of compact subsets.
\emph{Theoretical Computer Science} \textbf{219}, 19-48,
Elsevier 1999.
\bibitem[Blanck 2000]
{Blanck00}
J.~Blanck,
Domain Representations of Topological Spaces.
\emph{Theoretical Computer Science} \textbf{247}, 229-255,
Elsevier 2000.
\bibitem[Blanck 2008]
{Blanck08}
J.~Blanck,
Reducibility of Domain Representations and Cantor-Weihrauch Domain Representations.
\emph{Mathematical Structures in Computer Science} \textbf{18}, 1031-1056,
Cambridge University Press 2008.
\bibitem[Ershov 1977]{Ershov77}
Y.~L.~Ershov.
\newblock Model {$C$} of partial continuous functionals.
\newblock In R.~Gandy and M.~Hyland, editors, {\em Logic {C}olloquium 1976},
pages 455--467. North--Holland, 1977.
\bibitem[Escardó et al. 2004]
{ELS}
M.~Escardó,
J.~Lawson and
A.~Simpson,
Comparing Cartesian Closed Categories of (Core) Compactly Generated Spaces.
Topology and its applications \textbf{143}, 105-145,
Elsevier 2004.
\bibitem[Escardó 2008]
{Escardo08}
M.~Escardó,
Exhaustible Sets in Higher-Type Computation.
\emph{Logical Methods in Computer Science} \textbf{4}, 1-37,
2008
\bibitem[Gierz et al. 2003]
{GHKLMS}
G.~Gierz,
K.~H.~Hofmann,
K.~Keimel,
J.~D.~Lawson,
M.~W.~Mislove and
D.~S.~Scott,
\emph{Continuous Lattices and Domains}.
Cambridge University Press 2003.
\bibitem[Hamrin 2005]
{Hamrin05}
G.~Hamrin, Effective Domains and Admissible Domain Representations, PhD
Thesis, \emph{Uppsala Dissertations in Mathematics} \textbf{42},
Uppsala University 2005.
\bibitem[Kleene 1959]{Kleene59}
S.~C.~Kleene.
\newblock Countable functionals.
\newblock In A.~Heyting, editor, {\em Constructivity in Mathematics}, pages
81--100. North--Holland, 1959.
\bibitem[Kreisel 1959]{Kreisel59}
G.~Kreisel.
\newblock Interpretation of analysis by means of constructive functionals of
finite types.
\newblock {\em Constructivity in Mathematics}, pages 101--128, 1959.
\bibitem[Normann 1980]{Normann80}
D.~Normann.
\newblock {\em Recursion on the countable functionals}, {\em
Lecture Notes in Mathematics} \textbf{811}.
\newblock Springer, 1980.
\bibitem[Normann 2008]
{Normann08}
D.~Normann,
A rich hierarchy of functionals of finite types.
Manuscript 2008.
\bibitem[Plotkin 1983]
{Plotkin83}
G.~Plotkin,
Pisa Notes (on Domains).
1983.
\bibitem[Schröder 2003]
{Schroder03}
M.~Schröder,
\emph{Admissible Representations for Continuous Computations},
PhD Thesis,
FernUniversität Hagen 2003.
\bibitem[Scott 1970]
{Scott70}
D.~S.~Scott,
\newblock Outline of a mathematical theory of computation.
\newblock In {\em 4th Annual Princeton Conference on Information
Sciences and
Systems}, pages 169--176, 1970.
\bibitem[Smyth 1983]
{Smyth83}
M.~B.~Smyth,
Power Domains and Predicate Transformers: A Topological View.
\emph{Lecture Notes in Computer Science} \textbf{154}, 662-675,
Springer-Verlag 1983.
\bibitem[Stoltenberg-Hansen et al. 1994]{SHLG}
V.~Stoltenberg-Hansen, I.~Lindstr\"om and E.~R.~Griffor, \emph{Mathematical
Theory of Domains}, Cambridge University Press, 1994.
\bibitem[Stoltenberg-Hansen and Tucker 1995]{ST95}
V.~Stoltenberg-Hansen and J.~V.~Tucker, Effective algebra, in S.~Abramsky et al.,
\emph{Handbook of Logic in Computer Science} \textbf{4}, 357--526, 1995.
\bibitem[Stoltenberg-Hansen and Tucker 2008]
{ST08}
V.~Stoltenberg-Hansen, J.~Tucker,
Computability on topological spaces via domain representations.
In S.~B.~Cooper et al. (Eds), \emph{New Computational Paradigms}, 153--194, 2008.
\bibitem[Weihrauch 2000]{Weihrauch00}
K.~Weihrauch, An Introduction to Computable Analysis. Springer, 2000.
\end{thebibliography}
\end{document}