Way Below iff Second Operand Preceding Supremum of Prime Ideal implies First Operand is Element of Ideal

Theorem

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a distributive complete lattice.

Let $x, y \in S$.

Then $x \ll y$ if and only if:

for every prime ideal $P$ in $L$: $y \preceq \sup P \implies x \in P$

Proof

Sufficient Condition

The result follows by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal.

$\Box$

Necessary Condition

Suppose

for every prime ideal $P$ in $L$:

$y \preceq \sup P \implies x \in P$

We will prove that:

for every ideal $I$ in $L$: $y \preceq \sup I \implies x \in I$

Let $I$ be an ideal in $L$ such that

$y \preceq \sup I$

Aiming for a contradiction, suppose

$x \notin I$

By If Element Does Not Belong to Ideal then There Exists Prime Ideal Including Ideal and Excluding Element:

there exists a prime ideal $P$ in $L$: $I \subseteq P$ and $x \notin P$

By Supremum of Subset:

$\sup I \preceq \sup P$

By definition of transitivity:

$y \preceq \sup P$

By assumption:

$x \in P$

Thus by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:

$x \ll y$

$\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:32