Proper and Prime iff Ultrafilter in Boolean Lattice

Theorem

Let $B = \left({S, \vee, \wedge, \neg, \preceq}\right)$ be a Boolean lattice.

Let $F$ be a filter in $B$.

Then

$F$ is a proper subset of $S$ and $F$ is a prime filter in $B$

if and only if:

$F$ is ultrafilter on $B$

Proof

Sufficient Condition

Let us assume

$F$ is a proper subset of $S$ and $F$ is a prime filter in $B$.

Thus

$F$ is a proper subset of $S$.

Let $G$ be a filter in $B$ such that

$F \subseteq G$ and $F \ne G$.

By definitions of subset and set equality:

$\exists x: x \in G \land x \notin F$

By definition of Boolean algebra:

$x \vee \neg x = \top$

where $\top$ denotes the top of $B$.

By Top in Filter:

$\top \in F$

By definition of prime filter:

$\neg x \in F$

By definition of subset:

$\neg x \in G$

By Filtered in Meet Semilattice:

$x \wedge \neg x \in G$

By definition of Boolean algebra:

$\bot \in G$

Thus by definition of subset:

$G \subseteq S$

By definition of set equality it remains to prove that

$S \subseteq G$

Let $y \in S$.

By definition of smallest element:

$\bot \preceq y$

Thus by definition of upper set:

$y \in G$

$\Box$

Necessary Condition

Let $F$ be ultrafilter on $B$.

Thus by definition of ultrafilter:

$F$ is proper subset of $S$.

Let $x \in S$.

Aiming for a contradiction suppose that

$x \notin F$ and $\neg x \notin F$

By Finite Infima Set and Upper Closure is Smallest Filter:

$F \cup \left\{ {x}\right\} \subseteq {\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq$

By Set is Subset of Union:

$\left\{ {x}\right\} \subseteq F \cup \left\{ {x}\right\}$ and $F \subseteq F \cup \left\{ {x}\right\}$

By definition of singleton:

$x \in \left\{ {x}\right\}$

By definition of subset:

$x \in {\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq$

By Finite Infima Set and Upper Closure is Filter:

${\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq$ is filter in $L$.

By Subset Relation is Transitive:

$F \subseteq {\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq$

By definition of ultrafilter:

${\operatorname{fininfs}\left({F \cup \left\{ {x}\right\} }\right)}^\succeq = S$

By Finite Subset Bounds Element of Finite Infima Set and Upper Closure:

$\exists a \in S: a \in F \land \neg x \succeq a \wedge \inf \left\{ {x}\right\}$

By definition of greatest element:

$a \preceq \top$

\(\displaystyle a\)

\(=\)

\(\displaystyle a \wedge \top\)

Preceding iff Meet equals Less Operand

\(\displaystyle \)

\(=\)

\(\displaystyle a \wedge \left({x \vee \neg x}\right)\)

definition of Boolean algebra

\(\displaystyle \)

\(=\)

\(\displaystyle a \wedge x \vee a \wedge \neg x\)

definition of distributive lattice

By Infimum of Singleton:

$\inf \left\{ {x}\right\} = x$

By Meet Precedes Operands:

$a \wedge \neg x \preceq \neg x$

By definition of infimum:

$a \preceq \neg x$

By definition of upper set:

$\neg x \in F$

This contradicts $\neg x \notin F$

Thus by Proof by Contradiction:

$F$ is a prime filter by Filter is Prime iff For Every Element Element either Negation Belongs to Filter in Boolean Lattice.

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article WAYBEL_7:22