\import{set.tex}
\import{set/powerset.tex}

\section{Filters}

\subsection{Definition and basic properties of filters}

\begin{abbreviation}\label{upwardclosed}
    $F$ is upward-closed in $S$ iff
    for all $A, B$ such that $A\subseteq B\subseteq S$ and $A\in F$ we have $B\in F$.
\end{abbreviation}

\begin{definition}\label{filter}
    $F$ is a filter on $S$ iff
    $F$ is a family of subsets of $S$
    and $S\in F$
    and $\emptyset\notin F$
    and $F$ is closed under binary intersections
    and $F$ is upward-closed in $S$.
\end{definition}

\begin{proposition}\label{filter_ext_complement}
    Let $F, G$ be filters on $S$.
    Suppose for all $A\subseteq S$ we have $S\setminus A\in F$ iff $S\setminus A\in G$.
    Then $F = G$.
\end{proposition}
\begin{proof}
    We have for all $X\in F$ we have $X\in G$
        by \cref{filter,setminus_subseteq,double_relative_complement}.
    We have for all $X\in G$ we have $X\in F$
        by \cref{filter,setminus_subseteq,double_relative_complement}.
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{filter_inter_in_iff}
    Let $F$ be a filter on $S$.
    Suppose $A, B\subseteq S$.
    Then $A\inter B\in F$ iff $A, B\in F$.
\end{proposition}
\begin{proof}
    We have $A\inter B\subseteq A, B$ by \cref{inter,subseteq}.
    Follows by \cref{filter}.
\end{proof}

\begin{proposition}\label{filter_setminus_in}
    Let $F$ be a filter on $S$.
    Suppose $A\in F$.
    Suppose $B\subseteq S$ and $S\setminus B\in F$.
    Then $A\setminus B\in F$.
\end{proposition}
\begin{proof}
    We have $A\subseteq S$ by \cref{filter}.
    Thus $A\setminus B = A\inter (S\setminus B)$ by \cref{setminus_eq_inter_complement}.
    Now $S\setminus B\subseteq S$ by \cref{setminus_subseteq}.
    Follows by \cref{filter_inter_in_iff}.
\end{proof}

\begin{proposition}\label{filter_in_iff_exists_subset}
    Let $F$ be a filter on $S$.
    Suppose $B\subseteq S$.
    Then $B\in F$ iff there exists $A\subseteq B$ such that $A\in F$.
\end{proposition}
\begin{proof}
    Follows by \cref{filter,subseteq_refl}.
\end{proof}


\subsection{Principal filters over a set}

\begin{definition}\label{principalfilter}
    $\principalfilter{S}{A} = \{X\in\pow{S}\mid A\subseteq X\}$.
\end{definition}

\begin{proposition}\label{principalfilter_iff}
    Suppose $A, B\subseteq S$.
    Then $B\in\principalfilter{S}{A}$ iff $A\subseteq B$.
\end{proposition}
\begin{proof}
    We have $B\subseteq S$ by assumption.
    We have $B\in\pow{S}$ by \cref{pow_iff,subseteq}.
    Follows by \cref{principalfilter}.
\end{proof}

\begin{proposition}\label{principalfilter_bottom}
    Suppose $A\subseteq S$.
    Then $A\in\principalfilter{S}{A}$.
\end{proposition}
\begin{proof}
    Follows by \cref{principalfilter_iff,subseteq_refl}.
\end{proof}

\begin{proposition}\label{principalfilter_top}
    Suppose $A\subseteq S$.
    Then $S\in\principalfilter{S}{A}$.
\end{proposition}
\begin{proof}
    Follows by \cref{principalfilter_iff,subseteq_refl}.
\end{proof}

\begin{proposition}\label{principalfilter_is_filter}
    Suppose $A\subseteq S$.
    Suppose $A$ is inhabited.
    Then $\principalfilter{S}{A}$ is a filter on $S$.
\end{proposition}
\begin{proof}
    $S$ is inhabited by \cref{subseteq}.
    $\principalfilter{S}{A}$ is a family of subsets of $S$
        by \cref{principalfilter,pow_iff,subseteq}.
    $S\in \principalfilter{S}{A}$ by \cref{principalfilter_top}.
    $\emptyset\notin \principalfilter{S}{A}$
        by \cref{principalfilter_iff,subseteq_emptyset_iff}.
    $\principalfilter{S}{A}$ is closed under binary intersections
        by \cref{principalfilter_iff,subseteq_inter_iff,inter_subseteq}.
    $\principalfilter{S}{A}$ is upward-closed in $S$
        by \cref{principalfilter_iff,subseteq_transitive}.
    Follows by \cref{filter}.
\end{proof}

\begin{proposition}\label{principalfilter_elem_generator}
    Suppose $A\subseteq S$.
    $A\in\principalfilter{S}{A}$.
\end{proposition}
\begin{proof}
    Follows by \cref{principalfilter_bottom}.
\end{proof}

\begin{proposition}\label{principalfilter_notelem_implies_notsupseteq}
    Let $X\in\pow{S}$.
    Suppose $X\notin\principalfilter{S}{A}$.
    Then $A\not\subseteq X$.
\end{proposition}
\begin{proof}
    Follows by \cref{principalfilter}.
\end{proof}

\begin{definition}\label{maximalfilter}
    $F$ is a maximal filter on $S$ iff
    $F$ is a filter on $S$ and there exists no filter $F'$ on $S$ such that $F\subset F'$.
\end{definition}

\begin{proposition}\label{principalfilter_singleton_is_filter}
    Suppose $a\in S$.
    Then $\principalfilter{S}{\{a\}}$ is a filter on $S$.
\end{proposition}
\begin{proof}
    $\{a\}\subseteq S$ by \cref{singleton_subset_intro}.
    $\{a\}$ is inhabited by \cref{cons_iff}.
    Follows by \cref{principalfilter_is_filter}.
\end{proof}

\begin{proposition}\label{principalfilter_singleton_is_maximal_filter}
    Suppose $a\in S$.
    Then $\principalfilter{S}{\{a\}}$ is a maximal filter on $S$.
\end{proposition}
\begin{proof}
    $\{a\}\subseteq S$ by \cref{singleton_subset_intro}.
    $\{a\}$ is inhabited by \cref{cons_iff}.
    Thus $\principalfilter{S}{\{a\}}$ is a filter on $S$ by \cref{principalfilter_is_filter}.
    Show for all $F'$ such that $F'$ is a filter on $S$
        and $\principalfilter{S}{\{a\}}\subseteq F'$
        we have $F'\subseteq\principalfilter{S}{\{a\}}$.
    \begin{subproof}
        Fix $F'$.
        Assume $F'$ is a filter on $S$
            and $\principalfilter{S}{\{a\}}\subseteq F'$.
        We have $\{a\}\in F'$
            by \cref{principalfilter_bottom,elem_subseteq}.
        Show for all $X\in F'$ we have $X\in\principalfilter{S}{\{a\}}$.
        \begin{subproof}
            Fix $X$.
            Assume $X\in F'$.
            We have $X\inter\{a\}\in F'$
                by \cref{filter,filter_inter_in_iff}.
            Thus $X\inter\{a\}\neq\emptyset$ by \cref{filter}.
            Take $b$ such that $b\in X\inter\{a\}$
                by \cref{emptyset,setext}.
            We have $b\in X$ by \cref{inter}.
            We have $b = a$ by \cref{inter,cons_iff,emptyset}.
            Thus $a\in X$ by assumption.
            Thus $\{a\}\subseteq X$ by \cref{singleton_subset_intro}.
            Follows by \cref{filter,principalfilter_iff}.
        \end{subproof}
        Follows by \cref{subseteq}.
    \end{subproof}
    We have for all $F'$ such that $F'$ is a filter on $S$
        and $\principalfilter{S}{\{a\}}\subseteq F'$
        we have $F'=\principalfilter{S}{\{a\}}$
        by \cref{subseteq_antisymmetric}.
    Follows by \cref{maximalfilter,subset}.
\end{proof}