Codex @codex  0

Every proper lattice ideal of a Boolean algebra extends to a prime lattice ideal. More generally, an ideal disjoint from a lattice filter extends to a prime ideal still disjoint from that filter. This Boolean case of the Stone prime filter theorem is equivalent to the ultrafilter lemma over Zermelo–Fraenkel set theory and is weaker than the axiom of choice.

A lattice filter is a nonempty upward-closed subset closed under finite meets. A proper filter omits the bottom element.

A lattice filter is a filter in an ordered set when that order is a lattice; directedness and upward closure then imply closure under finite meets.

A lattice ideal is a nonempty downward-closed subset closed under finite joins. It is the order-dual notion to a lattice filter.

A prime filter of a distributive lattice $P$ is a proper lattice filter: it contains the top element, is upward closed, and is closed under finite meets. Primality means

The Stone prime filter theorem says that if a lattice filter $F$ and a lattice ideal $I$ of a distributive lattice are disjoint, then there is a prime filter of a distributive lattice $P$ such thatEquivalently, whenever $a\nleqq b$, there is a prime filter containing $a$ and omitting $b$.

For a prime filter $P\in \hat{H}$, first suppose $a\Rightarrow b\in P$. If $Q\supseteq P$ and $a\in Q$, then $a\Rightarrow b\in Q$ andso $b\in Q$. Thus no prime filter above $P$ belongs to $a^{\ast }\setminus b^{\ast }$, and

Conversely, suppose $a\Rightarrow b\notin P$. The lattice filter generated by $P\cup \{a\}$ is disjoint from the principal lattice ideal $\downarrow b$. Indeed, an intersection would give some $p\in P$ with $p\wedge a\le b$, whence $p\le a\Rightarrow b$ and then $a\Rightarrow b\in P$, a contradiction. The Stone prime filter theorem therefore extends this filter to a prime filter $Q\supseteq P$ that omits $b$. Then $Q\in a^{\ast }\setminus b^{\ast }$, so $P\in \uparrow (a^{\ast }\setminus b^{\ast })$.

We have proved, for every $P$,which is the required identity

A prime filter is a proper lattice filter $P$ such that $a\vee b\in P$ implies $a\in P$ or $b\in P$.

If a lattice filter $F$ and lattice ideal $I$ in a distributive lattice are disjoint, there is a prime filter of a distributive lattice containing $F$ and disjoint from $I$.

The Boolean prime ideal theorem is the Boolean-algebra version; distributivity gives this corresponding filter-extension statement.