chap-cofinite.tex

\chapter{Generalized cofinite filters}

The following is a straightforward generalization of cofinite filter.

\begin{defn}
  $\Omega_{1 a} = \bigsqcap^{\mathfrak{A}}_{X \in
  \operatorname{coatoms}^{\mathfrak{Z}}} X$; $\Omega_{1 b} =
  \bigsqcap^{\mathfrak{A}}_{X \in \operatorname{coatoms}^{\mathfrak{A}}} X$.
\end{defn}

\begin{prop}
The following is an implications tuple:
\begin{enumerate}
 \item\label{omeq-pow} $(\mathfrak{A},\mathfrak{Z})$ is a powerset filtrator.
 \item\label{omeq-flt} $(\mathfrak{A},\mathfrak{Z})$ is a primary filtrator.
 \item\label{omeq-res} $\Omega_{1 a} = \Omega_{1 b}$ for this filtrator.
\end{enumerate}  
\end{prop}

\begin{proof}
~
\begin{description}
 \item[\ref{omeq-pow}$\Rightarrow$\ref{omeq-flt}] Obvious.
 \item[\ref{omeq-flt}$\Rightarrow$\ref{omeq-res}] Proposition~\ref{coat}.
\end{description}
\end{proof}

\begin{prop}
  Let $(\mathfrak{A},\mathfrak{Z})$ be a primary filtrator.
  Let $\mathfrak{Z}$ be a subset of $\subsets U$. Let it be a
  meet-semilattice with greatest element.
  Let also every non-coempty cofinite set lies in
  $\mathfrak{Z}$. Then
  \begin{equation}
    \corestar \Omega = \setcond{ Y \in \mathfrak{Z} }{
    \card \atoms^{\mathfrak{Z}} Y \geq \omega } .
    \label{d-cofin}
  \end{equation}
\end{prop}

\begin{proof}
  $\Omega$ exists by corollary~\ref{filt-is-complete}.
\begin{multline*}
  Y \in \corestar \Omega \Leftrightarrow Y \nasymp^{\mathfrak{A}} 
  \bigsqcap^{\mathfrak{A}}_{X \in \operatorname{coatoms}^{\mathfrak{Z}}} X
  \Leftrightarrow \\ \text{(by properties of filter bases)} \Leftrightarrow \\
  \forall S \in \subsets_{\operatorname{fin}} \operatorname{coatoms}^{\mathfrak{Z}} : Y
  \nasymp^{\mathfrak{A}} \bigsqcap^{\mathfrak{A}} S \Leftrightarrow \\
  \text{(corollary~\ref{f-meet-closed})} \Leftrightarrow \forall S \in \subsets_{\operatorname{fin}}
  \operatorname{coatoms}^{\mathfrak{Z}} : Y \nasymp \bigsqcap S \Leftrightarrow \\
  \forall K \in \subsets_{\operatorname{fin}} U : Y \setminus K \neq \emptyset
  \Leftrightarrow \\ \card Y \geq \omega \Leftrightarrow \card
  \atoms^{\mathfrak{Z}} Y \geq \omega.
\end{multline*}
  (Here $\subsets_{\operatorname{fin}}$ denotes
  the set of finite subsets.)
\end{proof}

\begin{cor}
  Formula (\ref{d-cofin}) holds for both reloids and funcoids.
\end{cor}

\begin{proof}
  For reloiods it's straightforward, for funcoids take that they are
  isomorphic to filters on lattice $\Gamma$.
\end{proof}

\begin{cor}
$\Omega^{\mathsf{FCD}} \ne \bot^{\mathsf{FCD}}$ (for $\mathsf{FCD}(A,B)$ where $A\times B$ is an infinite set).
\end{cor}

\begin{prop}\label{omega-bot}
The following is an implications tuple:
\begin{enumerate}
 \item\label{omega-bot-pow} $(\mathfrak{A},\mathfrak{Z})$
  is a powerset filtrator.
 \item\label{omega-bot-flt} $(\mathfrak{A},\mathfrak{Z})$
   is a primary filtrator over an atomic ideal base
   and $\forall \alpha \in
  \atoms^{\mathfrak{Z}} \exists X \in \operatorname{coatoms}^{\mathfrak{Z}}: a
  \nsqsubseteq X$.
 \item\label{omega-bot-cond} $\Omega_{1 a}$ and $\Cor \Omega_{1 a}$ are defined,
  $\forall \alpha \in
  \atoms^{\mathfrak{Z}} \exists X \in \operatorname{coatoms}^{\mathfrak{Z}}: a
  \nsqsubseteq X$ and $\mathfrak{Z}$ is an atomic poset.
 \item\label{omega-bot-res} $\Cor \Omega_{1 a} = \bot^{\mathfrak{Z}}$.
\end{enumerate}  
\end{prop}

\begin{proof}
~
\begin{description}
\item[\ref{omega-bot-pow}$\Rightarrow$\ref{omega-bot-flt}]
  Obvious.
\item[\ref{omega-bot-flt}$\Rightarrow$\ref{omega-bot-cond}]
  Obvious.
\item[\ref{omega-bot-cond}$\Rightarrow$\ref{omega-bot-res}]
  Suppose $\alpha \in \atoms^{\mathfrak{Z}} \Cor \Omega$. Then
  $\exists X \in \up \Omega : \alpha \nsqsubseteq X$.
  Therefore $\alpha \notin \atoms^{\mathfrak{Z}} \Cor \Omega$. So $\atoms^{\mathfrak{Z}}
  \Cor \Omega_{1 a} = \emptyset$ and thus by atomicity $\Cor
  \Omega_{1 a} = \bot^{\mathfrak{Z}}$.
\end{description}
\end{proof}

\begin{cor}
  $\Cor \Omega^{\mathsf{FCD}} = \bot$.
\end{cor}

\begin{prop}
The following is an implications tuple:
\begin{enumerate}
\item\label{om-max-pow} $(\mathfrak{A},\mathfrak{Z})$ is a powerset filtrator.
\item\label{om-max-flt} $(\mathfrak{A},\mathfrak{Z})$ is a primary filtrator
  over an atomic meet-semilattice with greatest element such that
  $\forall \alpha \in
  \atoms^{\mathfrak{Z}} \exists X \in \operatorname{coatoms}^{\mathfrak{Z}}: a
  \nsqsubseteq X$.
\item\label{om-max-cond} $\mathfrak{A}$ is
  a complete lattice,
  $\forall \alpha \in
  \atoms^{\mathfrak{Z}} \exists X \in \operatorname{coatoms}^{\mathfrak{Z}}: a
  \nsqsubseteq X$ and~$(\mathfrak{A}; \mathfrak{Z})$ is a filtered filtrator over an atomic poset.
\item\label{om-max-res} $\Omega_{1 a} = \max \setcond{ \mathcal{X} \in \mathfrak{A} }{
  \Cor \mathcal{X} = \bot^{\mathfrak{Z}} }$
\end{enumerate}
\end{prop}

\begin{proof}
~
\begin{description}
\item[\ref{om-max-pow}$\Rightarrow$\ref{om-max-flt}]
  Obvious.

\item[\ref{om-max-flt}$\Rightarrow$\ref{om-max-cond}]
  Obvious.

\item[\ref{om-max-cond}$\Rightarrow$\ref{om-max-res}]
  Due the last proposition, it is enough to show that $\Cor \mathcal{X}
  = \bot^{\mathfrak{Z}} \Rightarrow \mathcal{X} \sqsubseteq \Omega_{1 a}$ for
  every $\mathcal{X} \in \mathfrak{A}$.
  
  Let $\Cor \mathcal{X} = \bot^{\mathfrak{Z}}$ for some $\mathcal{X} \in
  \mathfrak{A}$. Because of our filtrator being filtered, it's enough to show~$X\in\up\mathcal{X}$
  for every~$X \in \up \Omega_{1 a}$ . $X = a_0 \sqcap \ldots \sqcap a_n$ for $a_i$
  being coatoms of $\mathfrak{Z}$. $a_i \sqsupseteq \mathcal{X}$ because
  otherwise $a_i \nsqsupseteq \Cor \mathcal{X}$. So $X
  \in \up \mathcal{X}$.
\end{description}
\end{proof}

\begin{prop}
The following is an implications tuple:
\begin{enumerate}
\item\label{omfinm-pow} $(\mathfrak{A},\mathfrak{Z})$ is
  a powerset filtrator.
\item\label{omfinm-flt} $(\mathfrak{A},\mathfrak{Z})$ is
  a primary filtrator over a meet-semilattice.
\item\label{omfinm-res} $\up \Omega_{1a} = \setcond{ \bigsqcap S }{ S \in
  \subsets_{\operatorname{fin}} \operatorname{coatoms}^{\mathfrak{Z}} }$
\end{enumerate}
\end{prop}

\begin{proof}
~
\begin{description}
 \item[\ref{omfinm-pow}$\Rightarrow$\ref{omfinm-flt}]
  Obvious.
 \item[\ref{omfinm-flt}$\Rightarrow$\ref{omfinm-res}]
  Because $\setcond{ \bigsqcap S }{ S \in
  \subsets_{\operatorname{fin}} \operatorname{coatoms}^{\mathfrak{Z}} }$ is a
  filter.
\end{description}
\end{proof}

\begin{cor}
  $\up \Omega^{\mathsf{FCD}} = \up
  \Omega^{\mathsf{RLD}}$.
\end{cor}

\begin{defn}
$\Omega_{1c} =
\bigsqcup(\atoms^{\mathfrak{A}}\setminus\mathfrak{Z})$.
\end{defn}

\begin{prop}
The following is an implications tuple:
\begin{enumerate}
 \item\label{omeq-ca-pow} $(\mathfrak{A}; \mathfrak{Z})$ is a powerset
  filtrator.
 \item\label{omeq-ca-flt} $(\mathfrak{A}; \mathfrak{Z})$ is a down-aligned
  filtered complete lattice filtrator over an atomistic poset and
  $\forall \alpha \in \atoms^{\mathfrak{Z}} \exists X \in \operatorname{coatoms}^{\mathfrak{Z}} : a \nsqsubseteq X$.
 \item\label{omeq-ca-res} $\Omega_{1c} = \Omega_{1a}$.
\end{enumerate}
\end{prop}

\begin{proof}
~
\begin{description}
 \item[\ref{omeq-ca-pow}$\Rightarrow$\ref{omeq-ca-flt}]
  Obvious.
 \item[\ref{omeq-ca-flt}$\Rightarrow$\ref{omeq-ca-res}]
  For $x\in\atoms^{\mathfrak{A}}\setminus\mathfrak{Z}$ we have
  $\Cor x=\bot$ because otherwise $\bot\ne\Cor x\sqsubset x$.
  Thus by previous $x\sqsubseteq\Omega_{1a}$ and so
  $\Omega_{1c} =
  \bigsqcup(\atoms^{\mathfrak{A}}\setminus\mathfrak{Z}) \sqsubseteq
  \Omega_{1a}$.

  If $x\in\atoms\Omega_{1a}$ then $x\notin\mathfrak{Z}$ because otherwise
  $\Cor x\ne\bot$. So \[ \Omega_{1a}=\bigsqcup\atoms \Omega_{1a}=
  \bigsqcup(\atoms \Omega_{1a}\setminus\mathfrak{Z})\sqsubseteq
  \bigsqcup(\atoms^{\mathfrak{A}}\setminus\mathfrak{Z}) =
  \Omega_{1c}. \]
\end{description}
\end{proof}

\begin{thm}\label{cor-adjom}
The following is an implications tuple:
\begin{enumerate}
\item\label{cor-adj-omega-pow}
  $(\mathfrak{A},\mathfrak{Z})$ is a powerset filtrator.
\item\label{cor-adj-omega-cond}
  $(\mathfrak{A},\mathfrak{Z})$ is a primary filtrator over
  a complete atomic boolean lattice.
\item\label{cor-adj-omega-flt} All of the following:
  \begin{enumerate}
    \item $\mathfrak{A}$ is atomistic complete starrish lattice.
    \item $\mathfrak{Z}$ is a complete atomistic lattice.
    \item $(\mathfrak{A},\mathfrak{Z})$ is a filtered
      down-aligned filtrator with binarily meet-closed core.
  \end{enumerate}
\item\label{cor-adj-omega-res} $\Cor'$ is the lower adjoint of
  $\Omega_{1c}\sqcup^{\mathfrak{A}}-$.
\end{enumerate}
\end{thm}

\begin{proof}
~
\begin{widedisorder}
\item[\ref{cor-adj-omega-pow}$\Rightarrow$\ref{cor-adj-omega-cond}]
Obvious.

\item[\ref{cor-adj-omega-cond}$\Rightarrow$\ref{cor-adj-omega-flt}]
Obvious.

\item[\ref{cor-adj-omega-flt}$\Rightarrow$\ref{cor-adj-omega-res}]
It with join-closed core by theorem~\ref{semifilt-joinclosed}.

We will prove $\Cor'\mathcal{X} \sqsubseteq \mathcal{Y} \Leftrightarrow
\mathcal{X} \sqsubseteq \Omega_{1c} \sqcup \mathcal{Y}$.

By atomisticity it is equivalent to:
$\atoms^{\mathfrak{A}}\Cor'\mathcal{X} \subseteq \atoms^{\mathfrak{A}}\mathcal{Y}
\Leftrightarrow
\atoms^{\mathfrak{A}}\mathcal{X} \subseteq \atoms^{\mathfrak{A}}(\Omega_{1c} \sqcup \mathcal{Y})$;
(theorem~\ref{dual-core-join})
$\atoms^{\mathfrak{A}}\Cor'\mathcal{X} \subseteq \atoms^{\mathfrak{A}}\mathcal{Y}
\Leftrightarrow
\atoms^{\mathfrak{A}}\mathcal{X} \subseteq \atoms^{\mathfrak{A}}\Omega_{1c} \cup \atoms^{\mathfrak{A}}\mathcal{Y}$;
what by below is equivalent to:
$\atoms^{\mathfrak{Z}}  \mathcal{X} \subseteq
\atoms^{\mathfrak{Z}}  \mathcal{Y} \Leftrightarrow
\atoms^{\mathfrak{A}}  \mathcal{X} \subseteq \atoms^{\mathfrak{A}}
\Omega_{1c} \cup \atoms^{\mathfrak{A}}  \mathcal{Y}$.

$\Cor' \mathcal{X} \sqsubseteq \mathcal{Y} \Leftrightarrow
\atoms^{\mathfrak{A}} \Cor' \mathcal{X} \subseteq
\atoms^{\mathfrak{A}}  \mathcal{Y} \Rightarrow
\atoms^{\mathfrak{Z}} \Cor' \mathcal{X} \subseteq
\atoms^{\mathfrak{Z}}  \mathcal{Y} \Leftrightarrow
\atoms^{\mathfrak{Z}}  \mathcal{X} \subseteq \atoms^{\mathfrak{Z}}
\mathcal{Y}$;

$\atoms^{\mathfrak{Z}}  \mathcal{X} \subseteq
\atoms^{\mathfrak{Z}}  \mathcal{Y} \Rightarrow
\text{(theorem~\ref{cor-join-atom})} \Rightarrow
\Cor' \mathcal{X}
\sqsubseteq \Cor' \mathcal{Y} \Rightarrow
\text{(theorem~\ref{f-cor-max})} \Rightarrow
\Cor' \mathcal{X} \sqsubseteq \mathcal{Y}$.

Finishing the proof
$\atoms^{\mathfrak{A}} \mathcal{X} \subseteq \atoms^{\mathfrak{A}}
\Omega_{1c} \cup \atoms^{\mathfrak{A}} \mathcal{Y} \Leftrightarrow
\atoms^{\mathfrak{A}} \mathcal{X} \subseteq
(\atoms^{\mathfrak{A}} \setminus \mathfrak{Z})
\cup \atoms^{\mathfrak{A}} \mathcal{Y} \Leftrightarrow
\atoms^{\mathfrak{Z}} \mathcal{X} \subseteq
\atoms^{\mathfrak{A}} \mathcal{Y} \Leftrightarrow
\atoms^{\mathfrak{Z}} \mathcal{X} \subseteq
\atoms^{\mathfrak{Z}} \mathcal{Y}$.
\end{widedisorder}
\end{proof}

Next there is an alternative proof of the above theorem.
This alternative proof requires additional condition
$\forall \alpha \in \atoms^{\mathfrak{Z}} \exists X \in \operatorname{coatoms}^{\mathfrak{Z}} : a
\nsqsubseteq X$ however.

\begin{proof}
Define $\Omega = \Omega_{1a} = \Omega_{1c}$.

It with join-closed core by theorem~\ref{semifilt-joinclosed}.

It's enough to prove that
\[
\mathcal{X}\sqsubseteq\Omega\sqcup^{\mathfrak{A}}\Cor'\mathcal{X}\quad\text{and}\quad\Cor'(\Omega\sqcup^{\mathfrak{A}}\mathcal{Y})\sqsubseteq\mathcal{Y}.
\]
$\Cor'(\Omega\sqcup^{\mathfrak{A}}\mathcal{Y}) =
\text{(theorem~\ref{dual-core-join})} =
\Cor'\Omega\sqcup^{\mathfrak{Z}}\Cor'\mathcal{Y} =
\text{(proposition~\ref{omega-bot})} =
\bot^{\mathfrak{Z}}\sqcup^{\mathfrak{Z}}\Cor'\mathcal{Y} \sqsubseteq
\text{(theorem~\ref{f-cor-max})} \sqsubseteq
\mathcal{Y}$.

$\Omega\sqcup^{\mathfrak{A}}\Cor'\mathcal{X} =
\bigsqcup\atoms(\Omega\sqcup^{\mathfrak{A}}\Cor'\mathcal{X}) =
\bigsqcup(\atoms\Omega\cup\Cor'\mathcal{X}) =
\bigsqcup\atoms\Omega\sqcup\bigsqcup\atoms\mathcal{X}) \sqsupseteq
\bigsqcup(\atoms\mathcal{X}\setminus\mathfrak{Z}) \sqcup
\bigsqcup(\atoms\mathcal{X}\cap\mathfrak{Z}) =
\bigsqcup((\atoms\mathcal{X}\setminus\mathfrak{Z}) \cup
(\atoms\mathcal{X}\cap\mathfrak{Z}) =
\bigsqcup\atoms\mathcal{X} = \mathcal{X}$.
\end{proof}

\begin{cor}
 Under conditions of the last theorem
 $\Cor'\bigsqcup^{\mathfrak{A}} S=\bigsqcup^{\mathfrak{A}} \rsupfun{\Cor'}S$.
\end{cor}

\begin{prop}
The following is an implications tuple:
\begin{enumerate}
 \item\label{corom-pow} $(\mathfrak{A},\mathfrak{Z})$ is a powerset
  filtrator.
 \item\label{corom-flt} $(\mathfrak{A},\mathfrak{Z})$ is a primary
  filtrator over a complete atomic boolean lattice.
 \item\label{corom-cond} All of the following:
  \begin{enumerate}
    \item $\mathfrak{A}$ is atomistic complete co-brouwerian lattice.
    \item $\mathfrak{Z}$ is a complete atomistic lattice.
    \item $(\mathfrak{A},\mathfrak{Z})$ is a filtered
      down-aligned filtrator with binarily meet-closed core.
  \end{enumerate}
 \item\label{corom-res} $\Cor'\mathcal{X} = \mathcal{X}\psetminus\Omega_{1c}$
\end{enumerate}
\end{prop}

\begin{proof}
~
\begin{enumerate}
 \item[\ref{corom-pow}$\Rightarrow$\ref{corom-flt}]
  Obvious.
 \item[\ref{corom-flt}$\Rightarrow$\ref{corom-cond}]
  Because complete atomic boolean lattice is isomorphic
  to a powerset.
 \item[\ref{corom-cond}$\Rightarrow$\ref{corom-res}]
  Theorems~\ref{cor-adjom} and~\ref{cobrow}.
\end{enumerate}
\end{proof}

\begin{prop}
  ~  
  \begin{enumerate}
    \item $\langle \Omega^{\mathsf{FCD}} \rangle \{ x \} = \Omega^U$;
    
    \item $\langle \Omega^{\mathsf{FCD}} \rangle p = \top$ for every
    nontrivial atomic filter $p$.
  \end{enumerate}
\end{prop}

\begin{proof}
  $\langle \Omega^{\mathsf{FCD}} \rangle \{ x \} =
  \bigsqcap^{\mathfrak{A}}_{y \in U} (U \setminus \{ y \}) = \Omega^U$;
  $\langle \Omega^{\mathsf{FCD}} \rangle p = \bigsqcap^{\mathfrak{A}}_{y
  \in U} \top = \top$.
\end{proof}

\begin{prop}
  $\tofcd \Omega^{\mathsf{RLD}} =
  \Omega^{\mathsf{FCD}}$.
\end{prop}

\begin{proof}
  $\tofcd \Omega^{\mathsf{RLD}} =
  \bigsqcap^{\mathsf{FCD}} \up \Omega^{\mathsf{RLD}} =
  \Omega^{\mathsf{FCD}}$.
\end{proof}

\begin{prop}
  $(\mathsf{RLD})_{\operatorname{out}} \Omega^{\mathsf{FCD}} =
  \Omega^{\mathsf{RLD}}$.
\end{prop}

\begin{proof}
  $(\mathsf{RLD})_{\operatorname{out}} \Omega^{\mathsf{FCD}} =
  \bigsqcap^{\mathsf{RLD}} \up \Omega^{\mathsf{FCD}} =
  \bigsqcap^{\mathsf{RLD}} \up \Omega^{\mathsf{RLD}} =
  \Omega^{\mathsf{RLD}}$.
\end{proof}

\begin{prop}
  $(\mathsf{RLD})_{\operatorname{in}} \Omega^{\mathsf{FCD}} = \Omega^{\mathsf{RLD}}$.
\end{prop}

\begin{proof}
  \begin{multline*}
  (\mathsf{RLD})_{\operatorname{in}} \Omega^{\mathsf{FCD}} = \bigsqcup
  \setcond{ a \times^{\mathsf{RLD}} b }{ a \in
  \atoms^{\mathscr{F}}, b \in \atoms^{\mathscr{F}}, a
  \times^{\mathsf{FCD}} b \sqsubseteq \Omega^{\mathsf{FCD}}
  } = \\
  \bigsqcup \setcond{ a \times^{\mathsf{RLD}} b }{
  a \in \atoms^{\mathscr{F}}, b \in
  \atoms^{\mathscr{F}}, \text{not $a$ and $b$ both trivial} } = \\
  \bigsqcup \setcond{ \bigsqcup \atoms (a \times^{\mathsf{RLD}} b)
  }{ a \in \atoms^{\mathscr{F}}, b \in
  \atoms^{\mathscr{F}}, \text{not $a$ and $b$ both trivial} } = \\
  \bigsqcup \bigcup \setcond{ \atoms (a \times^{\mathsf{RLD}} b) }{
  a \in \atoms^{\mathscr{F}}, b \in
  \atoms^{\mathscr{F}}, \text{not $a$ and $b$ both trivial} } = \\
  \bigsqcup \left( \text{nontrivial atomic reloids under $A \times B$} \right) =
  \Omega^{\mathsf{RLD}}.
  \end{multline*}
\end{proof}