Way Below in Meet-Continuous Lattice

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be a meet-continuous bounded below lattice.

Let $x, y \in S$.


Then $x \ll y$ if and only if

$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y = \sup I \implies x \in I$

where

$\ll$ denotes the way below relation,
$\map {\operatorname {Ids} } {\mathscr S}$ denotes the set of all ideals in $\mathscr S$.


Proof

Sufficient Condition

Let $x \ll y$

Let $I \in \map {\operatorname {Ids} } {\mathscr S}$ such that

$y = \sup I$

By definition of reflexivity:

$y \preceq \sup I$

By definition of meet-continuous:

$\mathscr S$ is up-complete.

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

$x \in I$

$\Box$


Necessary Condition

Assume:

$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y = \sup I \implies x \in I$

We will prove that:

$\forall I \in \map {\operatorname {Ids} } {\mathscr S}: y \preceq \sup I \implies x \in I$

Let $I \in \map {\operatorname {Ids} } {\mathscr S}$ such that

$y \preceq \sup I$

By definition of ideal:

$I$ is directed and lower.

Define $Y := \set {y \wedge d: d \in I}$

By Set of Finite Suprema is Directed:

$\set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}$ is directed.

where $\map {\operatorname {Fin} } Y$ denotes the set of all finite subsets of $Y$.

By definition of up-complete:

$\set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}$ admits a supremum.

By definition of union:

$Y = \bigcup \map {\operatorname {Fin} } Y$
\(\ds y\) \(=\) \(\ds y \wedge \sup I\) Preceding iff Meet equals Less Operand
\(\ds \) \(=\) \(\ds \sup Y\) Definition of Meet-Continuous Lattice
\(\ds \) \(=\) \(\ds \sup \set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}\) Supremum of Suprema
\(\ds \) \(=\) \(\ds \sup \set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}^\preceq\) Supremum of Lower Closure of Set

where $^\preceq$ denotes the lower closure of set.


By Lower Closure of Directed Subset is Ideal:

$\set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}^\preceq$ is an ideal in $\mathscr S$

By assumption:

$x \in \set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}^\preceq$

By definition of lower closure of set:

$\exists z \in \set {\sup A: A \in \map {\operatorname {Fin} } Y \land A \ne \O}: x \preceq z$

Then

$\exists A \in \map {\operatorname {Fin} } Y: z = \sup A \land A \ne \O$

We will prove as a sublemma that:

$A \subseteq I$

Let $a \in A$.

By definition of subset:

$a \in Y$

By definition of $Y$:

$\exists i \in I: a = y \wedge i$

By Meet Precedes Operands:

$a \preceq i$

Thus by definition of lower section:

$a \in I$

This ends the proof of sublemma.

By Directed iff Finite Subsets have Upper Bounds:

$\exists h \in I: \forall a \in A: a \preceq h$

By definition:

$h$ is upper bound for $A$

By definition of supremum:

$z = \sup A \preceq h$

By definition of transitivity:

$x \preceq h$

Thus by definition of lower section:

$x \in I$

$\Box$


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

$x \ll y$

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Way_Below_in_Meet-Continuous_Lattice&oldid=664922"