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$
- $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$
- $\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$
\(\ds a\) | \(=\) | \(\ds a \wedge \top\) | Preceding iff Meet equals Less Operand | |||||||||||
\(\ds \) | \(=\) | \(\ds a \wedge \left({x \vee \neg x}\right)\) | definition of Boolean algebra | |||||||||||
\(\ds \) | \(=\) | \(\ds a \wedge x \vee a \wedge \neg x\) | definition of distributive lattice |
- $\inf \left\{ {x}\right\} = x$
- $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