chap-cauchy.tex

\chapter{Cauchy Filters on Reloids}

In this chapter I consider \emph{low filters} on reloids, generalizing
Cauchy filters on uniform spaces. Using low filters, I define Cauchy-complete
reloids, generalizing complete uniform spaces.

\fxnote{I forgot to note that Cauchy spaces induce topological (or convergence) spaces.}

\section{Preface}

Replace {\tt \textbackslash langle \dots \textbackslash rangle} with {\tt \textbackslash supfun\{\dots\}} in \LaTeX{}.

This is a preliminary partial draft.

To understand this article you need first look into my book \cite{volume-1}.

\url{http://math.stackexchange.com/questions/401989/what-are-interesting-properties-of-totally-bounded-uniform-spaces}

\url{http://ncatlab.org/nlab/show/proximity+space\#uniform\_spaces} for a proof
sketch that proximities correspond to totally bounded uniformities.

\section{Low spaces}

\fxwarning{Analyze \url{http://link.springer.com/article/10.1007/s10474-011-0136-9} (``A note on Cauchy spaces''),
\url{http://link.springer.com/article/10.1007/BF00873992} (``Filter spaces''). It also contains references to some useful results,
including (``On continuity structures and spaces of mappings'' freely available at \url{https://eudml.org/doc/16128}) that the category $\mathrm{FIL}$ of filter spaces is isomorphic to
the category of filter merotopic spaces (copy its definition).}

\begin{defn}
A \emph{lower set}\footnote{Remember that our orders on filters is the
reverse to set theoretic inclusion. It could be called an \emph{upper} set
in other sources.} of filters on $U$ (a set) is a set $\mathscr{C}$
of filters on $U$, such that if $\mathcal{G} \sqsubseteq
\mathcal{F}$ and $\mathcal{F} \in \mathscr{C}$ then $\mathcal{G} \in
\mathscr{C}$.
\end{defn}

\begin{rem}
Note that we are particularly interested in nonempty (=~containing the improper filter) lower sets of filters.
This does not match the traditional theory of Cauchy spaces (see below) which are traditionally defined as not containing empty set.
Allowing them to contain empty set has some advantages:
\begin{itemize}
\item Meet of any lower filters is a lower filter.
\item Some formulas become a little simpler.
\end{itemize}
\end{rem}


\begin{defn}
  I call \emph{low space} a set together with a nonempty lower set of
  filters on this set.
  Elements of a (given) low space are called \emph{Cauchy filters}.
\end{defn}

\begin{defn}
  $\GR \left( U , \mathscr{C} \right) = \mathscr{C}$; $\Ob \left(
  U , \mathscr{C} \right) = U$.
  $\GR (U, \mathscr{C})$ is read as \emph{graph} of space $(U, \mathscr{C})$.
  I denote $\Low(U)$ the set of graphs of low spaces on the set~$U$.
  Similarly I will denote its subsets $\mathbf{ASJ}(U)$, $\mathbf{CASJ}(U)$, $\mathbf{Cau}(U)$, $\mathbf{CCau}(U)$ (see below).
\end{defn}

\fxnote{Should use ``space structure'' instead of ``graph of space'', to match customary terminology.}

\begin{defn}
  Introduce an order on graphs of low spaces and on low spaces:
  $\mathscr{C}\sqsubseteq\mathscr{D}\Leftrightarrow\mathscr{C}\subseteq\mathscr{D}$ and
  $\left( U , \mathscr{C} \right) \sqsubseteq \left( U , \mathscr{D} \right) \Leftrightarrow \mathscr{C} \sqsubseteq \mathscr{D}$.
\end{defn}

\begin{obvious}
Every set of low spaces on some set is partially ordered.
\end{obvious}

\section{Almost sub-join-semilattices}

\begin{defn}
For a join-semilattice~$\mathfrak{A}$, a \emph{almost sub-join-semilattice} is such a set~$S\in\subsets\mathfrak{A}$, that
if $\mathcal{F},\mathcal{G}\in S$ and $\mathcal{F} \nasymp \mathcal{G}$ then $\mathcal{F} \sqcup \mathcal{G}\in S$.
\end{defn}

\begin{defn}
For a complete lattice~$\mathfrak{A}$, a \emph{completely almost sub-join-semilattice} is such a set~$S\in\subsets\mathfrak{A}$, that
if $\bigsqcap T \neq \bot^{\mathscr{F}(X)}$ then $\bigsqcup T\in S$ for every $T\in\subsets S$.
\end{defn}

\begin{obvious}
Every completely almost sub-join-semilattice is a almost sub-join-semilattice.
\end{obvious}

\section{Cauchy spaces}

\begin{defn}
A \emph{reflexive} low space is a low space $( U , \mathscr{C})$ such that
$\forall x \in U : \uparrow^U \{ x \} \in \mathscr{C}$.
\end{defn}

\begin{defn}
The \emph{identity} low space~$1^{\Low(U)}$ on a set~$U$ is the low space with graph $\setcond{\uparrow^U \{x\}}{x\in U}$.
\end{defn}

\begin{obvious}\label{cs-refl-by-id}
A low space~$f$ is reflexive iff $f\sqsupseteq 1^{\Low(\Ob f)}$.
\end{obvious}

\begin{defn}
\emph{An almost sub-join space} is a low space whose graph is an almost sub-join-semilattice.
I will denote such spaces as $\mathbf{ASJ}$.
\end{defn}

\begin{defn}
\emph{A completely almost sub-join space} is a low space whose graph is a completely almost sub-join-semilattice.
I will denote such spaces as $\mathbf{CASJ}$.
\end{defn}

\begin{defn}
A \emph{precauchy space} (aka \emph{filter space}) is a reflexive low space.
I will denote such spaces as $\mathbf{preCau}$.
\end{defn}

\begin{defn}
A \emph{Cauchy space} is a precauchy space which is also an almost sub-join space.
I will denote such spaces as $\mathbf{Cau}$.
\end{defn}

\begin{defn}
  A \emph{completely Cauchy space} is a precauchy space which is also a completely almost sub-join space.
I will denote such spaces as $\mathbf{CCau}$.
\end{defn}

\begin{obvious}
Every completely Cauchy space is a Cauchy space.
\end{obvious}

\begin{prop}
  $a\sqcup^{
    \setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}
  } b = a\sqcup b$ for
  $a,b \in \setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}$,
  provided that $\mathcal{F}$ is a proper fixed Cauchy filter on an almost sub-join space.
\end{prop}

\begin{proof}
  $\mathcal{F}$ is proper. So
  we have $a \sqcap b \sqsupseteq \mathcal{F} \neq \bot^{\mathscr{F} (X)}$. Thus $a\sqcup b$ is a Cauchy
  filter and so $a\sqcup b \in \setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}$.
\end{proof}

\begin{prop}
  $\bigsqcup^{
    \setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}
  } S = \bigsqcup S$ for nonempty
  $S \in \subsets \setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}$,
  provided that $\mathcal{F}$ is a proper fixed Cauchy filter on a completely almost sub-join space.
\end{prop}

\begin{proof}
  $\mathcal{F}$ is proper. So for every nonempty $S \in \subsets
  \setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}$
  we have $\bigsqcap S \sqsupseteq \mathcal{F} \neq \bot^{\mathscr{F} (X)}$. Thus $\bigsqcup S$ is a Cauchy
  filter and so $\bigsqcup S \in \setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}$.
\end{proof}

\begin{cor}
Every proper Cauchy filter is contained in a unique maximal Cauchy filter (for completely almost sub-join spaces).
\end{cor}

\begin{proof}
Let $\mathcal{F}$ be a proper Cauchy filter. Then
$\bigsqcup^{ \setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}} }\setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}$
(existing by the above proposition) is the maximal Cauchy filter containing~$\mathcal{F}$.

Suppose another maximal Cauchy filter~$\mathcal{T}$ contains~$\mathcal{F}$. Then $\mathcal{T}\in\setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}$
and thus $\mathcal{T} = \bigsqcup^{ \setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}} }\setcond{\mathcal{X} \in \mathscr{C} }{\mathcal{X} \sqsupseteq \mathcal{F}}$.
\end{proof}

\section{Relationships with symmetric reloids}

\fxnote{Also consider relationships with funcoids.}

\begin{defn}
  Denote $(\mathsf{RLD})_{\Low} \left( U , \mathscr{C} \right) =
  \bigsqcup \setcond{ \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X}}
  {\mathcal{X} \in \mathscr{C} }$.
\end{defn}

\begin{defn}
  $(\Low) \nu$ (\emph{low space} for endoreloid $\nu$) is a low
  space on $U$ such that
  \[ \GR (\Low) \nu = \setcond{\mathcal{X} \in \mathscr{F}(U)}
     {\mathcal{X} \times^{\mathsf{RLD}} \mathcal{X} \sqsubseteq \nu } . \]
\end{defn}

\begin{thm}
  If $\left( U , \mathscr{C} \right)$ is a low space, then $\left( U ,
  \mathscr{C} \right) = (\Low) (\mathsf{RLD})_{\Low} \left(
  U , \mathscr{C} \right)$.
\end{thm}

\begin{proof}
  If $\mathcal{X} \in \mathscr{C}$ then $\mathcal{X}
  \times^{\mathsf{RLD}} \mathcal{X} \sqsubseteq
  (\mathsf{RLD})_{\Low} \left( U , \mathscr{C} \right)$ and thus
  $\mathcal{X} \in \GR (\Low) (\mathsf{RLD})_{\Low}
  \left( U , \mathscr{C} \right)$. Thus $\left( U , \mathscr{C} \right)
  \sqsubseteq (\Low) (\mathsf{RLD})_{\Low} \left( U ,
  \mathscr{C} \right)$.
  
  Let's prove $\left( U , \mathscr{C} \right) \sqsupseteq (\Low)
  (\mathsf{RLD})_{\Low} \left( U , \mathscr{C} \right)$.
  
  Let $\mathcal{A} \in \GR (\Low)
  (\mathsf{RLD})_{\Low} \left( U , \mathscr{C} \right)$. We need
  to prove $\mathcal{A} \in \mathscr{C}$.
  
  Really $\mathcal{A} \times^{\mathsf{RLD}} \mathcal{A} \sqsubseteq
  (\mathsf{RLD})_{\Low} \left( U , \mathscr{C} \right)$. It is
  enough to prove that $\exists \mathcal{X} \in \mathscr{C} : \mathcal{A}
  \sqsubseteq \mathcal{X}$.
  
  Suppose $\nexists \mathcal{X} \in \mathscr{C} : \mathcal{A} \sqsubseteq
  \mathcal{X}$.
  
  For every $\mathcal{X} \in \mathscr{C}$ obtain $X_{\mathcal{X}} \in
  \mathcal{X}$ such that $X_{\mathcal{X}} \notin \mathcal{A}$ (if forall $X \in
  \mathcal{X}$ we have $X_{\mathcal{X}} \in \mathcal{A}$, then $\mathcal{X}
  \sqsupseteq \mathcal{A}$ what is contrary to our supposition).
  
  It is now enough to prove $\mathcal{A} \times^{\mathsf{RLD}}
  \mathcal{A} \nsqsubseteq \bigsqcup \setcond{ \uparrow^U
  X_{\mathcal{X}} \times^{\mathsf{RLD}} \uparrow^U X_{\mathcal{X}}
  }{\mathcal{X} \in \mathscr{C} }$.
  
  Really, $\bigsqcup \setcond{ \uparrow^U X_{\mathcal{X}}
  \times^{\mathsf{RLD}} \uparrow^U X_{\mathcal{X}} }{
  \mathcal{X} \in \mathscr{C} } =
  \uparrow^{\mathsf{RLD} (U , U)} \bigcup \setcond{ \uparrow^U X_{\mathcal{X}}
  \times^{\mathsf{RLD}} \uparrow^U X_{\mathcal{X}} }{
  \mathcal{X} \in \mathscr{C} }$. So our claim takes the form $\bigcup \setcond{ \uparrow^U X_{\mathcal{X}}
  \times^{\mathsf{RLD}} \uparrow^U X_{\mathcal{X}} }{
  \mathcal{X} \in \mathscr{C} } \notin \GR (\mathcal{A}
  \times^{\mathsf{RLD}} \mathcal{A})$ that is $\forall A \in
  \mathcal{A} : \bigcup \setcond{ \uparrow^U X_{\mathcal{X}}
  \times^{\mathsf{RLD}} \uparrow^U X_{\mathcal{X}} }{
  \mathcal{X} \in \mathscr{C} } \nsupseteq
  A \times A$ what is true because $X_{\mathcal{X}} \nsupseteq A$ for every $A
  \in \mathcal{A}$.
\end{proof}

\begin{rem}
  The last theorem does not hold with $\mathcal{X}
  \times^{\mathsf{FCD}} \mathcal{X}$ instead of $\mathcal{X}
  \times^{\mathsf{RLD}} \mathcal{X}$ (take $\mathscr{C} = \setcond{ \{ x
  \} }{x \in U}$ for an infinite set $U$ as a counter-example).
\end{rem}

\begin{rem}
  Not every symmetric reloid is in the form
  $(\mathsf{RLD})_{\Low} \left( U , \mathscr{C} \right)$ for some
  Cauchy space $\left( U , \mathscr{C} \right)$. The same Cauchy space can be
  induced by different uniform spaces. See
  \url{http://math.stackexchange.com/questions/702182/different-uniform-spaces-having-the-same-set-of-cauchy-filters}
\end{rem}

\begin{prop}
~
\begin{enumerate}
\item \label{low-rld-relf}$(\Low)f$~is reflexive iff endoreloid~$f$ is reflexive.
\item \label{rld-low-relf}$(\mathsf{RLD})_{\Low}f$~is reflexive iff low space~$f$ is reflexive.
\end{enumerate}
\end{prop}

\begin{proof}
~
\begin{widedisorder}
\item[\ref{low-rld-relf}] $\text{$f$ is reflexive} \Leftrightarrow
  1^{\mathsf{RLD}}\sqsubseteq f  \Leftrightarrow \forall x\in\Ob f:\uparrow(\{x\}\times\{x\})\sqsubseteq f \Leftrightarrow
  \forall x\in\Ob f:\uparrow\{x\}\times^{\mathsf{RLD}}\uparrow\{x\}\sqsubseteq f \Leftrightarrow
  \forall x\in\Ob f:\uparrow\{x\}\in(\Low)f \Leftrightarrow \text{$(\Low)f$~is reflexive}$.

\item[\ref{rld-low-relf}] Let $f$ is reflexive. Then $\forall x\in\Ob f:\uparrow\{x\}\in f$;
  $\forall x\in\Ob f:\uparrow\{x\}\times^{\mathsf{RLD}}\uparrow\{x\}\sqsubseteq(\mathsf{RLD})_{\Low}f$;
  $\forall x\in\Ob f:\uparrow(\{x\}\times\{x\})\sqsubseteq(\mathsf{RLD})_{\Low}f$;
  $1^{\mathsf{RLD}}\sqsubseteq(\mathsf{RLD})_{\Low}f$.
  
  Let now $(\mathsf{RLD})_{\Low}f$~be reflexive. Then $f = (\Low)(\mathsf{RLD})_{\Low}f$ is reflexive.
\end{widedisorder}
\end{proof}

\begin{defn}
A \emph{transitive} low space is such low space~$f$ that $(\mathsf{RLD})_{\Low}f\circ(\mathsf{RLD})_{\Low}f=(\mathsf{RLD})_{\Low}f$.
\end{defn}

\begin{rem}
The composition $(\mathsf{RLD})_{\Low}f\circ(\mathsf{RLD})_{\Low}f$ may be inequal to $(\mathsf{RLD})_{\Low}\mu$ for all low spaces~$\mu$ (exercise!).
Thus usefulness of the concept of transitive low spaces is questionable.
\end{rem}

\begin{rem}
Every low space is ``symmetric'' in the sense that it corresponds to a symmetric reloid.
\end{rem}

\begin{thm}
  $(\Low)$ is the upper adjoint of $(\mathsf{RLD})_{\Low}$.
\end{thm}

\begin{proof}
  We will prove $(\Low) (\mathsf{RLD})_{\Low} f \sqsupseteq
  f$ and $(\mathsf{RLD})_{\Low} (\Low) g \sqsubseteq g$
  (that $(\Low)$ and $(\mathsf{RLD})_{\Low}$ are monotone
  is obvious).
  
  Really:
  \begin{multline*}
  \GR (\Low) (\mathsf{RLD})_{\Low} f =
  \GR (\Low) \bigsqcup \setcond{ \mathcal{X}
  \times^{\mathsf{RLD}} \mathcal{X} }{
  \mathcal{X} \in \GR f } = \\
  \setcond{ \mathcal{Y} \in \mathscr{F}\Ob (f) }{ \mathcal{Y}
  \times^{\mathsf{RLD}} \mathcal{Y} \sqsubseteq \bigsqcup \setcond{
  \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X} }{
  \mathcal{X} \in \GR f } } \supseteq \setcond{
  \mathcal{Y} \in \mathscr{F} \Ob (f) }{
  \mathcal{Y} \in \GR f } = \GR f;
  \end{multline*}
  
  $(\mathsf{RLD})_{\Low} (\Low) g = \bigsqcup \setcond{
  \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X} }{
  \mathcal{X} \in \GR (\Low) g } = \bigsqcup
  \setcond{ \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X} }{
  \mathcal{X} \in \mathscr{F}(\Ob g),
  \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X}
  \sqsubseteq g } \sqsubseteq g$.
\end{proof}

\begin{cor}
  ~
  \begin{enumerate}
    \item $(\mathsf{RLD})_{\Low} \bigsqcup S = \bigsqcup \langle
    (\mathsf{RLD})_{\Low} \rangle^{\ast} S$;
    
    \item $(\Low) \bigsqcap S = \bigsqcap \langle (\Low)
    \rangle^{\ast} S$.
  \end{enumerate}
\end{cor}

Below it's proved that $(\Low)$ and $(\mathsf{RLD})_{\Low}$ can be restricted to completely almost sub-join spaces and symmetrically transitive reloids.
Thus they preserve joins of (completely) almost sub-join spaces and meets of symmetrically transitive reloids.
\fxwarning{Check.}
\fxwarning{Move it to be below the definition.}

\section{Lattices of low spaces}

\begin{prop}\label{ls-order2}
$\mu \sqsubseteq \nu \Leftrightarrow \forall \mathcal{X}\in\GR\mu \exists\mathcal{Y}\in\GR\nu: \mathcal{X}\sqsubseteq\mathcal{Y}$ for
low filter spaces (on the same set~$U$).
\end{prop}

\begin{proof}
~
\begin{description}
\item[$\Rightarrow$] $\mu \sqsubseteq \nu \Leftrightarrow \GR\mu\subseteq\GR\nu \Rightarrow
  \forall \mathcal{X}\in\GR\mu \exists\mathcal{Y}\in\GR\nu: \mathcal{X}=\mathcal{Y} \Rightarrow
  \forall \mathcal{X}\in\GR\mu \exists\mathcal{Y}\in\GR\nu: \mathcal{X}\sqsubseteq\mathcal{Y}$.
\item[$\Leftarrow$] Let $\forall \mathcal{X}\in\GR\mu \exists\mathcal{Y}\in\GR\nu: \mathcal{X}\sqsubseteq\mathcal{Y}$.
  Take $\mathcal{X}\in\GR\mu$. Then $\exists\mathcal{Y}\in\GR\nu: \mathcal{X}\sqsubseteq\mathcal{Y}$. Thus $\mathcal{X}\in\GR\nu$.
  So $\GR\mu\subseteq\GR\nu$ that is $\mu \sqsubseteq \nu$.
\end{description}
\end{proof}

\begin{obvious}
~
\begin{enumerate}
\item $(\mathsf{RLD})_{\Low}$ is an order embedding.
\item $(\Low)$ is an order homomorphism.
\end{enumerate}
\end{obvious}

I will denote $\bigsqcup$, $\bigsqcap$, $\sqcup$, $\sqcap$ the lattice operations on low spaces or graphs of low spaces.

\begin{prop}
$\bigsqcup S=\bigcup S$ for every set~$S$ of graphs of low spaces on some set.
\end{prop}

\begin{proof}
It's enough to prove that there is a low space~$\mu$ such that $\GR\mu=\bigcup S$. In other words, it's enough to prove
that $\bigcup S$ is a nonempty lower set, but that's obvious. \fxwarning{A little more detailed proof.}
\end{proof}

\begin{prop}
$\bigsqcap S=\setcond{\bigsqcap\im P}{P\in\prod_{X\in S} X}$ for every set~$S$ of graphs of low spaces on some set.
\end{prop}

\begin{proof}
First prove that there is such low space~$\mu$ that $\mu=\setcond{\bigsqcap\im P}{P\in\prod_{X\in S} X}$. In other words,
we need to prove that $\setcond{\bigsqcap\im P}{P\in\prod_{X\in S} X}$ is a nonempty lower set. That it is nonempty is obvious.
Let filter $\mathcal{G}\sqsubseteq\mathcal{F}$ and $\mathcal{F}\in\setcond{\bigsqcap\im P}{P\in\prod_{X\in S} X}$. Then
$\mathcal{F}=\bigsqcap\im P$ for a $P\in\prod_{X\in S} X$ that is $P(X)\in X$ for every $X\in S$. Take $P'=(\mathcal{G}\sqcap)\circ P$.
Then $P'\in\prod_{X\in S} X$ because $P'(X)\in X$ for every $X\in S$ and thus
obviously $\mathcal{G}=\bigsqcap\im P'$ and thus $\mathcal{G}\in\setcond{\bigsqcap\im P}{P\in\prod_{X\in S} X}$. So such~$\mu$ exists.

It remains to prove that $\mu$ is the greatest lower bound of~$S$.

$\mu$ is a lower bound of~$S$. Really, let $X\in S$ and $Y\in X$.
Then exists $P\in\prod_{X\in S} X$ such that $P(X)=Y$ (taken into account that every $ X$ is nonempty)
and thus $\im P\ni Y$ and so $\bigsqcap\im P\sqsubseteq Y$, that is (proposition~\ref{ls-order2}) $\mu\sqsubseteq X$.

Let $\nu$ be a lower bound of~$S$. It remains to prove that $\mu\sqsupseteq\nu$, that is
$\forall Q\in\nu: Q=\bigsqcap\im P$ for some $P\in\prod_{X\in S} X$.
Take $P=(\mylambda{X}{S}{Q})$. This $P\in\prod_{X\in S} X$ because $Q\in X$ for every~$X\in S$.
\end{proof}

\begin{cor}
$f\sqcap g = \setcond{F\sqcap G}{F\in f,G\in g}$ for every graphs~$f$ and~$g$ of low spaces (on some set).
\end{cor}

\subsection{Its subsets}

\begin{prop}
The set of sub-join low spaces (on some fixed set) is meet-closed in the lattice of low spaces on a set.
\end{prop}

\begin{proof}
Let $f$, $g$ be graphs of almost sub-join spaces (on some fixed set), $f\sqcap g = \setcond{F\sqcap G}{F\in f,G\in g}$.

If $\mathcal{A}, \mathcal{B} \in f\sqcap g$ and $\mathcal{A}
\nasymp \mathcal{B}$, then $\mathcal{A}, \mathcal{B} \in f$ and $\mathcal{A}, \mathcal{B} \in g$.
Thus $\mathcal{A}\sqcup\mathcal{B}\in f$ and $\mathcal{A}\sqcup\mathcal{B}\in g$ and so
$\mathcal{A} \sqcup \mathcal{B} \in f\sqcap g$.
\end{proof}

\begin{cor}
The set of Cauchy spaces (on some fixed set), is meet-closed in the lattice of low spaces on a set.
\end{cor}

\begin{prop}
The set of completely almost sub-join spaces is meet-closed in the lattice of low spaces on a set.
\end{prop}

\begin{proof}
Let $S$~be a set of graphs of almost completely sub-join low spaces (on some fixed set). $ \bigsqcap S = \setcond{ \bigsqcap
\im P }{ P \in \prod_{X \in S}  X}$.

If $\mathcal{A}, \mathcal{B} \in  \bigsqcap S$ and $\mathcal{A}
\nasymp \mathcal{B}$, then $\mathcal{A}, \mathcal{B} \in  X$ for
every $X \in S$. Thus $\mathcal{A} \sqcup \mathcal{B} \in  X$ and so
$\mathcal{A} \sqcup \mathcal{B} \in  \bigsqcap S$.
\end{proof}

\begin{cor}
The set of completely Cauchy spaces is meet-closed in the lattice of low spaces on a set.
\end{cor}

From the above it follows:

\begin{obvious}
The following sets are complete lattices in our order:
\begin{enumerate}
\item almost sub-join spaces, whose graphs are almost sub-join-semilattices;
\item completely almost sub-join spaces;
\item reflexive low spaces;
\item precauchy spaces;
\item Cauchy spaces;
\item completely Cauchy spaces.
\end{enumerate}
\end{obvious}

Denote $Z(f)=\setcond{F\sqcup G}{F\in f,G\in f,F\nasymp G}\cup\{\bot\}$ for every set $f$ of filters (on some fixed set).

\begin{prop}
$Z(f)\sqsupseteq f$ for every set $f$ of filters.
\end{prop}

\begin{proof}
Consider for $F\in f$ both cases $F=\bot$ and $F\ne\bot$.
\end{proof}

\begin{lem}
For graphs of low spaces~$f$, $g$ (on the same set)
\[
Q = \bigcup S\cup Z\left(\bigcup S\right)\cup Z\left(Z\left(\bigcup S\right)\right)\cup\dots
\]
is a graph of some almost sub-join space.
\end{lem}

\begin{proof}
That it is nonempty and a lower set of filters is obvious. It remains to prove that it is an almost sub-join-semilattice.

Let $\mathcal{A},\mathcal{B}\in Q$ and $\mathcal{A}\nasymp\mathcal{B}$.
Then
\[
\mathcal{A},\mathcal{B} \in \underbrace{Z\dots Z}_{n\text{ times}}\left(\bigcup S\right)
\]
for a natural~$n$. Thus
\[
\mathcal{A}\sqcup\mathcal{B} \in \underbrace{Z\dots Z}_{n+1\text{ times}}\left(\bigcup S\right)
\]
and so $\mathcal{A}\sqcup\mathcal{B}\in Q$.
\end{proof}

\begin{prop}
Join on the lattice of graphs of almost sub-join spaces is described by the formula
\[
\bigsqcup^{\mathbf{ASJ}}S = \bigcup S\cup Z\left(\bigcup S\right)\cup Z\left(Z\left(\bigcup S\right)\right)\cup\dots
\]
\end{prop}

\begin{proof}
The right part of the above formula~$\mu$ is a graph of an almost sub-join space (lemma).

That $\mu$ is an upper bound of $S$ is obvious.

It remains to prove that $\mu$ is the least upper bound.

Suppose $\nu$~is an upper bound of $S$. Then $\nu\supseteq\bigcup S$. Thus, because $\nu$ is an almost sub-join-semilattice,
$Z(\nu)\subseteq\nu$, likewise $Z(Z(\nu))\subseteq\nu$, etc. Consequently $Z(\bigcup S)\subseteq\nu$, $Z(Z(\bigcup S))\subseteq\nu$, etc.
So we have $\mu\sqsubseteq\nu$.
\end{proof}

\begin{prop}
~ \fxnote{Should be merged with the previous proposition.}
\[
\bigsqcup^{\mathbf{ASJ}}S =
\setcond{F_0\sqcup\dots\sqcup F_{n-1}}{F_0,\dots,F_{n-1}\in\bigcup S,F_0\nasymp F_1\land F_1\nasymp F_2\land\dots\land F_{n-2}\nasymp F_{n-1} \text{ for } n\in\mathbb{N}}.
\]
\end{prop}

\begin{rem}
We take $F_0\sqcup\dots\sqcup F_{n-1} = \bot$ for $n=0$.
\end{rem}

\begin{proof}
Denote the right part of the above formula as~$R$.

Suppose $F\in R$. Let's prove by induction that $F\in Q$. If $F=\bot$ that's obvious. Suppose we know that
$F_0\sqcup\dots\sqcup F_{n-1}\in Q$ that is for a natural~$m$
\[F_0\sqcup\dots\sqcup F_{n-1}\in \underbrace{Z\dots Z}_{m\text{ times}}\left(\bigcup S\right)\]
for $F_0,\dots,F_{n-1}\in\bigcup S$, $F_0\nasymp F_1\land F_1\nasymp F_2\land\dots\land F_{n-2}\nasymp F_{n-1}$
and also $F_{n-1}\nasymp F_n$. Then $F_0\sqcup\dots\sqcup F_{n-1}\nasymp F_n$ and thus
$F_0\sqcup\dots\sqcup F_{n-1}\sqcup F_n\in \underbrace{Z\dots Z}_{m+1\text{ times}}\left(\bigcup S\right)$ that is
$F_0\sqcup\dots\sqcup F_{n-1}\sqcup F_n\in Q$. So $F\in Q$ for every~$F\in R$.

Now suppose $F\in Q$ that is for a natural~$m$
\[F \in \underbrace{Z\dots Z}_{m\text{ times}}\left(\bigcup S\right).\]
Let's prove by induction that $F=F_0\sqcup\dots\sqcup F_{n-1}$ for some $F_0,\dots,F_{n-1}\in\bigcup S$
such that $F_0\nasymp F_1\land F_1\nasymp F_2\land\dots\land F_{n-2}\nasymp F_{n-1}$.
If $m=0$ then $F\in\bigcup S$ and our promise is obvious.
Let our statement holds for a natural~$m$. Prove that it holds for
\[F' \in \underbrace{Z\dots Z}_{m+1\text{ times}}\left(\bigcup S\right).\]
We have $F'=Z(F)$ for some $F=F_0\sqcup\dots\sqcup F_{n-1}$ where $F_0\nasymp F_1\land F_1\nasymp F_2\land\dots\land F_{n-2}\nasymp F_{n-1}$.
The case $F'=\bot$ is easy. So we can assume $F'=A\sqcup B$ where $A,B\in F$ and $A\nasymp B$.
By the statement of induction $A=A_0\sqcup\dots\sqcup A_{p-1}$, $B=B_0\sqcup\dots\sqcup B_{q-1}$ for natural~$p$ and~$q$,
where $A_0\nasymp A_1\land A_1\nasymp A_2\land\dots\land A_{p-2}\nasymp A_{p-1}$,
$B_0\nasymp B_1\land B_1\nasymp B_2\land\dots\land B_{n-2}\nasymp B_{n-1}$.
Take $j$ such that $A\nasymp B_j$ and then take $i$ such that $A_i\nasymp B_j$.
Then (using symmetry of the relation~$\nasymp$) we have
$(A_0\nasymp A_1\land A_1\nasymp A_2\land\dots\land A_{p-2}\nasymp A_{p-1}) \land
(A_{p-1} \nasymp A_{p-2} \nasymp \dots A_{i+1} \nasymp A_i) \land A_i \nasymp B_j \land
(B_j \nasymp B_{j-1} \land \dots \land B_1\nasymp B_0) \land
(B_0\nasymp B_1\land B_1\nasymp B_2\land\dots\land B_{q-2}\nasymp B_{q-1})$.
So $F'=A\sqcup B$ is representable as the join of a finite sequence of filters with each adjacent pair of filters in this sequence being intersecting.
That is $F'\in Q$.
\end{proof}

\begin{prop}
The lattice of Cauchy spaces (on some set) is a complete sublattice of the lattice of almost sub-join spaces.
\end{prop}

\begin{proof}
It's obvious, taking into account obvious~\ref{cs-refl-by-id}.
\end{proof}

Denote $Z_{\infty}(f)=\setcond{\bigsqcup T}{T\in\subsets f\land\bigsqcap T\ne\bot}\cup\{\bot\}$.

\begin{prop}
$Z_{\infty}(f)\sqsupseteq f$.
\end{prop}

\begin{proof}
Consider for $F\in f$ both cases $F=\bot$ and $F\ne\bot$.
\end{proof}

\begin{lem}
If $S$ is a set of graphs of low spaces, then
\[
Q = \bigcup S \cup Z_{\infty}\left(\bigcup S\right) \cup Z_{\infty}\left(Z_{\infty}\left(\bigcup S\right)\right) \cup \dots
\]
is a graph of a completely Cauchy space.
\end{lem}

\begin{proof}
That it is nonempty and a lower set of filters is obvious. It remains to prove that it is a completely almost sub-join-semilattice.

Let $T\in\subsets Q$ and $\bigsqcap T\ne\bot$.
Then
\[
T\in\subsets \underbrace{Z_{\infty}\dots Z_{\infty}}_{n\text{ times}}\left(\bigcup S\right)
\]
for a natural~$n$. Thus
\[
T\in\subsets \underbrace{Z_{\infty}\dots Z_{\infty}}_{n+1\text{ times}}\left(\bigcup S\right)
\]
and so $\bigsqcup T\in Q$.
\end{proof}

\begin{prop}
The lattice of completely Cauchy spaces (on some set) is a complete sublattice of the lattice of completely almost sub-join spaces.
\end{prop}

\begin{proof}
It's obvious, taking into account obvious~\ref{cs-refl-by-id}.
\end{proof}

\begin{prop}
Join of a set~$S$ on the lattice of graphs of completely almost sub-join-semilattice is described by the formula:
\[
\bigsqcup^{\mathbf{CASJ}}S=\bigcup S \cup Z_{\infty}\left(\bigcup S\right) \cup Z_{\infty}\left(Z_{\infty}\left(\bigcup S\right)\right) \cup \dots
\]
\end{prop}

\begin{proof}
The right part of the above formula~$\mu$ is a graph of an almost sub-join space (lemma).

That $\mu$ is an upper bound of $S$ is obvious.

It remains to prove that $\mu$ is the least upper bound.

Suppose $\nu$~is an upper bound of $S$. Then $\nu\supseteq\bigcup S$. Thus, because $\nu$ is an almost sub-join-semilattice,
$Z_{\infty}(\nu)\subseteq\nu$, likewise $Z_{\infty}(Z_{\infty}(\nu))\subseteq\nu$, etc. Consequently $Z_{\infty}(\bigcup S)\subseteq\nu$, $Z_{\infty}(Z_{\infty}(\bigcup S))\subseteq\nu$, etc.
So we have $\mu\sqsubseteq\nu$.
\end{proof}

\begin{conjecture}
~
\begin{enumerate}
\item $\bigsqcup^{\mathbf{CASJ}}S=
\setcond{\bigsqcup T_0\sqcup\dots\sqcup\bigsqcup T_{n-1}}{
\begin{aligned}
&n\in\mathbb{N},T_0,\dots,T_{n-1}\in\bigcup S, \\
&\bigsqcap T_0\ne\bot\land\dots\land\bigsqcap T_{n-1}\ne\bot, \\
&\bigsqcup T_0\nasymp\bigsqcup T_1\land\dots\land\bigsqcup T_{n-2}\nasymp\bigsqcup T_{n-1}.
\end{aligned}}$;

\item $\bigsqcup^{\mathbf{CASJ}}S=
\setcond{\bigsqcup T_0\sqcup \bigsqcup T_1\sqcup\dots}{
\begin{aligned}
&T_0,T_1,\dots\in\bigcup S, \\
&\bigsqcap T_0\ne\bot\land\bigsqcap T_2\ne\bot\land\dots,
\bigsqcup T_0\nasymp\bigsqcup T_1\land\bigsqcup T_1\nasymp\bigsqcup T_2\land\dots
\end{aligned}}$.
\end{enumerate}
\end{conjecture}

\section{Up-complete low spaces}

\begin{defn}
  \emph{Ideal base} is a nonempty subset $S$ of a poset such that $\forall
  a, b \in S \exists c \in S : (a, b \sqsubseteq c)$.
\end{defn}

\begin{obvious}
Ideal base is dual of filter base.
\end{obvious}

\begin{thm}
  Product of nonempty posets is a ideal base iff every factor is an ideal
  base.
\end{thm}

\begin{proof}
  \fxwarning{more detailed proof}
  
  In one direction it is easy: Suppose one multiplier is not a dcpo. Take a
  chain with fixed elements (thanks our posets are nonempty) from other
  multipliers and for this multiplier take the values which form a chain
  without the join. This proves that the product is not a dcpo.
  
  Let now every factor is dcpo. $S$ is a filter base in $\prod \mathfrak{A}$
  iff each component is a filter base. Each component has a join. Thus by proposition~\bookref{cw-join} $S$ has a componentwise join.
\end{proof}

\begin{defn}
  I call a low space \emph{up-complete} when each ideal base (or
  equivalently every nonempty chain, see theorem~\bookref{fclosed}) in this space has join in
  this space.
\end{defn}

\begin{rem}
  Elements of this ideal base are filters. (Thus is could be called a
  generalized ideal base.)
\end{rem}

\begin{example}
  ~  
  \begin{enumerate}
    \item $\setcond{ \mathcal{X} \in \mathfrak{F} ]0 ; + \infty[ }{
    \exists \varepsilon > 0 : \mathcal{X} \sqsubseteq \uparrow
    ]\varepsilon ; + \infty[ } \cup \uparrow\{ 0 \}$ is a graph of Cauchy space
    on $\mathbb{R}_+$, but not up-complete.
    
    \item $\mathfrak{F} [0 ; + \infty[$ is a strictly greater graph of Cauchy
    space on $\mathbb{R}_+$ and is up-complete.
  \end{enumerate}
\end{example}

\begin{lem}
  Let $f$ be a reloid. Each ideal base $T \subseteq \setcond{ (\mathcal{A} ,
  \mathcal{B}) }{ \mathcal{A}
  \times^{\mathsf{RLD}} \mathcal{B} \sqsubseteq f }$ has a join
  in this set.
\end{lem}

\begin{proof}
  Let $T$ be an ideal base and $\forall (\mathcal{A} , \mathcal{B}) \in T :
  \mathcal{A} \times^{\mathsf{FCD}} \mathcal{B} \sqsubseteq f$.
  
  $\forall (\mathcal{A} , \mathcal{B}) \in T \forall \mathcal{X} \in
  \mathscr{F} \Src f : (\mathcal{X} \nasymp \mathcal{A} \Rightarrow
  \mathcal{B} \sqsubseteq \supfun{f} \mathcal{X})$;
  
  taking join we have:
  
  $\forall \mathcal{A} \in \Pr_0 T \forall \mathcal{X} \in \mathscr{F}
  \Src f : \left( \mathcal{X} \nasymp \mathcal{A} \Rightarrow
  \bigsqcup_{\mathcal{B} \in \Pr_1 T} \mathcal{B} \sqsubseteq \langle f
  \rangle \mathcal{X} \right)$;
  
  $\forall \mathcal{A} \in \Pr_0 T : \mathcal{A} \times^{\mathsf{FCD}}
  \bigsqcup_{\mathcal{B} \in \Pr_1 T} \mathcal{B} \sqsubseteq f$.
  
  Now repeat a similar operation second time:
  
  $\forall \mathcal{A} \in \Pr_0 T : \bigsqcup_{\mathcal{B} \in \Pr_1 T}
  \mathcal{B} \times^{\mathsf{FCD}} \mathcal{A} \sqsubseteq f^{- 1}$;
  
  $\forall \mathcal{A} \in \Pr_0 T \forall \mathcal{Y} \in \mathscr{F}
  \Dst f : \left( \mathcal{Y} \nasymp \bigsqcup_{\mathcal{B} \in \Pr_1
  T} \mathcal{B} \Rightarrow \mathcal{A} \sqsubseteq \langle f^{- 1} \rangle
  \mathcal{Y} \right)$;
  
  $\forall \mathcal{Y} \in \mathscr{F} \Dst f : \left( \mathcal{Y}
  \nasymp \bigsqcup_{\mathcal{B} \in \Pr_1 T} \mathcal{B} \Rightarrow
  \bigsqcup_{\mathcal{A} \in \Pr_0 T} \mathcal{A} \sqsubseteq \langle f^{- 1}
  \rangle \mathcal{Y} \right)$;
  
  $\bigsqcup_{\mathcal{B} \in \Pr_1 T} \mathcal{B}
  \times^{\mathsf{FCD}} \bigsqcup_{\mathcal{A} \in \Pr_0 T} \mathcal{A}
  \sqsubseteq f^{- 1}$;
  
  $\bigsqcup_{\mathcal{A} \in \Pr_0 T} \mathcal{A}
  \times^{\mathsf{FCD}} \bigsqcup_{\mathcal{B} \in \Pr_1 T} \mathcal{B}
  \sqsubseteq f$. But $\bigsqcup_{\mathcal{A} \in \Pr_0 T} \mathcal{A}
  \times^{\mathsf{FCD}} \bigsqcup_{\mathcal{B} \in \Pr_1 T}
  \mathcal{B}$ is the join in consideration, because ideal base is ideal base
  in each argument.
\end{proof}

\begin{prop}
  A Cauchy space generated by an endoreloid is always up-complete.
\end{prop}

\begin{proof}
  Let $f$ be an endoreloid. $\GR (\Low) f = \setcond{ \mathcal{X} \in
  \Ob f }{ \mathcal{X}
  \times^{\mathsf{RLD}} \mathcal{X} \sqsubseteq f }$.

  Let $T\subseteq \setcond{ \mathcal{X} \in \Ob f }{ \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X} \sqsubseteq f }$
  be an ideal base.
  
  Then $N = \setcond{(\mathcal{F},\mathcal{F})}{\mathcal{F}\in T}$ is also an ideal base.
  Obviously $N \subseteq \setcond{ (\mathcal{A} , \mathcal{B}) }{ \mathcal{A} \times^{\mathsf{RLD}} \mathcal{B} \sqsubseteq f }$.
  Thus by the lemma it has a join in
  $\setcond{ (\mathcal{A} , \mathcal{B}) }{ \mathcal{A} \times^{\mathsf{RLD}} \mathcal{B} \sqsubseteq f }$.
  It's easy to see that this join is in
  $\setcond{ (\mathcal{A} , \mathcal{A}) }{ \mathcal{A}\in\Ob f, \mathcal{A} \times^{\mathsf{RLD}} \mathcal{A} \sqsubseteq f }$.
  Consequently $T$ has a join in $\setcond{ \mathcal{X} \in \Ob f }{ \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X} \sqsubseteq f }$.
\end{proof}

It is long time known that (using our terminology) low space induced by a
uniform space is a Cauchy space, but that it is complete and up-complete is
probably first discovered by Victor Porton.

\section{More on Cauchy filters}

\begin{obvious}
Low filter on an endoreloid $\nu$ is a filter $\mathcal{F}$ such that
\[ \forall U \in \GR f \exists A \in \mathcal{F} : A \times A \subseteq
   U. \]
\end{obvious}

\begin{rem}
  The above formula is the standard definition of Cauchy filters on uniform
  spaces.
\end{rem}

\begin{prop}
  If $\nu \sqsupseteq \nu \circ \nu^{- 1}$ then every neighborhood filter is a
  Cauchy filter, that it
  \[ \nu \sqsupseteq \rsupfun{\tofcd \nu} \{ x \}
     \times^{\mathsf{RLD}} \rsupfun{\tofcd \nu} \{ x \} \]
  for every point $x$.
\end{prop}

\begin{proof}
  $\rsupfun{\tofcd \nu} \{ x \}
  \times^{\mathsf{RLD}} \rsupfun{\tofcd \nu} \{ x \} = \supfun{\tofcd \nu}
  \uparrow^{\Ob \nu} \left\{ x \right\} \times^{\mathsf{RLD}}
  \supfun{\tofcd \nu} \uparrow^{\Ob \nu} \{ x \} =
  \nu \circ (\uparrow^{\Ob \nu} \{ x \} \times^{\mathsf{RLD}}
  \uparrow^{\Ob \nu} \{ x \}) \circ \nu^{- 1} = \nu \circ
  (\uparrow^{\mathsf{RLD} (\Ob \nu , \Ob \nu)} \{ (x , x)
  \}) \circ \nu^{- 1} \sqsubseteq \nu \circ \id^{\mathsf{RLD}
  (\Ob \nu , \Ob \nu)} \circ \nu^{- 1} = \nu \circ \nu^{- 1}
  \sqsubseteq \nu$.
\end{proof}

\begin{prop}
  If $\nu \sqsupseteq \nu \circ \nu^{- 1}$ a filter converges (in~$\nu$) to a point, it is a low filter, provided that every
  neighborhood filter is a low filter.
\end{prop}

\begin{proof}
  Let $\mathcal{F} \sqsubseteq \rsupfun{\tofcd \nu} \{ x \}$. Then $\mathcal{F} \times^{\mathsf{RLD}}
  \mathcal{F} \sqsubseteq \rsupfun{\tofcd \nu} \{
  x \} \times^{\mathsf{RLD}} \rsupfun{\tofcd \nu} \{ x \} \sqsubseteq \nu$.
\end{proof}

\begin{cor}
  If a filter converges to a point, it is a low filter, provided that $\nu
  \sqsupseteq \nu \circ \nu^{- 1}$.
\end{cor}

\section{Maximal Cauchy filters}

\begin{lem}
  Let $S$ be a set of sets with $\bigsqcap \rsupfun{ \uparrow^{\mathfrak{F}} }
  S \neq 0^{\mathfrak{F}}$ (in other words, $S$ has finite
  intersection property). Let $T = \setcond{ X \times X}
  {X \in S }$. Then
  \[ \bigcup T \circ \bigcup T = \bigcup S \times \bigcup S. \]
\end{lem}

\begin{proof}
  Let $x \in \bigcup S$. Then $x \in X$ for some $X \in S$. $\left\langle
  \bigcup T \right\rangle \{ x \} \sqsupseteq \uparrow X \supseteq \bigcap S
  \neq \emptyset$. Thus
  
  $\left\langle \bigcup T \circ \bigcup T \right\rangle \{ x \} = \left\langle
  \bigcup T \right\rangle \left\langle \bigcup T \right\rangle \{ x \} \in
  \left\langle \uparrow^{\mathsf{FCD}} \bigcup T \right\rangle
  \bigsqcap \langle \uparrow^{\mathfrak{F}} \rangle S \sqsupseteq \bigsqcup
  \setcond{ \langle \uparrow^{\mathsf{FCD}} (X \times X) \rangle
  \bigsqcap \langle \uparrow^{\mathfrak{F}} \rangle S }{
  X \in S } = \bigsqcup \setcond{ \uparrow^{\mathfrak{F}} X}{X \in S } =
  \bigsqcup \langle
  \uparrow^{\mathfrak{F}} \rangle S$ that is $\left\langle \bigcup T \circ
  \bigcup T \right\rangle \{ x \} \supseteq \bigcup S$.
\end{proof}

\begin{cor}
  Let $S$ be a set of filters (on some fixed set) with nonempty meet. Let
  \[ T = \setcond{ \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X} }
     {\mathcal{X} \in S} \]
  Then
  \[ \bigsqcup T \circ \bigsqcup T = \bigsqcup S \times^{\mathsf{RLD}}
     \bigsqcup S. \]
\end{cor}

\begin{proof}
  $\bigsqcup T \circ \bigsqcup T = \bigsqcap \setcond{ \uparrow^{\mathfrak{F}}
  (X \circ X) }{ X \in \bigsqcup T }$.
  
  If $X \in \bigsqcup T$ then $X = \bigcup_{Q \in T} (P_Q \times P_Q)$ where
  $P_Q \in Q$. Therefore by the lemma we have
  \[ \bigcup \setcond{ P_Q \times P_Q}{Q \in T} \circ \bigcup
  \setcond{ P_Q \times P_Q}{ Q \in T } = \bigcup_{Q \in T} P_Q \times \bigcup_{Q \in T} P_Q .
  \]
  Thus $X \circ X = \bigcup_{Q \in T} P_Q \times \bigcup_{Q \in T} P_Q$.
  
  Consequently $\bigsqcup T \circ \bigsqcup T = \bigsqcap \setcond{
  \uparrow^{\mathfrak{F}} \left( \bigcup_{Q \in T} P_Q \times \bigcup_{Q \in
  T} P_Q \right)}{X \in \bigsqcup T }
  \sqsupseteq \bigsqcup S \times^{\mathsf{RLD}} \bigsqcup S$.
  
  $\bigsqcup T \circ \bigsqcup T \sqsubseteq \bigsqcup S
  \times^{\mathsf{RLD}} \bigsqcup S$ is obvious.
\end{proof}

\begin{defn}
  I call an endoreloid $\nu$ \emph{symmetrically transitive} iff for every
  symmetric endofuncoid $f \in \mathsf{FCD} (\Ob \nu , \Ob
  \nu)$ we have $f \sqsubseteq \nu \Rightarrow f \circ f \sqsubseteq \nu$.
\end{defn}

\begin{obvious}
  It is symmetrically transitive if at least one of the following holds:
  \begin{enumerate}
    \item $\nu \circ \nu \sqsubseteq \nu$;
    
    \item $\nu \circ \nu^{- 1} \sqsubseteq \nu$;
    
    \item $\nu^{- 1} \circ \nu \sqsubseteq \nu$.
    
    \item $\nu^{- 1} \circ \nu^{- 1} \sqsubseteq \nu$.
  \end{enumerate}
\end{obvious}

\begin{cor}
  Every uniform space is symmetrically transitive.
\end{cor}

\begin{prop}
  $(\Low) \nu$ is a completely Cauchy space for every symmetrically
  transitive endoreloid $\nu$.
\end{prop}

\begin{proof}
  Suppose $S \in \subsets \setcond{ \mathcal{X} \in \mathfrak{F} }{ \mathcal{X}
  \times^{\mathsf{RLD}} \mathcal{X} \sqsubseteq \nu }$.
  
  $\bigsqcup \setcond{ \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X}}
  {\mathcal{X} \in S } \sqsubseteq \nu$;
  $\bigsqcup \setcond{ \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X}}
  {\mathcal{X} \in S } \circ \bigsqcup
  \setcond{ \mathcal{X} \times^{\mathsf{RLD}} \mathcal{X} }
  {\mathcal{X} \in S} \sqsubseteq \nu$; $\bigsqcup S
  \times^{\mathsf{RLD}} \bigsqcup S \sqsubseteq \nu$ (taken into
  account that $S$ has nonempty meet). Thus $\bigsqcup S$ is Cauchy.
\end{proof}

\begin{prop}
  The neighbourhood filter $\langle \tofcd \nu \rangle^{\ast} \{
  x \}$ of a point $x \in \Ob \nu$ is a maximal Cauchy filter, if it is a
  Cauchy filter and $\nu$ is a reflexive reloid.
  \fxnote{Does it holds for all low filters?}
\end{prop}

\begin{proof}
  Let $\mathscr{N} = \langle \tofcd \nu \rangle^{\ast} \{ x
  \}$. Let $\mathscr{C \sqsupseteq N}$ be a Cauchy filter. We need to show
  $\mathscr{N \sqsupseteq C}$.
  
  Since $\mathscr{C}$ is Cauchy filter, $\mathscr{C}
  \times^{\mathsf{RLD}} \mathscr{C} \sqsubseteq \nu$. Since $\mathscr{C
  \sqsupseteq N}$ we have $\mathscr{C}$ is a neighborhood of $x$ and thus
  $\uparrow^{\Ob \nu} \{ x \} \sqsubseteq \mathscr{C}$ (reflexivity of
  $\nu$). Thus $\uparrow^{\Ob \nu} \{ x \} \times^{\mathsf{RLD}}
  \mathscr{C} \sqsubseteq \mathscr{C} \times^{\mathsf{RLD}}
  \mathscr{C}$ and hence $\uparrow^{\Ob \nu} \{ x \}
  \times^{\mathsf{RLD}} \mathscr{C} \sqsubseteq \nu$;
  \[ \mathscr{C} \sqsubseteq \im (\nu |_{\uparrow^{\Ob \nu} \{ x
     \}}) = \langle \tofcd \nu \rangle^{\ast} \{ x \} =
     \mathscr{N} . \]
\end{proof}

\section{Cauchy continuous functions}

\begin{defn}
  A function $f : U \rightarrow V$ is \emph{Cauchy continuous} from a low
  space $\left( U , \mathscr{C} \right)$ to a low space
  $\left( V , \mathscr{D} \right)$ when $\forall \mathcal{X} \in \mathscr{C} :
  \langle \uparrow^{\mathsf{FCD}} f \rangle \mathcal{X} \in
  \mathscr{D}$.
\end{defn}

\begin{prop}
  Let $f$ be a principal reloid. Then $f \in \mathrm{C} \left( 
  (\mathsf{RLD})_{\Low} \mathscr{C} ,
  (\mathsf{RLD})_{\Low} \mathscr{D} \right)$ iff $f$ is Cauchy
  continuous.
  \begin{eqnarray*}
    f \circ (\mathsf{RLD})_{\Low} \mathscr{C} \circ f^{- 1}
    \sqsubseteq (\mathsf{RLD})_{\Low} \mathscr{D} &
    \Leftrightarrow & \\
    \bigsqcup_{\mathcal{X} \in
    \mathscr{C}} (f \circ (\mathcal{X} \times^{\mathsf{RLD}}
    \mathcal{X} ) \circ f^{- 1} ) \sqsubseteq (\mathsf{RLD})_{\Low}
    \mathscr{D} & \Leftrightarrow & \\
    \bigsqcup_{\mathcal{X} \in \mathscr{C}} ( \langle \uparrow^{\mathsf{FCD}} f \rangle
    \mathcal{X} \times^{\mathsf{RLD}} \langle
    \uparrow^{\mathsf{FCD}} f \rangle \mathcal{X}) \sqsubseteq
    (\mathsf{RLD})_{\Low} \mathscr{D} & \Leftrightarrow & \\
    \forall \mathcal{X} \in \mathscr{C} : \langle
    \uparrow^{\mathsf{FCD}} f \rangle \mathcal{X}
    \times^{\mathsf{RLD}} \langle \uparrow^{\mathsf{FCD}} f
    \rangle \mathcal{X} \sqsubseteq (\mathsf{RLD})_{\Low}
    \mathscr{D} & \Leftrightarrow & \\
    \forall \mathcal{X} \in \mathscr{C} : \langle
    \uparrow^{\mathsf{FCD}} f \rangle \mathcal{X} \in \mathscr{D} . & 
    & 
  \end{eqnarray*}
\end{prop}

Thus we have expressed Cauchy properties through the algebra of reloids.

\section{Cauchy-complete reloids}

\begin{defn}
  An endoreloid $\nu$ is \emph{Cauchy-complete} iff every low filter for
  this reloid converges to a point.
\end{defn}

\begin{rem}
  In my book \cite{volume-1} \emph{complete reloid} means something
  different. I will always prepend the word ``Cauchy'' to the word
  ``complete'' when meaning is by the last definition.
\end{rem}

\url{https://en.wikipedia.org/wiki/Complete\_uniform\_space\#Completeness}

\section{Totally bounded}

\url{http://ncatlab.org/nlab/show/Cauchy+space}

\begin{defn}
  Low space is called \emph{totally bounded} when every proper filter
  contains a proper Cauchy filter.
\end{defn}

\begin{obvious}
A reloid $\nu$ is totally bounded iff
\[ \forall X \in \subsets \Ob \nu \exists \mathcal{X} \in
   \mathfrak{F}^{\Ob \nu} : (\bot \neq \mathcal{X} \sqsubseteq
   \uparrow^{\Ob \nu} X \wedge \mathcal{X} \times^{\mathsf{RLD}}
   \mathcal{X} \sqsubseteq \nu) . \]
\end{obvious}

\begin{thm}
  A symmetric transitive reloid is totally bounded iff its Cauchy space is
  totally bounded.
\end{thm}

\begin{proof}~
  
  \begin{description}
    \item[$\Rightarrow$] Let $\mathcal{F}$ be a proper filter on $\Ob
    \nu$ and let $a \in \atoms \mathcal{F}$. It's enough to prove that
    $a$ is Cauchy.
    
    Let $D \in \GR \nu$. Let also $E \in \GR \nu$ is symmetric
    and $E \circ E \subseteq D$. There existsa finite subset $F \subseteq
    \Ob \nu$ such that $\langle E \rangle F = \Ob \nu$. Then
    obviously exists $x \in F$ such that $a \sqsubseteq \uparrow^{\Ob
    \nu} \langle E \rangle \{ x \}$, but $\langle E \rangle \{ x \} \times
    \langle E \rangle \{ x \} = E^{- 1} \circ (\{ x \} \times \{ x \}) \circ E
    \subseteq D$, thus $a \times^{\mathsf{RLD}} a \sqsubseteq
    \uparrow^{\mathsf{RLD} (\Ob \nu , \Ob \nu)} D$.
    
    Because $D$ was taken arbitrary, we have $a \times^{\mathsf{RLD}} a
    \sqsubseteq \nu$ that is $a$ is Cauchy.
    
    \item[$\Leftarrow$] Suppose that Cauchy space associated with a reloid
    $\nu$ is totally bounded but the reloid $\nu$ isn't totally bounded. So
    there exists a $D \in \GR \nu$ such that $(\Ob \nu) \setminus
    \langle D \rangle F \neq \emptyset$ for every finite set $F$.
    
    Consider the filter base
    \[ S = \setcond{ (\Ob \nu) \setminus \langle D \rangle F}
       {F \in \subsets \Ob \nu, F \text{ is finite}
       } \]
    and the filter $\mathcal{F} = \bigsqcap \langle \uparrow^{\Ob \nu}
    \rangle S$ generated by this base. The filter $\mathcal{F}$ is proper
    because intersection $P \cap Q \in S$ for every $P, Q \in S$ and
    $\emptyset \notin S$. Thus there exists a Cauchy (for our Cauchy space)
    filter $\mathcal{X} \sqsubseteq \mathcal{F}$ that is $\mathcal{X}
    \times^{\mathsf{RLD}} \mathcal{X} \sqsubseteq \nu$.
    
    Thus there exists $M \in \mathcal{X}$ such that $M \times M \subseteq D$.
    Let $F$ be a finite subset of $\Ob \nu$. Then $(\Ob \nu)
    \setminus \langle D \rangle F \in \mathcal{F} \sqsupseteq \mathcal{X}$.
    Thus $M \nasymp (\Ob \nu) \setminus \langle D \rangle F$ and so
    there exists a point $x \in M \cap ((\Ob \nu) \setminus \langle D
    \rangle F)$.
    
    $\langle M \times M \rangle \{ p \} \subseteq \langle D \rangle \{ x \}$
    for every $p \in M$; thus $M \subseteq \langle D \rangle \{ x \}$.
    
    So $M \subseteq \langle D \rangle (F \cup \{ x \})$. But this means that
    $M \in \mathcal{X}$ does not intersect $(\Ob \nu) \setminus \langle
    D \rangle (F \cup \{ x \}) \in \mathcal{F} \sqsupseteq \mathcal{X}$, what
    is a contradiction (taken into account that $\mathcal{X}$ is proper).
  \end{description}
\end{proof}

\url{http://math.stackexchange.com/questions/104696/pre-compactness-total-boundedness-and-cauchy-sequential-compactness}

\section{Totally bounded funcoids}

\begin{defn}
  A funcoid $\nu$ is totally bounded iff
  \[ \forall X \in \Ob \nu \exists \mathcal{X} \in
     \mathfrak{F}^{\Ob \nu} : (0 \neq \mathcal{X} \sqsubseteq
     \uparrow^{\Ob \nu} X \wedge \mathcal{X}
     \times^{\mathsf{FCD}} \mathcal{X} \sqsubseteq \nu) . \]
\end{defn}

This can be rewritten in elementary terms (without using funcoidal product:

$\mathcal{X} \times^{\mathsf{FCD}} \mathcal{X} \sqsubseteq \nu
\Leftrightarrow \forall P \in \corestar \mathcal{X} : \mathcal{X} \sqsubseteq
\supfun{\nu} P \Leftrightarrow \forall P \in \corestar \mathcal{X}, Q
\in \corestar \mathcal{X} : P \mathrel{[\nu]^{\ast}} Q \Leftrightarrow \forall
P, Q \in \Ob \nu : \left( \forall E \in \mathcal{X} : (E \cap P \neq
\emptyset \wedge E \cap Q \neq \emptyset) \Rightarrow P \mathrel{[\nu]^{\ast}}
Q \right)$.

Note that probably I am the first person which has written the above formula
(for proximity spaces for instance) explicitly.

\section{On principal low spaces}

\begin{defn}
  A low space $\left( U , \mathscr{C} \right)$ is \emph{principal}
  when all filters in $\mathscr{C}$ are principal.
\end{defn}

\begin{prop}
  Having fixed a set $U$, principal reflexive low spaces on $U$
  bijectively correspond to principal reflexive symmetric endoreloids on $U$.
\end{prop}

\begin{proof}
  ??
  
  http://math.stackexchange.com/questions/701684/union-of-cartesian-squares
\end{proof}

\section{Rest}

\url{https://en.wikipedia.org/wiki/Cauchy\_filter\#Cauchy\_filters}

\url{https://en.wikipedia.org/wiki/Uniform\_space} ``Hausdorff completion of a
uniform space'' here)

\url{http://at.yorku.ca/z/a/a/b/13.htm} : the category $\mathbf{Prox}$ of proximity
spaces and proximally continuous maps (i.e. maps preserving nearness between
two sets) is isomorphic to the category of totally bounded uniform spaces (and
uniformly continuous maps).

\url{https://en.wikipedia.org/wiki/Cauchy\_space}
\url{http://ncatlab.org/nlab/show/Cauchy+space}

\url{http://arxiv.org/abs/1309.1748}

\url{http://projecteuclid.org/download/pdf\_1/euclid.pja/1195521991}

\url{http://www.emis.de/journals/HOA/IJMMS/Volume5\_3/404620.pdf}

\url{\~/math/books/Cauchy\_spaces.pdf}

\url{https://ncatlab.org/nlab/show/Cauchy+space} defines compact Cauchy spaces!

\url{http://www.hindawi.com/journals/ijmms/1982/404620/abs/} (open access article) describes criteria for a Cauchy space to be uniformizable.