chap-funcoids-are-filters.tex

\chapter{Funcoids are filters}\label{fcd-filters}

The motto of this chapter is: ``Funcoids are filters on a (boolean) lattice.''


\section{Rearrangement of collections of sets}

Let $Q$ be a set of sets.

Let $\equiv$ be the relation on $\bigcup Q$ defined by the formula
\[
a\equiv b\Leftrightarrow\forall X\in Q:(a\in X\Leftrightarrow b\in X).
\]

\begin{prop}
$\equiv$ is an equivalence relation on $\bigcup Q$.\end{prop}
\begin{proof}
~
\begin{description}
\item [{Reflexivity}] Obvious.
\item [{Symmetry}] Obvious.
\item [{Transitivity}] Let $a\equiv b\wedge b\equiv c$. Then $a\in X\Leftrightarrow b\in X\Leftrightarrow c\in X$
for every $X\in Q$. Thus $a\equiv c$.
\end{description}
\end{proof}
\begin{defn}
\emph{Rearrangement} $\mathfrak{R}(Q)$ of $Q$ is the set of equivalence
classes of $\bigcup Q$ for $\equiv$.\end{defn}
\begin{obvious}
$\bigcup\mathfrak{R}(Q)=\bigcup Q$.
\end{obvious}

\begin{obvious}
$\emptyset\notin\mathfrak{R}(Q)$.\end{obvious}
\begin{lem}
$\card\mathfrak{R}(Q)\leq2^{\card Q}$.\end{lem}
\begin{proof}
Having an equivalence class $C$, we can find the set $f\in\subsets Q$
of all $X\in Q$ such that $a\in X$, for every $a\in C$. 
\[
b\equiv a\Leftrightarrow\forall X\in Q:(a\in X\Leftrightarrow b\in X)\Leftrightarrow\forall X\in Q:(X\in f\Leftrightarrow b\in X).
\]
So $C=\setcond{b\in\bigcup Q}{b\equiv a}$ can be restored knowing
$f$. Consequently there are no more than $\card\subsets Q=2^{\card Q}$
classes.\end{proof}
\begin{cor}
If $Q$ is finite, then $\mathfrak{R}(Q)$ is finite.\end{cor}
\begin{prop}
If $X\in Q$, $Y\in\mathfrak{R}(Q)$ then $X\cap Y\neq\emptyset\Leftrightarrow Y\subseteq X$.\end{prop}
\begin{proof}
Let $X\cap Y\neq\emptyset$ and $x\in X\cap Y$. Then 
\[
y\in Y\Leftrightarrow x\equiv y\Leftrightarrow\forall X'\in Q:(x\in X'\Leftrightarrow y\in X')\Rightarrow(x\in X\Leftrightarrow y\in X)\Leftrightarrow y\in X
\]
 for every $y$. Thus $Y\subseteq X$.

$Y\subseteq X\Rightarrow X\cap Y\neq\emptyset$ because $Y\neq\emptyset$.\end{proof}
\begin{prop}
If $\emptyset\neq X\in Q$ then there exists $Y\in\mathfrak{R}(Q)$
such that $Y\subseteq X\wedge X\cap Y\neq\emptyset$.\end{prop}
\begin{proof}
Let $a\in X$. Then 
\begin{multline*}
[a]=\setcond{b\in\bigcup Q}{\forall X'\in Q:(a\in X'\Leftrightarrow b\in X')}\subseteq\\
\setcond{b\in\bigcup Q}{a\in X\Leftrightarrow b\in X} = \setcond{b\in\bigcup Q}{b\in X}=X.
\end{multline*}
But $[a]\in\mathfrak{R}(Q)$.

$X\cap Y\neq\emptyset$ follows from $Y\subseteq X$ by the previous
proposition.\end{proof}
\begin{prop}
If $X\in Q$ then $X=\bigcup(\mathfrak{R}(Q)\cap\subsets X)$.\end{prop}
\begin{proof}
$\bigcup(\mathfrak{R}(Q)\cap\subsets X)\subseteq X$ is obvious.

Let $x\in X$. Then there is $Y\in\mathfrak{R}(Q)$ such that $x\in Y$.
We have $Y\subseteq X$ that is $Y\in\subsets X$ by a proposition
above. So $x\in Y$ where $Y\in\mathfrak{R}(Q)\cap\subsets X$ and
thus $x\in\bigcup(\mathfrak{R}(Q)\cap\subsets X)$. We have $X\subseteq\bigcup(\mathfrak{R}(Q)\cap\subsets X)$.
\end{proof}

\section{Finite unions of Cartesian products}

Let $A$, $B$ be sets.

I will denote $\overline{X}=A\setminus X$.

Let denote $\Gamma(A,B)$ the set of all finite unions $X_{0}\times Y_{0}\cup\ldots\cup X_{n-1}\times Y_{n-1}$
of Cartesian products, \ where $n\in\mathbb{N}$ and $X_{i}\in\subsets A$,
$Y_{i}\in\subsets B$ for every $i=0,\ldots,n-1$.
\begin{prop}
The following sets are pairwise equal:
\begin{enumerate}
\item \label{gamma-gamma}$\Gamma(A,B)$;
\item \label{gamma-YX}the set of all sets of the form $\bigcup_{X\in S}(X\times Y_{X})$
where $S$ are finite collections on $A$ and $Y_{X}\in\subsets B$
for every $X\in S$;
\item \label{gamma-YXpart}the set of all sets of the form $\bigcup_{X\in S}(X\times Y_{X})$
where $S$ are finite partitions of $A$ and $Y_{X}\in\subsets B$
for every $X\in S$;
\item \label{gamma-sigma}the set of all finite unions $\bigcup_{(X,Y)\in\sigma}(X\times Y)$
where $\sigma$ is a relation between a partition of $A$ and a partition
of $B$ (that is $\dom\sigma$ is a partition of $A$ and $\im\sigma$
is a partition of $B$).
\item \label{gamma-lineX}the set of all finite intersections $\bigcap_{i=0,\ldots,n-1}\left(X_{i}\times Y_{i}\cup\overline{X_{i}}\times B\right)$
where $n\in\mathbb{N}$ and $X_{i}\in\subsets A$, $Y_{i}\in\subsets B$
for every $i=0,\ldots,n-1$.
\end{enumerate}
\end{prop}
\begin{proof}
~
\begin{description}
\item [{\ref{gamma-gamma}$\supseteq$\ref{gamma-YX},~\ref{gamma-YX}$\supseteq$\ref{gamma-YXpart}}] Obvious.
\item [{\ref{gamma-gamma}$\subseteq$\ref{gamma-YX}}] Let $Q\in\Gamma(A,B)$.
Then $Q=X_{0}\times Y_{0}\cup\ldots\cup X_{n-1}\times Y_{n-1}$. Denote
$S=\{X_{0},\ldots,X_{n-1}\}$. We have $Q=\bigcup_{X'\in S}\left(X'\times\bigcup_{i=0,\dots,n-1}\setcond{Y_{i}}{X_{i}=X'}\right)\in\text{\ref{gamma-YX}}$.
\item [{\ref{gamma-YX}$\subseteq$\ref{gamma-YXpart}}] Let $Q=\bigcup_{X\in S}(X\times Y_{X})$
where $S$ is a finite collection on $A$ and $Y_{X}\in\subsets B$
for every $X\in S$. Let 
\[
P=\bigcup_{X'\in\mathfrak{R}(S)}\left(X'\times\bigcup_{X\in S}\setcond{Y_{X}}{\exists X\in S:X'\subseteq X}\right).
\]
To finish the proof let's show $P=Q$.


$\langle P\rangle^{\ast}\{x\}=\bigcup_{X\in S}\setcond{Y_{X}}{\exists X\in S:X'\subseteq X}$
where $x\in X'$.


Thus $\langle P\rangle^{\ast}\{x\}=\bigcup\setcond{Y_{X}}{\exists X\in S:x\in X}=\langle Q\rangle^{\ast}\{x\}$.
So $P=Q$.

\item [{\ref{gamma-sigma}$\subseteq$\ref{gamma-YXpart}}] $\bigcup_{(X,Y)\in\sigma}(X\times Y)=\bigcup_{X\in\dom\sigma}\left(X\times\bigcup\setcond{Y\in\subsets B}{(X,Y)\in\sigma}\right)\in\text{\text{\ref{gamma-YXpart}}}$.
\item [{\ref{gamma-YXpart}$\subseteq$\ref{gamma-sigma}}] 
\begin{multline*}
\bigcup_{X\in S}(X\times Y_{X})=\bigcup_{X\in S}\left(X\times\bigcup\left(\mathfrak{R}\left(\setcond{Y_{X}}{X\in S}\right)\cap\subsets Y_{X}\right)\right)=\\
\bigcup_{X\in S}\left(X\times\bigcup\setcond{Y'\in\mathfrak{R}\left(\setcond{Y_{X}}{X\in S}\right)}{Y'\subseteq Y_{X}}\right)=\\
\bigcup_{X\in S}\left(X\times\bigcup\setcond{Y'\in\mathfrak{R}\left(\setcond{Y_{X}}{X\in S}\right)}{(X,Y')\in\sigma}\right)=\bigcup_{(X,Y)\in\sigma}(X\times Y)
\end{multline*}
 where $\sigma$ is a relation between $S$ and $\mathfrak{R}\left(\setcond{Y_{X}}{X\in S}\right)$,
and $(X,Y')\in\sigma\Leftrightarrow Y'\subseteq Y_{X}$.
\item [{\ref{gamma-lineX}$\subseteq$\ref{gamma-gamma}}] Obvious.
\item [{\ref{gamma-YXpart}$\subseteq$\ref{gamma-lineX}}] Let $Q=\bigcup_{X\in S}(X\times Y_{X})=\bigcup_{i=0,\ldots,n-1}(X_{i}\times Y_{i})$
for a partition $S=\{X_{0},\ldots,X_{n-1}\}$ of $A$. Then $Q=\bigcap_{i=0,\ldots,n-1}\left(X_{i}\times Y_{i}\cup\overline{X_{i}}\times B\right)$.
\end{description}
\end{proof}
\begin{xca}
Formulate the duals of these sets.\end{xca}
\begin{prop}
$\Gamma(A,B)$ is a boolean lattice, a sublattice of the lattice $\subsets(A\times B)$.\end{prop}
\begin{proof}
That it's a sublattice is obvious. That it has complement, is also
obvious. Distributivity follows from distributivity of $\subsets(A\times B)$.
\end{proof}

\section{Before the diagram}

Next we will prove the below theorem \ref{fcd-diagram} (the theorem
with a diagram). First we will present parts of this theorem as several
lemmas, and then then state a statement about the diagram which concisely
summarizes the lemmas (and their easy consequences).

Below for simplicity we will equate reloids with their graphs (that
is with filters on binary cartesian products).
\begin{obvious}
$\up^{\Gamma(\Src f,\Dst f)}f=(\up f)\cap\Gamma$ for every reloid
$f$.\end{obvious}
\begin{conjecture}
$\upuparrows^{\mathfrak{F}(\mathfrak{B})}\up^{\mathfrak{A}}\mathcal{X}$
is not a filter for some filter $\mathcal{X}\in\mathfrak{F}\Gamma(A,B)$
for some sets $A$, $B$.\end{conjecture}
\begin{rem}
About this conjecture see also: 
\begin{itemize}
\item \href{http://goo.gl/DHyuuU}{http://goo.gl/DHyuuU}
\item \href{http://goo.gl/4a6wY6}{http://goo.gl/4a6wY6}
\end{itemize}
\end{rem}
\begin{lem}
\label{faf-bij}Let $A$, $B$ be sets. The following are mutually
inverse order isomorphisms between $\mathfrak{F}\Gamma(A,B)$ and
$\mathsf{FCD}(A,B)$:
\begin{enumerate}
\item $\mathcal{A}\mapsto\bigsqcap^{\mathsf{FCD}}\up\mathcal{A}$;
\item $f\mapsto\up^{\Gamma(A,B)}f$.
\end{enumerate}
\end{lem}
\begin{proof}
Let's prove that $\up^{\Gamma(A,B)}f$ is a filter for every funcoid
$f$. We need to prove that $P\cap Q\in\up f$ whenever 
\[
P=\bigcap_{i=0,\ldots,n-1}\left(X_{i}\times Y_{i}\cup\overline{X_{i}}\times B\right)\quad\text{and}\quad Q=\bigcap_{j=0,\ldots,m-1}\left(X'_{j}\times Y'_{j}\cup\overline{X'_{j}}\times B\right).
\]
This follows from $P\in\up f\Leftrightarrow\forall i\in0,\ldots,n-1:\supfun fX_{i}\subseteq Y_{i}$
and likewise for $Q$, so having $\supfun f(X_{i}\cap X'_{j})\subseteq Y_{i}\cap Y'_{j}$
for every $i=0,\ldots,n-1$ and $j=0,\ldots,m-1$. From this it follows
\[
((X_{i}\cap X'_{j})\times(Y_{i}\cap Y'_{j}))\cup\left(\overline{X_{i}\cap X'_{j}}\times B\right)\supseteq f
\]
and thus $P\cap Q\in\up f$.

Let $\mathcal{A}$, $\mathcal{B}$ be filters on $\Gamma$. Let $\bigsqcap^{\mathsf{FCD}}\up\mathcal{A}=\bigsqcap^{\mathsf{FCD}}\up\mathcal{B}$.
We need to prove $\mathcal{A}=\mathcal{B}$. (The rest follows from
proof of the lemma~\ref{fcd-rep}). We have:
\begin{align*}
\mathcal{A}=\bigsqcap^{\mathsf{FCD}}\setcond{X\times Y\cup\overline{X}\times B\in\up\mathcal{A}}{X\in\subsets A,Y\in\subsets B} & =\\
\bigsqcap^{\mathsf{FCD}}\setcond{X\times Y\cup\overline{X}\times B}{X\in\subsets A,Y\in\subsets B,\exists P\in\up\mathcal{A}:P\subseteq X\times Y\cup\overline{X}\times B} & =\\
\bigsqcap^{\mathsf{FCD}}\setcond{X\times Y\cup\overline{X}\times B}{X\in\subsets A,Y\in\subsets B,\exists P\in\up\mathcal{A}:\rsupfun PX\subseteq Y} & =\text{(*)}\\
\bigsqcap^{\mathsf{FCD}}\setcond{X\times Y\cup\overline{X}\times B}{X\in\subsets A,Y\in\subsets B,\bigsqcap\setcond{\rsupfun PX}{X\in\up\mathcal{A}}\sqsubseteq Y} & =\\
\bigsqcap^{\mathsf{FCD}}\setcond{X\times Y\cup\overline{X}\times B}{X\in\subsets A,Y\in\subsets B,\bigsqcap\setcond{\rsupfun PX}{X\in\up\bigsqcap^{\mathsf{RLD}}\up\mathcal{A}}\sqsubseteq Y} & =\\
\bigsqcap^{\mathsf{FCD}}\setcond{X\times Y\cup\overline{X}\times B}{X\in\subsets A,Y\in\subsets B,\left\langle \tofcd\bigsqcap^{\mathsf{RLD}}\up\mathcal{A}\right\rangle X\sqsubseteq Y} & =\text{(**)}\\
\bigsqcap^{\mathsf{FCD}}\setcond{X\times Y\cup\overline{X}\times B}{X\in\subsets A,Y\in\subsets B,\left\langle \bigsqcap^{\mathsf{FCD}}\up\bigsqcap^{\mathsf{RLD}}\up\mathcal{A}\right\rangle X\sqsubseteq Y} & =\\
\bigsqcap^{\mathsf{FCD}}\setcond{X\times Y\cup\overline{X}\times B}{X\in\subsets A,Y\in\subsets B,\left\langle \bigsqcap^{\mathsf{FCD}}\up\mathcal{A}\right\rangle X\sqsubseteq Y}.
\end{align*}


({*}) by properties of generalized filter bases, because $\setcond{\rsupfun PX}{P\in\up\mathcal{A}}$
is a filter base.

({*}{*}) by theorem \ref{fcd-as-meet}.

Similarly 
\[
\mathcal{B}=\bigsqcap^{\mathsf{FCD}}\setcond{X\times Y\cup\overline{X}\times B}{X\in\subsets A,Y\in\subsets B,\left\langle \bigsqcap^{\mathsf{FCD}}\up\mathcal{B}\right\rangle X\sqsubseteq Y}.
\]
Thus $\mathcal{A}=\mathcal{B}$.\end{proof}
\begin{prop}
$g\circ f\in\Gamma(A,C)$ if $f\in\Gamma(A,B)$ and $g\in\Gamma(B,C)$
for some sets $A$, $B$, $C$.\end{prop}
\begin{proof}
Because composition of Cartesian products is a Cartesian product.\end{proof}
\begin{defn}
$g\circ f=\bigsqcap^{\mathfrak{F}\Gamma(A,C)}\setcond{G\circ F}{F\in\up f,G\in\up g}$
for $f\in\mathfrak{F}\Gamma(A,B)$ and $g\in\mathfrak{F}\Gamma(B,C)$
(for every sets $A$, $B$, $C$).
\end{defn}
We define $f^{-1}$ for $f\in\mathfrak{F}\Gamma(A,B)$ similarly to
$f^{-1}$ for reloids and similarly derive the formulas:
\begin{enumerate}
\item $(f^{-1})^{-1}=f$;
\item $(g\circ f)^{-1}=f^{-1}\circ g^{-1}$.
\end{enumerate}

\section{Associativity over composition}
\begin{lem}
\label{uparr-gamma-comp}$\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(A,C)}(g\circ f)=\left(\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(B,C)}g\right)\circ\left(\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(B,C)}\right)$
for every $f\in\mathfrak{F}(\Gamma(A,B))$, $g\in\mathfrak{F}(\Gamma(B,C))$
(for every sets $A$, $B$, $C$).\end{lem}
\begin{proof}
If $K\in\up\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(A,C)}(g\circ f)$ then
$K\supseteq G\circ F$ for some $F\in f$, $G\in g$. But $F\in\up^{\Gamma(A,B)}f$,
thus 
\[
F\in\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(A,B)}f
\]
and similarly 
\[
G\in\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(B,C)}g.
\]
So we have 
\[
K\supseteq G\circ F\in\up\left(\left(\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(B,C)}g\right)\circ\left(\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(A,B)}f\right)\right).
\]
Let now 
\[
K\in\up\left(\left(\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(B,C)}g\right)\circ\left(\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(A,B)}f\right)\right).
\]
Then there exist $F\in\up\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(A,B)}f$
and $G\in\up\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(B,C)}g$ such that
$K\supseteq G\circ F$. By properties of generalized filter bases
we can take $F\in\up^{\Gamma(A,B)}f$ and $G\in\up^{\Gamma(B,C)}g$.
Thus $K\in\up^{\Gamma(A,C)}(g\circ f)$ and so $K\in\up\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(A,C)}(g\circ f)$.\end{proof}
\begin{lem}
$\torldin X=X$ for $X\in\Gamma(A,B)$.\end{lem}
\begin{proof}
$X=X_{0}\times Y_{0}\cup\ldots\cup X_{n}\times Y_{n}=(X_{0}\times^{\mathsf{FCD}}Y_{0})\sqcup^{\mathsf{FCD}}\ldots\sqcup^{\mathsf{FCD}}(X_{n}\times^{\mathsf{FCD}}Y_{n})$.
\begin{multline*}
\torldin X=\\
\torldin(X_{0}\times^{\mathsf{FCD}}Y_{0})\sqcup^{\mathsf{RLD}}\ldots\sqcup^{\mathsf{RLD}}\torldin(X_{n}\times^{\mathsf{FCD}}Y)=\\
(X_{0}\times^{\mathsf{RLD}}Y_{0})\sqcup^{\mathsf{RLD}}\ldots\sqcup^{\mathsf{RLD}}(X_{n}\times^{\mathsf{RLD}}Y_{n})=\\
X_{0}\times Y_{0}\cup\ldots\cup X_{n}\times Y_{n}=X.
\end{multline*}
\end{proof}
\begin{lem}
\label{rld-in-fcd-meet}$\bigsqcap^{\mathsf{RLD}} f=\torldin\bigsqcap^{\mathsf{FCD}} f$
for every filter $f\in\mathfrak{F}\Gamma(A,B)$.\end{lem}
\begin{proof}
~
\[
\torldin\bigsqcap^{\mathsf{FCD}} f=\bigsqcap^{\mathsf{RLD}}\rsupfun{\torldin} f=
\text{(by the previous lemma)}=\bigsqcap^{\mathsf{RLD}} f.
\]
\end{proof}
\begin{lem}
\label{rld-gamma-bij}~
\begin{enumerate}
\item \label{rld-gamma-bij-mu}$f\mapsto\bigsqcap^{\mathsf{RLD}}\up f$
and $\mathcal{A}\mapsto\Gamma(A,B)\cap\up\mathcal{A}$ are mutually
inverse bijections between $\mathfrak{F}\Gamma(A,B)$ and a subset
of reloids.
\item \label{rld-gamma-bij-comp}These bijections preserve composition.
\end{enumerate}
\end{lem}
\begin{proof}
~
\begin{widedisorder}
\item [{\ref{rld-gamma-bij-mu}}] That they are mutually inverse bijections
is obvious.
\item [{\ref{rld-gamma-bij-comp}}] ~
\begin{multline*}
\left(\bigsqcap^{\mathsf{RLD}}\up g\right)\circ\left(\bigsqcap^{\mathsf{RLD}}\up f\right)=\bigsqcap^{\mathsf{RLD}}\setcond{G\circ F}{F\in\bigsqcap^{\mathsf{RLD}}f,G\in\bigsqcap^{\mathsf{RLD}}g}=\\
\bigsqcap^{\mathsf{RLD}}\setcond{G\circ F}{F\in f,G\in g}=\bigsqcap^{\mathsf{RLD}}\bigsqcap^{\mathfrak{F}\Gamma(\Src f,\Dst g)}\setcond{G\circ F}{F\in f,G\in g}=\bigsqcap^{\mathsf{RLD}}(g\circ f).
\end{multline*}
So $\bigsqcap^{\mathsf{RLD}}$ preserves composition. That $\mathcal{A}\mapsto\Gamma(A,B)\cap\up\mathcal{A}$
preserves composition follows from properties of bijections.
\end{widedisorder}
\end{proof}
\begin{lem}
Let $A$, $B$, $C$ be sets.
\begin{enumerate}
\item $\left(\bigsqcap^{\mathsf{FCD}}\up g\right)\circ\left(\bigsqcap^{\mathsf{FCD}}\up f\right)=\bigsqcap^{\mathsf{FCD}}\up(g\circ f)$
for every $f\in\mathfrak{F}\Gamma(A,B)$, $g\in\mathfrak{F}\Gamma(B,C)$;
\item $(\up^{\Gamma(B,C)}g)\circ(\up^{\Gamma(A,B)}f)=\up^{\Gamma(A,B)}(g\circ f)$
for every funcoids $f\in\mathsf{FCD}(A,B)$ and $g\in\mathsf{FCD}(B:C)$.
\end{enumerate}
\end{lem}
\begin{proof}
It's enough to prove only the first formula, because of the bijection
from lemma~\ref{faf-bij}.

Really: 
\begin{multline*}
\bigsqcap^{\mathsf{FCD}}\up(g\circ f)=\bigsqcap^{\mathsf{FCD}}\up\bigsqcap^{\mathsf{RLD}}\up(g\circ f)=\\
\bigsqcap^{\mathsf{FCD}}\up\left(\bigsqcap^{\mathsf{RLD}}\up g\circ\bigsqcap^{\mathsf{RLD}}\up f\right)=\tofcd\left(\bigsqcap^{\mathsf{RLD}}\up g\circ\bigsqcap^{\mathsf{RLD}}\up f\right)=\\
\left(\tofcd\bigsqcap^{\mathsf{RLD}}\up g\right)\circ\left(\tofcd\bigsqcap^{\mathsf{RLD}}\up f\right)=\\
\left(\bigsqcap^{\mathsf{FCD}}\up\bigsqcap^{\mathsf{RLD}}\up g\right)\circ\left(\bigsqcap^{\mathsf{FCD}}\up\bigsqcap^{\mathsf{RLD}}\up f\right)=\\
\left(\bigsqcap^{\mathsf{FCD}}\up g\right)\circ\left(\bigsqcap^{\mathsf{FCD}}\up f\right).
\end{multline*}
\end{proof}
\begin{cor}
$(h\circ g)\circ f=h\circ(g\circ f)$ for every $f\in\mathfrak{F}(\Gamma(A,B))$,
$g\in\mathfrak{F}\Gamma(B,C)$, $h\in\mathfrak{F}\Gamma(C,D)$ for
every sets $A$, $B$, $C$, $D$.\end{cor}
\begin{lem}
$\Gamma(A,B)\cap\GR f$ is a filter on the lattice $\Gamma(A,B)$
for every reloid $f\in\mathsf{RLD}(A,B)$.\end{lem}
\begin{proof}
That it is an upper set, is obvious. If $A,B\in\Gamma(A,B)\cap\GR f$
then $A,B\in\Gamma(A,B)$ and $A,B\in\GR f$. Thus $A\cap B\in\Gamma(A,B)\cap\GR f$.\end{proof}
\begin{prop}
If $Y\in\up\supfun f\mathcal{X}$ for a funcoid $f$ then there exists
$A\in\up\mathcal{X}$ such that $Y\in\up\langle f\rangle A$.\end{prop}
\begin{proof}
$Y\in\up\bigsqcap_{A\in\up a}^{\mathscr{F}}\supfun fA$. So by properties
of generalized filter bases, there exists $A\in\up a$ such that $Y\in\up\supfun fA$.\end{proof}
\begin{lem}
$\tofcd f=\bigsqcap^{\mathsf{FCD}}(\Gamma(A,B)\cap\GR f)$ for every
reloid $f\in\mathsf{RLD}(A,B)$.\end{lem}
\begin{proof}
Let $a$ be an an atomic filter object. We need to prove 
\[
\supfun{\tofcd f}a=\supfun{\bigsqcap^{\mathsf{FCD}}(\Gamma(A,B)\cap\GR f)}a
\]
that is 
\[
\supfun{\bigsqcap^{\mathsf{FCD}}\up f}a=\supfun{\bigsqcap^{\mathsf{FCD}}(\Gamma(A,B)\cap\GR f)}a
\]
that is 
\[
\bigsqcap_{F\in\up f}^{\mathscr{F}}\supfun Fa=\bigsqcap_{F\in\Gamma(A,B)\cap\up f}^{\mathscr{F}}\supfun Fa.
\]
For this it's enough to prove that $Y\in\up\supfun Fa$ for some $F\in\up f$
implies $Y\in\up\supfun{F'}a$ for some $F'\in\Gamma(A,B)\cap\GR f$.

Let $Y\in\up\supfun Fa$. Then (proposition above) there exists $A\in\up a$
such that $Y\in\up\supfun FA$.

$Y\in\up\supfun{A\times^{\mathsf{FCD}}Y\sqcup\overline{A}\times^{\mathsf{FCD}}\top}a$;
$\supfun{A\times^{\mathsf{FCD}}Y\sqcup\overline{A}\times^{\mathsf{FCD}}\top}\mathcal{X}=Y\in\up\supfun F\mathcal{X}$
if $\bot\neq\mathcal{X}\sqsubseteq A$ and $\supfun{A\times^{\mathsf{FCD}}Y\sqcup\overline{A}\times^{\mathsf{FCD}}\top}\mathcal{X}=\top\in\up\langle F\rangle\mathcal{X}$
if $\mathcal{X}\nsqsubseteq A$.

Thus $A\times^{\mathsf{FCD}}Y\sqcup\overline{A}\times^{\mathsf{FCD}}\top\sqsupseteq F$.
So $A\times^{\mathsf{FCD}}Y\sqcup\overline{A}\times^{\mathsf{FCD}}\top$
is the sought for~$F'$.
\end{proof}

\section{The diagram}
\begin{thm}
\label{fcd-diagram}The diagram at the figure~\ref{gamma-dia} is
a commutative diagram (in category $\mathbf{Set}$), every arrow in
this diagram is an isomorphism. Every cycle in this diagram is an
identity (therefore ``parallel'' arrows are mutually inverse). The
arrows preserve order, composition, and reversal ($f\mapsto f^{-1}$).

\begin{figure}[ht]
\begin{tikzcd}[row sep=3cm, column sep=0.9cm]
& \text{funcoids}
\arrow[rd, shift left, "\up^\Gamma"]
\arrow[ld, shift left, "\torldin"] \\
\text{funcoidal reloids}
\arrow[ru, shift left, "\tofcd"]
\arrow[rr, shift left, "f\mapsto f\cap\Gamma"]
& & \text{filters on $\Gamma$}
\arrow[lu, shift left, "\bigsqcap^{\mathsf{FCD}}"]
\arrow[ll, shift left, "\bigsqcap^{\mathsf{RLD}}"]
\end{tikzcd}
\caption{\label{gamma-dia}}
\end{figure}
\end{thm}
\begin{proof}
First we need to show that $\bigsqcap^{\mathsf{RLD}}f$ is a funcoidal
reloid. But it follows from lemma~\ref{rld-in-fcd-meet}.

Next, we need to show that all morphisms depicted on the diagram are
bijections and the depicted ``opposite'' morphisms are mutually
inverse.

That $\tofcd$ and $\torldin$ are mutually inverse was proved above
in the book.

That $\bigsqcap^{\mathsf{RLD}}$ and $f\mapsto f\cap\Gamma$ are mutually
inverse was proved above.

That $\bigsqcap^{\mathsf{FCD}}$ and $\up^{\Gamma}$ are mutually
inverse was proved above.

That the morphisms preserve order and composition was proved above.
That they preserve reversal is obvious.

So it remains to apply lemma~\ref{three-loop-lem} (taking into account
lemma~\ref{rld-in-fcd-meet}).
\end{proof}

Another proof that $\tofcd\torldin f=f$ for every funcoid $f$:
\begin{proof}
For every filter $\mathcal{X}\in\mathscr{F}(\Src f)$ we have $\langle\tofcd\torldin f\rangle\mathcal{X}=\bigsqcap_{F\in\up\torldin f}^{\mathscr{F}}\supfun F\mathcal{X}=\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun F\mathcal{X}$.

Obviously $\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun F\mathcal{X}\sqsupseteq\supfun f\mathcal{X}$.
So $\tofcd\torldin f\sqsupseteq f$.

Let $Y\in\up\supfun f\mathcal{X}$. Then (proposition above) there
exists $A\in\up\mathcal{X}$ such that $Y\in\up\langle f\rangle A$.

Thus $A\times Y\sqcup\overline{A}\times\top\in\up f$. So $\supfun{\tofcd\torldin f}\mathcal{X}=\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun F\mathcal{X}\sqsubseteq\supfun{A\times Y\sqcup\overline{A}\times\top}\mathcal{X}=Y$.
So $Y\in\up\supfun{\tofcd\torldin f}\mathcal{X}$ that
is $\supfun f\mathcal{X}\sqsupseteq\supfun{\tofcd\torldin f}\mathcal{X}$
that is $f\sqsupseteq\tofcd\torldin f$.\end{proof}

\section{Some additional properties}
\begin{prop}
For every funcoid $f\in\mathsf{FCD}(A,B)$ (for sets $A$, $B$):
\begin{enumerate}
\item $\dom f=\bigsqcap^{\mathscr{F}(A)}\langle\dom\rangle^{\ast}\up^{\Gamma(A,B)}f$;
\item $\im f=\bigsqcap^{\mathscr{F}(B)}\langle\im\rangle^{\ast}\up^{\Gamma(A,B)}f$.
\end{enumerate}
\end{prop}
\begin{proof}
Take $\setcond{X\times Y}{X\in\subsets A,Y\in\subsets B,X\times Y\supseteq f}\subseteq\up^{\Gamma(A,B)}f$.
I leave the rest reasoning as an exercise.\end{proof}
\begin{thm}
For every reloid $f$ and $\mathcal{X}\in\mathscr{F}(\Src f)$, $\mathcal{Y}\in\mathscr{F}(\Dst f)$:
\begin{enumerate}
\item \label{fcd-up-g-rel}$\mathcal{X}\mathrel{[\tofcd f]}\mathcal{Y}\Leftrightarrow\forall F\in\up^{\Gamma(\Src f,\Dst f)}f:\mathcal{X}\suprel F\mathcal{Y}$;
\item \label{fcd-up-g-fcd}$\langle\tofcd f\rangle\mathcal{X}=\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun F\mathcal{X}$.
\end{enumerate}
\end{thm}
\begin{proof}
~
\begin{widedisorder}
\item [{\ref{fcd-up-g-rel}}] ~
\begin{multline*}
\forall F\in\up^{\Gamma(\Src f,\Dst f)}f:\mathcal{X}\suprel F\mathcal{Y}\Leftrightarrow\\
\forall F\in\up^{\Gamma(\Src f,\Dst f)}f:(\mathcal{X}\times^{\mathsf{FCD}}\mathcal{Y})\sqcap F\ne\bot\Leftrightarrow\text{(*)}\\
(\mathcal{X}\times^{\mathsf{FCD}}\mathcal{Y})\sqcap \bigsqcap^{\mathsf{FCD}}\up^{\Gamma(\Src f,\Dst f)}f\ne\bot\Leftrightarrow\\
\mathcal{X}\suprel{\bigsqcap^{\mathsf{FCD}}\up^{\Gamma(\Src f,\Dst f)}f}\mathcal{Y}\Leftrightarrow\mathcal{X}\suprel{\tofcd f}\mathcal{Y}.
\end{multline*}



({*}) by properties of generalized filter bases, taking into account
that funcoids are isomorphic to filters.

\item [{\ref{fcd-up-g-fcd}}] $\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun Fa=\left\langle \bigsqcap^{\mathsf{FCD}}\up^{\Gamma(\Src f,\Dst f)}f\right\rangle a=\supfun{\tofcd f}a$
for every ultrafilter $a$.


It remains to prove that the function 
\[
\varphi=\lambda\mathcal{X}\in\mathscr{F}(\Src f):\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun F\mathcal{X}
\]
is a component of a funcoid (from what follows that $\varphi=\supfun{\tofcd f}$).
To prove this, it's enough to show that it preserves finite joins
and filtered meets.


$\varphi\bot=\bot$ is obvious. $\varphi(\mathcal{I}\sqcup\mathcal{J})=\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}(\supfun F\mathcal{I}\sqcup\supfun F\mathcal{J})=\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun F\mathcal{I}\sqcup\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun F\mathcal{J}=\varphi\mathcal{I}\sqcup\varphi\mathcal{J}$.
If $S$ is a generalized filter base of $\Src f$, then 
\begin{multline*}
\varphi\bigsqcap^{\mathscr{F}}S=\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun F\bigsqcap^{\mathscr{F}}S=\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\bigsqcap^{\mathscr{F}}\rsupfun{\supfun F}S=\\
\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\bigsqcap_{\mathcal{X}\in S}^{\mathscr{F}}\supfun F\mathcal{X}=\bigsqcap_{\mathcal{X}\in S}^{\mathscr{F}}\bigsqcap_{F\in\up^{\Gamma(\Src f,\Dst f)}f}^{\mathscr{F}}\supfun F\mathcal{X}=\bigsqcap_{\mathcal{X}\in S}^{\mathscr{F}}\varphi\mathcal{X}=\bigsqcap^{\mathscr{F}}\rsupfun{\varphi}S.
\end{multline*}



So $\varphi$ is a component of a funcoid.

\end{widedisorder}
\end{proof}
\begin{defn}
$\boxbox f=\bigsqcap^{\mathsf{RLD}}\up^{\Gamma(\Src f,\Dst f)}f$
for reloid $f$.\end{defn}
\begin{conjecture}
$\boxbox f=\torldin \tofcd f$ for every reloid $f$.
\end{conjecture}
\begin{obvious}
$\boxbox f\sqsupseteq f$ for every reloid $f$.\end{obvious}
\begin{example}
$\torldin f\neq\boxbox\torldout f$ for some funcoid
$f$.\end{example}
\begin{proof}
Take $f=\id_{\Omega(\mathbb{N})}^{\mathsf{FCD}}$. Then, as it was
shown above, $\torldout f=\bot$ and thus $\boxbox\torldout f=\bot$.
But $\torldin f\sqsupseteq\torldin f\neq\bot$. So $\torldin f\neq\boxbox\torldout f$.\end{proof}
Another proof of the theorem ``$\dom\torldin f=\dom f$ and $\im\torldin f=\im f$
for every funcoid $f$.'':
\begin{proof}
We have for every filter $\mathcal{X}\in\mathscr{F}(\Src f)$:
\begin{multline*}
\mathcal{X}\sqsupseteq\dom\torldin f\Leftrightarrow\mathcal{X}\times^{\mathsf{RLD}}\top\sqsupseteq\torldin f\Leftrightarrow\\
\forall a\in\mathscr{F}(\Src f),b\in\mathscr{F}(\Dst f):(a\times^{\mathsf{FCD}}b\sqsubseteq f\Rightarrow a\times^{\mathsf{RLD}}b\sqsubseteq\mathcal{X}\times^{\mathsf{RLD}}\top)\Leftrightarrow\\
\forall a\in\mathscr{F}(\Src f),b\in\mathscr{F}(\Dst f):(a\times^{\mathsf{FCD}}b\sqsubseteq f\Rightarrow a\sqsubseteq\mathcal{X})
\end{multline*}
and 
\begin{multline*}
\mathcal{X}\sqsupseteq\dom f\Leftrightarrow\mathcal{X}\times^{\mathsf{FCD}}\top\sqsupseteq f\Leftrightarrow\\
\forall a\in\mathscr{F}(\Src f),b\in\mathscr{F}(\Dst f):(a\times^{\mathsf{FCD}}b\sqsubseteq f\Rightarrow a\times^{\mathsf{FCD}}b\sqsubseteq\mathcal{X}\times^{\mathsf{FCD}}\top)\Leftrightarrow\\
\forall a\in\mathscr{F}(\Src f),b\in\mathscr{F}(\Dst f):(a\times^{\mathsf{FCD}}b\sqsubseteq f\Rightarrow a\sqsubseteq\mathcal{X}).
\end{multline*}


Thus $\dom\torldin f=\dom f$. The rest follows from symmetry.\end{proof}

Another proof that
$\dom\torldin f=\dom f$ and $\im\torldin f=\im f$ for every funcoid $f$:
\begin{proof}
$\dom\torldin f\sqsupseteq\dom f$ and $\im\torldin f\sqsupseteq\im f$
because $\torldin f\sqsupseteq\torldin$ and $\dom\torldin f=\dom f$
and $\im\torldin f=\im f$.

It remains to prove (as the rest follows from symmetry) that $\dom\torldin f\sqsubseteq\dom f$.

Really, 
\begin{multline*}
\dom\torldin f\sqsubseteq\bigsqcap^{\mathscr{F}}\setcond{X\in\up\dom f}{X\times\top\in\up f}=\\
\bigsqcap^{\mathscr{F}}\setcond{X\in\up\dom f}{X\in\up\dom f}=\bigsqcap^{\mathscr{F}}\up\dom f=\dom f.
\end{multline*}
\end{proof}

\section{More on properties of funcoids}
\begin{prop}
$\Gamma(A,B)$ is the center of lattice $\mathsf{FCD}(A,B)$.\end{prop}
\begin{proof}
Theorem~\ref{pow-filt-central}.\end{proof}
\begin{prop}
$\up^{\Gamma(A,B)}(\mathcal{A}\times^{\mathsf{FCD}}\mathcal{B})$
is defined by the filter base $\setcond{A\times B}{A\in\up\mathcal{A},B\in\up\mathcal{B}}$
on the lattice $\Gamma(A,B)$.\end{prop}
\begin{proof}
It follows from the fact that $\mathcal{A}\times^{\mathsf{FCD}}\mathcal{B}=\bigsqcap^{\mathsf{FCD}}\setcond{A\times B}{A\in\up\mathcal{A},B\in\up\mathcal{B}}$.\end{proof}
\begin{prop}
$\up^{\Gamma(A,B)}(\mathcal{A}\times^{\mathsf{FCD}}\mathcal{B})=\mathfrak{F}(\Gamma(A,B))\cap\up(\mathcal{A}\times^{\mathsf{RLD}}\mathcal{B})$.\end{prop}
\begin{proof}
It follows from the fact that $\mathcal{A}\times^{\mathsf{FCD}}\mathcal{B}=\bigsqcap^{\mathsf{FCD}}\setcond{A\times B}{A\in\up\mathcal{A},B\in\up\mathcal{B}}$.\end{proof}
\begin{prop}
For every $f\in\mathfrak{F}(\Gamma(A,B))$:
\begin{enumerate}
\item \label{gamma-ff}$f\circ f$ is defined by the filter base $\setcond{F\circ F}{F\in\up f}$
(if $A=B$);
\item \label{gamma-f1f}$f^{-1}\circ f$ is defined by the filter base $\setcond{F^{-1}\circ F}{F\in\up f}$;
\item \label{gamma-ff1}$f\circ f^{-1}$ is defined by the filter base $\setcond{F\circ F^{-1}}{F\in\up f}$.
\end{enumerate}
\end{prop}
\begin{proof}
I will prove only \ref{gamma-ff} and \ref{gamma-f1f} because \ref{gamma-ff1}
is analogous to~\ref{gamma-f1f}.
\begin{widedisorder}
\item [{\ref{gamma-ff}}] It's enough to show that $\forall F,G\in\up f\exists H\in\up f:H\circ H\sqsubseteq G\circ F$.
To prove it take $H=F\sqcap G$.
\item [{\ref{gamma-f1f}}] It's enough to show that $\forall F,G\in\up f\exists H\in\up f:H^{-1}\circ H\sqsubseteq G^{-1}\circ F$.
To prove it take $H=F\sqcap G$. Then $H^{-1}\circ H=(F\sqcap G)^{-1}\circ(F\sqcap G)\sqsubseteq G^{-1}\circ F$.
\end{widedisorder}
\end{proof}
\begin{thm}
For every sets $A$, $B$, $C$ if $g,h\in\mathfrak{F}\Gamma(A,B)$
then
\begin{enumerate}
\item $f\circ(g\sqcup h)=f\circ g\sqcup f\circ h$;
\item $(g\sqcup h)\circ f=g\circ f\sqcup h\circ f$.
\end{enumerate}
\end{thm}
\begin{proof}
It follows from the order isomorphism above, which preserves composition.\end{proof}
\begin{thm}
$f\cap g=f\sqcap^{\mathsf{FCD}}g$ if $f,g\in\Gamma(A,B)$.\end{thm}
\begin{proof}
Let $f=X_{0}\times Y_{0}\cup\ldots\cup X_{n}\times Y_{n}$ and $g=X'_{0}\times Y'_{0}\cup\ldots\cup X'_{m}\times Y'_{m}$.

Then 
\begin{multline*}
f\cap g=\bigcup_{i=0,\ldots,n,j=0,\ldots,m}((X_{i}\times Y_{i})\cap(X'_{j}\times Y'_{j}))=\\
\bigcup_{i=0,\ldots,n,j=0,\ldots,m}((X_{i}\cap X'_{j})\times(Y_{i}\cap Y'_{j})).
\end{multline*}


But $f=X_{0}\times Y_{0}\sqcup^{\mathsf{FCD}}\ldots\sqcup^{\mathsf{FCD}}X_{n}\times Y_{n}$
and $g=X'_{0}\times Y'_{0}\sqcup^{\mathsf{FCD}}\ldots\sqcup^{\mathsf{FCD}}X'_{m}\times Y'_{m}$;

\begin{multline*}
f\sqcap^{\mathsf{FCD}}g=\bigsqcup_{i=0,\ldots,n,j=0,\ldots,m}((X_{i}\times Y_{i})\sqcap^{\mathsf{FCD}}(X'_{j}\times Y'_{j}))=\\
\bigsqcup_{i=0,\ldots,n,j=0,\ldots,m}((X_{i}\sqcap X'_{j})\times^{\mathsf{FCD}}(Y_{i}\sqcap Y'_{j})).
\end{multline*}

\begin{cor}
If $X$ and $Y$ are finite binary relations, then
\begin{enumerate}
  \item $X \sqcap^{\mathsf{FCD}} Y = X \sqcap Y$;
  \item $(\top \setminus X) \sqcap^{\mathsf{FCD}} (\top \setminus Y) =
  (\top \setminus X) \sqcap (\top \setminus Y)$;
  \item $X \sqcap^{\mathsf{FCD}} (\top \setminus Y) = X \sqcap (\top
  \setminus Y)$.
\end{enumerate}
\end{cor}

Now it's obvious that $f\cap g=f\sqcap^{\mathsf{FCD}}g$.\end{proof}
\begin{thm}
The set of funcoids (from a given set~$A$ to a given set~$B$)
is with separable core.\end{thm}
\begin{proof}
Let $f,g\in\mathsf{FCD}(A,B)$ (for some sets~$A$,$B$).

Because filters on distributive lattices are with separable core,
there exist $F,G\in\Gamma(A,B)$ such that $F\cap G=\emptyset$. Then
by the previous theorem $F\sqcap^{\mathsf{FCD}}G=\bot$.\end{proof}
\begin{thm}
The coatoms of funcoids from a set~$A$ to a set~$B$ are exactly
$(A\times B)\setminus(\{x\}\times\{y\})$ for $x\in A$, $y\in B$.\end{thm}
\begin{proof}
That coatoms of $\Gamma(A,B)$
are exactly $(A\times B)\setminus(\{x\}\times\{y\})$ for $x\in A$,
$y\in B$, is obvious. To show that coatoms of funcoids are the same,
it remains to apply proposition~\ref{coat}.\end{proof}
\begin{thm}
The set of funcoids (for given~$A$ and~$B$) is coatomic.\end{thm}
\begin{proof}
Proposition~\ref{coat-ic}.\end{proof}
\begin{xca}
Prove that in general funcoids are not coatomistic.\end{xca}

\section{Funcoid bases}

This section will present mainly a counter-example against a statement you have not thought about anyway.

\begin{lem}
If $S$ is an upper set of principal funcoids, then
$\bigsqcap^{\mathsf{FCD}} (S\cap\Gamma)=\bigsqcap^{\mathsf{FCD}} S$.
\end{lem}

\begin{proof}
  $\bigsqcap^{\mathsf{FCD}} (S\cap\Gamma) \sqsupseteq \bigsqcap^{\mathsf{FCD}} S$ is obvious.
  
  $\bigsqcap^{\mathsf{FCD}} S = \bigsqcap^{\mathsf{FCD}} \bigsqcap^{\mathsf{FCD}}_{K\in S} T_K \sqsupseteq \bigsqcap^{\mathsf{FCD}} (S\cap\Gamma)$.
  where $T_K\in\subsets (S\cap\Gamma)$.
  So $\bigsqcap^{\mathsf{FCD}} (S\cap\Gamma) = \bigsqcap^{\mathsf{FCD}} S$.
\end{proof}

\begin{thm}
  If $S$ is a filter base on the set of binary relations then $S$ is a base of
  $\bigsqcap^{\mathsf{FCD}} S$.
\end{thm}

First prove a special case of our theorem to get the idea:

\begin{example}
  Take the filter base $S = \setcond{
  \setcond{ (x, y) }{ | x - y | < \varepsilon }}{ \varepsilon > 0 }$ and $K = \setcond{ (x, y) }{
  | x - y | < \exp x }$ where $x$ and $y$ range real
  numbers. Then $K \notin \up \bigsqcap^{\mathsf{FCD}} S$.
\end{example}

\begin{proof}
  Take a nontrivial ultrafilter $x$ on $\mathbb{R}$. We can for simplicity
  assume $x \sqsubseteq \mathbb{Z}$.
  
  \[ \supfun{\bigsqcap^{\mathsf{FCD}} S} x =
  \bigsqcap^{\mathscr{F}}_{L \in S} \supfun{L} x =
  \bigsqcap^{\mathscr{F}}_{L \in S, X \in \up x} \rsupfun{L} X =
  \bigsqcap^{\mathscr{F}}_{\varepsilon > 0, X \in \up
  x} \bigsqcup_{\alpha \in X} \mathopen] \alpha - \varepsilon ; \alpha + \varepsilon \mathclose[. \]
  
  $\supfun{K} x = \bigsqcap^{\mathscr{F}}_{X \in \up x} \rsupfun{K} X =
  \bigsqcap^{\mathscr{F}}_{X \in \up x}
  \bigsqcup_{\alpha \in X}\mathopen] \alpha - \exp \alpha ; \alpha + \exp \alpha \mathclose[$.
  
  Suppose for the contrary that $\supfun{K} x \sqsupseteq \supfun{
  \bigsqcap^{\mathsf{FCD}} S } x$.
  
  Then
  
  $\bigsqcup_{\alpha \in X} \mathopen] \alpha - \exp \alpha ; \alpha + \exp \alpha \mathclose[
  \sqsupseteq \bigsqcap^{\mathscr{F}}_{\varepsilon > 0, X \in \up x}
  \bigsqcup_{\alpha \in X} \mathopen] \alpha - \varepsilon ; \alpha + \varepsilon \mathclose[$ for
  every $X \in \up x$;
  
  thus by properties of generalized filter bases ($\setcond{ \bigsqcup_{\alpha
  \in X} \mathopen] \alpha - \varepsilon ; \alpha + \varepsilon \mathclose[ }{
  \varepsilon > 0 }$ is a filter base and even a chain)
  
  $\bigsqcup_{\alpha \in X} \mathopen] \alpha - \exp \alpha ; \alpha + \exp \alpha \mathclose[
  \sqsupseteq \bigsqcap^{\mathscr{F}}_{X \in \up x} \bigsqcup_{\alpha
  \in X} \mathopen] \alpha - \varepsilon ; \alpha + \varepsilon \mathclose[$ for some $\varepsilon
  > 0$ and thus
  by properties of generalized filter bases ($\setcond{ \bigsqcup_{\alpha \in
  X} \mathopen] \alpha - \varepsilon ; \alpha + \varepsilon \mathclose[ }{
  X \in \up x }$ is a filter base) for some $X' \in \up x$
  
  \[ \bigsqcup_{\alpha \in X} \mathopen] \alpha - \exp \alpha ; \alpha + \exp \alpha \mathclose[
  \sqsupseteq \bigsqcup_{\alpha \in X'} \mathopen] \alpha - \varepsilon ; \alpha +
  \varepsilon \mathclose[ \]
  what is impossible by the fact that $\exp \alpha$ goes infinitely small as
  $\alpha \rightarrow - \infty$ and the fact that we can take $X =\mathbb{Z}$
  for some $x$.
\end{proof}

Now prove the general case:

\begin{proof}
  Suppose that $K \in \up \bigsqcap^{\mathsf{FCD}} S$ and thus
  $\supfun{K} x \sqsupseteq \supfun{
  \bigsqcap^{\mathsf{FCD}} S } x$.
  We need to prove that there is some~$L\in S$ such that $K\sqsupseteq L$.
  
  Take an ultrafilter $x$.
  
  $\supfun{\bigsqcap^{\mathsf{FCD}} S} x =
  \bigsqcap^{\mathscr{F}}_{L \in S} \supfun{L} x =
  \bigsqcap^{\mathscr{F}}_{L \in S, X \in \up x} \rsupfun{L} X$.
  
  $\supfun{K} x = \bigsqcap^{\mathscr{F}}_{X \in \up x} \rsupfun{K}X$.
  
  Then
  $\rsupfun{K} X \sqsupseteq \bigsqcap^{\mathscr{F}}_{L \in S, X
  \in \up x} \rsupfun{L} X$ for every $X \in \up x$;
  thus by properties of generalized filter bases ($\setcond{ \rsupfun{L}X
  }{ L \in S }$ is a filter base);
  
  $\rsupfun{K} X \sqsupseteq \bigsqcap^{\mathscr{F}}_{X \in
  \up x} \rsupfun{L} X$ for some $L \in S$ and thus
  by properties of generalized filter bases ($\setcond{ \rsupfun{L}
  X }{ X \in \up x }$ is a filter base) for some $X' \in \up x$
  
  $\rsupfun{K} X \sqsupseteq \rsupfun{L} X'
  \sqsupseteq \supfun{L} x$.
  
  So $\supfun{K} x \sqsupseteq \supfun{L} x$ because this
  equality holds for every $X \in \up x$. Therefore $K \sqsupseteq L$.
\end{proof}

\begin{example}
A base of a funcoid which is not a filter base.
\end{example}

\begin{proof}
Consider $f=\id^{\mathsf{FCD}}_{\Omega}$. We know that $\up f$ is not a
filter base. But it is a base of a funcoid.
\end{proof}

\begin{xca}
Prove that a set $S$ is a filter (on some set) iff
\[ \forall X_0,\dots,X_n\in S:\up(X_0\sqcap\dots\sqcap X_n)\subseteq S \]
for every natural~$n$.
\end{xca}

A similar statement does \emph{not} hold for funcoids:

\begin{example}
For a set $S$ of binary relations
\[ \forall X_0,\dots,X_n\in S:\up(X_0\sqcap^{\mathsf{FCD}}\dots\sqcap^{\mathsf{FCD}} X_n)\subseteq S \]
does not imply that there exists funcoid~$f$ such that $S=\up f$.
\end{example}

\begin{proof}
Take $S_0 = \up 1^{\mathsf{FCD}}$ (where $1^{\mathsf{FCD}}$ is the identity funcoid on any infinite set)
and $S_1 = \bigcup_{F\in S_0} \setcond{\up G}{G\in\up^{\Gamma} F}$ (that is
$S_1 = \bigcup_{F\in\up^{\Gamma} 1^{\mathsf{FCD}}}\up F$).

Both $S_0$ and $S_1$ are upper sets. $S_0\ne S_1$ because $1^{\mathsf{FCD}}\in S_0$ and $1^{\mathsf{FCD}}\notin S_1$.

The formula in the example works for $S=S_0$ because $X_0,\dots,X_n\in \up 1^{\mathsf{FCD}}$. It also holds for $S=S_1$ by the
following reason:

Suppose $X_0,\dots,X_n\in S_1$. Then $X_i\sqsupseteq F_i$ where $F_i\in S_0$.
Consequently (take into account that $\Gamma$ is a sublattice of $\mathsf{FCD}$)
$X_0,\dots,X_n \sqsupseteq F_0\sqcap^{\mathsf{FCD}}\dots\sqcap^{\mathsf{FCD}} F_n$ and so
$X_0\sqcap^{\mathsf{FCD}}\dots\sqcap^{\mathsf{FCD}} X_n=
X_0\sqcap\dots\sqcap X_n \sqsupseteq F_0\sqcap^{\mathsf{FCD}}\dots\sqcap^{\mathsf{FCD}} F_n \sqsupseteq 1^{\mathsf{FCD}}$.
Thus $X_0\sqcap\dots\sqcap X_n \in \up^{\Gamma} 1^{\mathsf{FCD}} \subseteq S_1$;
$\up(X_0\sqcap\dots\sqcap X_n)\subseteq S_1$ as $S_1$ is an upper set.

To finish the proof suppose for the contrary that $\up f_0=S_0$ and $\up f_1=S_1$ for some funcoids~$f_0$ and~$f_1$.
In this case $f_0=\bigsqcap^{\mathsf{FCD}} S_0 = 1^{\mathsf{FCD}} = \bigsqcap^{\mathsf{FCD}} \up^{\Gamma} 1^{\mathsf{FCD}} =
\bigsqcap^{\mathsf{FCD}} S_1 = f_1$ and thus $S_0=S_1$, contradiction.
\end{proof}

\begin{prop}
For a set $S$ of binary relations
\[ \forall X_0,\dots,X_n\in S:\up(X_0\sqcap^{\mathsf{FCD}}\dots\sqcap^{\mathsf{FCD}} X_n)\subseteq S \]
does not imply that~$S$ is a funcoid base.
\end{prop}

\begin{proof}
Suppose for the contrary that it does imply. Then, because~$S$ is an upper set (as follows from the condition,
taking $n=0$), it implies that~$S=\up f$ for a funcoid~$f$, what contradicts to the above example.
\end{proof}

\begin{conjecture}
  Let $\forall X,Y\in S:\up(X\sqcap^{\mathsf{FCD}} Y)\subseteq S$.
  
  Then
  \[ \forall X_0,\dots,X_n\in S:\up(X_0\sqcap^{\mathsf{FCD}}\dots\sqcap^{\mathsf{FCD}} X_n)\subseteq S. \]
\end{conjecture}

\begin{xca}
$\up (f_0 \sqcap^{\mathsf{FCD}} \ldots
\sqcap^{\mathsf{FCD}} f_n) \subseteq \setcond{ F_0 \sqcap \ldots \sqcap
F_n }{ F_0 \in \up f_0 \wedge \ldots \wedge F_n \in \up f_n }$ for every funcoids~$f_0$, \dots, $f_n$ ($n\in\mathbb{N}$).
\end{xca}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Some (example) values}

I will do some calculations of particular funcoids and reloids.

First note that $\sqcap^{\mathsf{FCD}}$ can be decomposed (see below for a short easy proof):
\[ f \sqcap^{\mathsf{FCD}} g = \tofcd ((\torldin f \sqcap \torldin g). \]

The above is a more understandable decomposition of the operation~$\sqcap^{\mathsf{FCD}}$
which behaves in strange way, mapping meet of two binary relations into a funcoid which
is not a binary relation ($1^{\mathsf{FCD}} \sqcap^{\mathsf{FCD}} (\top \setminus 1^{\mathsf{FCD}}) =
1^{\mathsf{FCD}}_{\Omega}$).

The last formula is easy to prove (and proved above in the book) but the result is counter-intuitive.

More generally:
\[ \bigsqcap^{\mathsf{FCD}} S = \tofcd \bigsqcap^{\mathsf{RLD}} \rsupfun{\torldin} S. \]

The above formulas follow from the fact that~$\tofcd$ is an upper adjoint
and that $\tofcd\torldin f=f$ for every funcoid $f$.

Let $\mathsf{FCD}$ denote funcoids on a set $U$.

Consider a special case of the above formulas:
\begin{equation}\label{fcd-meet-spec}
1^{\mathsf{FCD}} \sqcap^{\mathsf{FCD}} (\top \setminus 1^{\mathsf{FCD}}) =
\tofcd (\torldin 1^{\mathsf{FCD}} \sqcap \torldin (\top \setminus 1^{\mathsf{FCD}})).
\end{equation}

We want to calculate terms of the formula~\eqref{fcd-meet-spec} and more generally do some
(probably useless) calculations for particular funcoids and reloids related to the above formula.

The left side is already calculated. The term~$\torldin 1^{\mathsf{FCD}}$ which I call
``thick equality'' above is well understood. Let's compute $\torldin (\top \setminus 1^{\mathsf{FCD}})$.

\begin{prop}
$\torldin (\top \setminus 1^{\mathsf{FCD}}) = \top \setminus 1^{\mathsf{FCD}}$.
\end{prop}

\begin{proof}
Consider funcoids on a set $U$. For any filters~$x$ and~$y$ (or without loss of generality ultrafilters~$x$ and~$y$) we have:

\begin{multline*}
x \times^{\mathsf{FCD}} y \sqsubseteq \top \setminus
1^{\mathsf{FCD}} \Leftrightarrow \\ \text{(theorem 574 and the fact that
funcoids are filters)} \Leftrightarrow \\ x \times^{\mathsf{FCD}} y \asymp
1^{\mathsf{FCD}} \Leftrightarrow \neg \left( x
\mathrel{[1^{\mathsf{FCD}}]} y \right) \Leftrightarrow x \asymp y
\Rightarrow \\ \exists X \in \up x, Y \in \up y : X \asymp Y.
\end{multline*}

Thus $\torldin (\top \setminus
1^{\mathsf{FCD}}) = \bigsqcup \setcond{ X \times Y}
{X, Y \in \mathscr{T} U, X \asymp Y } = \top \setminus
1^{\mathsf{FCD}}$.
\end{proof}

So, we have:

\[
1^{\mathsf{FCD}}_{\Omega} =
1^{\mathsf{FCD}} \sqcap^{\mathsf{FCD}} (\top \setminus 1^{\mathsf{FCD}}) =
\torldin 1^{\mathsf{FCD}} \sqcap^{\mathsf{FCD}} (\top \setminus 1^{\mathsf{FCD}}).
\]

\begin{prop}\label{cj-rldin-diag}
  If $X_0 \sqcup \ldots \sqcup X_n = \top$ then $(X_0 \times X_0) \sqcup
  \ldots \sqcup (X_n \times X_n) \in \up
  \torldin 1^{\mathsf{FCD}}$.
\end{prop}

\begin{proof}
  It's enough to prove $(X_0 \times X_0) \sqcup \ldots \sqcup (X_n \times X_n)
  \in \up (x \times x)$ for every ultrafilter~$x$, what follows from the
  fact that $x \sqsubseteq X_i$ for some~$i$ and thus $x \times x \sqsubseteq
  X_i \times X_i$.
\end{proof}

\begin{prop}
  For finite tuples $X$, $Y$ of typed sets
  \[ (X_0 \times Y_0) \sqcup \ldots \sqcup (X_n \times Y_n) \sqsupseteq 1
     \Leftrightarrow (X_0 \sqcap Y_0) \sqcup \ldots \sqcup (X_n \sqcap Y_n) =
     \top . \]
\end{prop}

\begin{proof}
\begin{multline*}
  (X_0 \times Y_0) \sqcup \ldots \sqcup (X_n \times Y_n) \sqsupseteq 1
  \Leftrightarrow \\ ((X_0 \times Y_0) \sqcup \ldots \sqcup (X_n \times Y_n))
  \sqcap 1 = 1 \Leftrightarrow \\ ((X_0 \times Y_0) \sqcap 1) \sqcup \ldots
  \sqcup ((X_n \times Y_n) \sqcap 1) = 1 \Leftrightarrow \\ \id_{X_0 \sqcap
  Y_0} \sqcup \ldots \sqcup \id_{X_n \sqcap Y_n} = 1 \Leftrightarrow \\
  \id_{(X_0 \sqcap Y_0) \sqcup \ldots \sqcup (X_n \sqcap Y_n)} = 1
  \Leftrightarrow \\ (X_0 \sqcap Y_0) \sqcup \ldots \sqcup (X_n \sqcap Y_n) =
  \top.
\end{multline*}
\end{proof}

\begin{cor}
  ~
  \[ \up^{\Gamma} 1 = \setcond{ (X_0 \times Y_0) \sqcup \ldots \sqcup (X_n
     \times Y_n) }{ n \in \mathbb{N}, \forall i \in
     n : X_i, Y_i \in \mathscr{T} U, (X_0 \sqcap Y_0) \sqcup \ldots \sqcup
     (X_n \sqcap Y_n) = \top } . \]
\end{cor}

\begin{cor}
  The predicate
  $(X_0 \sqcap Y_0) \sqcup \ldots \sqcup (X_n \sqcap Y_n) = \top$ for an
  element $(X_0 \times Y_0) \sqcup \ldots \sqcup (X_n \times Y_n)$ of $\Gamma$
  does not depend on its representation $(X_0 \times Y_0) \sqcup \ldots \sqcup
  (X_n \times Y_n)$.
\end{cor}

\begin{prop}
  ~
  \[ \up^{\Gamma} 1 = \bigcup \setcond{ \up^{\Gamma} ((X_0 \times
     X_0) \sqcup \ldots \sqcup (X_n \times X_n)) }{ n
     \in \mathbb{N}, \forall i \in n : X_i \in \mathscr{T} U, X_0 \sqcup
     \ldots \sqcup X_n = \top } . \]
\end{prop}

\begin{proof}
  If $(X_0 \times Y_0) \sqcup \ldots \sqcup (X_n \times Y_n) \in
  \up^{\Gamma} 1$ then we have
\begin{multline*}
  (X_0 \times Y_0) \sqcup \ldots \sqcup (X_n \times Y_n) \sqsupseteq \\ ((X_0
     \sqcap Y_0) \times (X_0 \sqcap Y_0)) \sqcup \ldots \sqcup ((X_n \sqcap
     Y_n) \times (X_n \sqcap Y_n)) \in \up^{\Gamma} 1.
\end{multline*}
  Thus
  \[ \up^{\Gamma} 1 \subseteq \bigcup \setcond{ \up^{\Gamma} ((X_0
     \times X_0) \sqcup \ldots \sqcup (X_n \times X_n)) }{
     \hspace{1em} n \in \mathbb{N}, \forall i \in n : X_i \in \mathscr{T} U,
     X_0 \sqcup \ldots \sqcup X_n = \top } . \]
  The reverse inclusion is obvious.
\end{proof}

\begin{prop}
  ~
  \[ \torldin 1^{\mathsf{FCD}} =
     \bigsqcap^{\mathsf{RLD}} \setcond{ (X_0 \times X_0) \sqcup \ldots
     \sqcup (X_n \times X_n) }{ n \in \mathbb{N},
     \forall i \in n : X_i \in \mathscr{T} U, X_0 \sqcup \ldots \sqcup X_n =
     \top } . \]
\end{prop}

\begin{proof}
  By the diagram we have $\torldin
  1^{\mathsf{FCD}} = \bigsqcap^{\mathsf{RLD}} \up^{\Gamma} 1$. So it follows from the previous proposition.
\end{proof}

\begin{prop}
  $\up^{\Gamma} \torldin 1^{\mathsf{FCD}} = \up^{\Gamma} 1$.
\end{prop}

\begin{proof}
  If $K \in \up^{\Gamma} 1$ then $K \in \up^{\Gamma} ((X_0 \times
  X_0) \sqcup \ldots \sqcup (X_n \times X_n))$ and thus $K \in
  \up^{\Gamma}  \torldin
  1^{\mathsf{FCD}}$ (see proposition~\ref{cj-rldin-diag}). Thus $\up^{\Gamma}
  1 \subseteq \up^{\Gamma}  \torldin
  1^{\mathsf{FCD}}$. But $\up^{\Gamma} 
  \torldin 1^{\mathsf{FCD}} \subseteq
  \up^{\Gamma} 1$ is obvious.
\end{proof}