# 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$.

By Compact Closure is Subset of Way Below Closure:

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

By definitions of non-empty set and subset:

- $x^\ll \ne \O$

Thus by Non-Empty Way Below Closure is Directed in Join Semilattice:

- $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.

By Compact Closure is Subset of Way Below Closure:

- $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}$

By Operand is Upper Bound of Way Below Closure:

- $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} }$.

By Compact Closure is Subset of Way Below Closure:

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

By definition of subset:

By definition of continuous:

- $x^\ll$ is directed.

By Directed iff Finite Subsets have Upper Bounds:

- $\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} }$

Thus by Preceding implies if Less Upper Bound then Greater Upper Bound:

- $c$ is upper bound for $A$.

$\Box$

By Directed iff Finite Subsets have Upper Bounds:

- $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$

By Compact Closure is Subset of Way Below Closure:

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

By Upper Bound is Upper Bound for Subset:

- $\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.

By Upper Bounds are Equivalent implies Suprema are equal:

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

Thus by axiom of approximation:

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

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