Set of Upper Closures of Compact Elements is Basis implies Complete Scott Topological Lattice is Algebraic
Theorem
Let $L = \struct {S, \preceq, \tau}$ be a complete Scott Definition:Topological Lattice.
Let $\BB = \set {x^\succeq: x \in \map K L}$ be a basis of $L$, where:
- $x^\succeq$ denotes the upper closure of $x$,
- $\map K L$ denotes the compact subset of $L$.
Then $L$ is algebraic.
Proof
Thus by Compact Closure is Directed:
- $\forall x \in S:x^{\mathrm {compact} }$ is directed
where $x^{\mathrm {compact} }$ denotes the compact closure of $x$.
Thus by definition of complete lattice:
- $L$ is up-complete.
Let $x \in S$.
By definition of lower closure of element:
- $x$ is upper closure for $x^\preceq$
By definition of supremum:
- $\map \sup {x^\preceq} \preceq x$
By Compact Closure is Intersection of Lower Closure and Compact Subset:
- $x^{\mathrm {compact} } = x^\preceq \cap \map K L$
- $x^{\mathrm {compact} } \subseteq x^\preceq$
- $\map \sup {x^{\mathrm {compact} } } \preceq \map \sup {x^\preceq}$
By definition of transitivity:
- $\map \sup {x^{\mathrm {compact} } } \preceq x$
Aiming for a contradiction, suppose
- $x \ne \map \sup {x^{\mathrm {compact} } }$
We will prove that:
- $x \notin \paren {x^{\mathrm {compact} } }^\preceq$
Aiming for a contradiction, suppose:
- $x \in \paren {\map \sup {x^{\mathrm {compact} } } }^\preceq$
By definition of lower closure of element:
- $x \preceq \map \sup {x^{\mathrm {compact} } }$
Thus by definition of antisymmetry:
- this contradicts $x \ne \map \sup {x^{\mathrm {compact} } }$
$\Box$
By definition of relative complement:
- $x \in \relcomp S {\paren {\map \sup {x^{\mathrm {compact} } } }^\preceq}$
By Complement of Lower Closure of Element is Open in Scott Topological Ordered Set:
- $\relcomp S {\paren {\map \sup {x^{\mathrm {compact} } } }^\preceq}$ is open.
By definition of basis:
- $\relcomp S {\paren {\map \sup {x^{\mathrm {compact} } } }^\preceq} = \bigcup \set {G \in \BB: G \subseteq \relcomp S {\paren {\map \sup {x^{\mathrm {compact} } } }^\preceq} }$
By definition of union:
- $\exists X \in \set {G \in \BB: G \subseteq \relcomp S {\paren {\map \sup {x^{\mathrm {compact} } } }^\preceq} }: x \in X$
Then:
- $X \in \BB \land X \subseteq \relcomp S {\paren {\map \sup {x^{\mathrm {compact} } } }^\preceq}$
By definition of $\BB$:
- $\exists k \in \map K L: X = k^\succeq$
By definition of compact subset:
- $k$ is compact.
By definition of upper closure of element:
- $k \preceq x$
By definition of compact closure:
- $k \in x^{\mathrm {compact} }$
By definitions of supremum and upper bound:
- $k \preceq \map \sup {x^{\mathrm {compact} } }$
By definition of upper closure of element:
- $\map \sup {x^{\mathrm {compact} } } \in X$
By gefinition of subset:
- $\map \sup {x^{\mathrm {compact} } } \in \relcomp S {\paren {\map \sup {x^{\mathrm {compact} } } }^\preceq}$
By definition of difference:
- $\map \sup {x^{\mathrm {compact} } } \notin \paren {\map \sup {x^{\mathrm {compact} } } }^\preceq$
Thus by definition of lower closure of element:
- this contradicts $\map \sup {x^{\mathrm {compact} } } \in \paren {\map \sup {x^{\mathrm {compact} } } }^\preceq$
$\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 WAYBEL14:45