Algebraic iff Continuous and For Every Way Below Exists Compact Between

Theorem

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

Then $L$ is algebraic if and only if:

$L$ is continuous and
$\forall x, y \in S: x \ll y \implies \exists k \in \map K L: x \preceq k \preceq y$

where

$\ll$ denotes the way below relation,
$\map K L$ denotes the compact subset of $L$.

Proof

Sufficient Condition

Let $L$ be algebraic.

We will prove that

$\forall x \in S: x^\ll$ is directed

where $x^\ll$ denotes way below closure of $x$.

Let $x \in S$.

By definition of algebraic:

$x^{\mathrm{compact} }$ is directed

where $x^{\mathrm{compact} }$ denotes the compact closure of $x$.

$x^{\mathrm{compact} } \subseteq x^\ll$

By definitions of non-empty set and subset:

$x^\ll \ne \O$
$x^\ll$ is directed.

$\Box$

Thus by definition of algebraic:

$L$ is up-complete.

We will prove that:

$L$ satisfies axiom of approximation

Let $x \in S$.

By previous:

$x^\ll$ is directed.

By definition of algebraic:

$x^{\mathrm{compact} }$ is directed.

By definition of up-complete:

$x^\ll$ admits a supremum

and

$x^{\mathrm{compact} }$ admits a supremum.
$x^{\mathrm{compact} } \subseteq x^\ll$
$\map \sup {x^{\mathrm {compact} } } \preceq \map \sup {x^\ll}$

By definition of algebraic:

$L$ satisfies axiom of K-approximation.

By definition of axiom of K-approximation:

$x \preceq \map \sup {x^\ll}$
$x$ is an upper bound for $x^\ll$.

By definition of supremum:

$\map \sup {x^\ll} \preceq x$

Thus by definition of antisymmetry:

$x = \map \sup {x^\ll}$

$\Box$

Hence $L$ is continuous.

Let $x, y \in S$ such that:

$x \ll y$

By definition of algebraic:

$D := y^{\mathrm{compact} }$ is directed.

By definition of axiom of K-approximation:

$y = \sup D$

By definition of way below relation:

$\exists d \in D: x \preceq d$

By definition of compact closure:

$d$ is compact.

Thus by definition of compact subset:

$d \in \map K L$

By definition of supremum:

$y$ is an upper bound for $D$.

Thus by definition of upper bound:

$x \preceq d \preceq y$

$\Box$

Necessary Condition

Suppose that:

$L$ is continuous

and:

$\forall x, y \in S: x \ll y \implies \exists k \in \map K L: x \preceq k \preceq y$

We will prove that:

$\forall x \in S: x^{\mathrm{compact} }$ is directed.

Let $x \in S$.

We will prove that:

for every finite subset $A$ of $x^{\mathrm{compact} }$: there exists $c \in x^{\mathrm{compact} }$: $c$ is an upper bound for $A$.

Let $A$ be a finite subset of $x^{\mathrm{compact} }$.

$x^{\mathrm{compact} } \subseteq x^\ll$

By definition of subset:

$A$ is a finite subset of $x^\ll$

By definition of continuous:

$x^\ll$ is directed.
$\exists b \in x^\ll: b$ is an upper bound for $A$.

By definition of way below closure:

$b \ll x$

By assumption:

$\exists c \in \map K L: b \preceq c \preceq x$

By definition of compact subset:

$c$ is compact.

Thus by definition of compact closure:

$c \in x^{\mathrm{compact} }$
$c$ is upper bound for $A$.

$\Box$

$x^{\mathrm{compact} }$ is directed.

$\Box$

Thus by definition of continuous:

$L$ is up-complete.

It remains to prove that:

$L$ satisfies axiom of K-approximation.

Let $x \in S$.

We will prove that:

$\forall z \in S: z$ is an upper bound for $x^{\mathrm{compact} } \implies z$ is an upper bound for $x^\ll$

Let $z \in S$ such that:

$z$ is an upper bound for $x^{\mathrm{compact} }$

Let $d \in x^\ll$.

By definition of way below closure:

$d \ll x$

By assumption:

$\exists k \in \map K L: d \preceq k \preceq x$

By definition of compact subset:

$k$ is compact.

By definition of compact closure:

$k \in x^{\mathrm{compact} }$

By definition of upper bound:

$k \preceq z$

Thus by definition of transitivity:

$d \preceq z$

$\Box$

$x^{\mathrm{compact} } \subseteq x^\ll$
$\forall z \in S: z$ is upper bound for $x^\ll \implies z$ is upper bound for $x^{\mathrm{compact} }$

By definition of continuous:

$x^\ll$ is directed.

By definition of up-complete:

$x^\ll$ admits a supremum.
$\map \sup {x^{\mathrm{compact} } } = \map \sup {x^\ll}$

Thus by axiom of approximation:

$x = \map \sup {x^{\mathrm{compact} } }$

$\blacksquare$