Set of Upper Closures of Compact Elements is Basis implies Complete Scott Topological Lattice is Algebraic

From ProofWiki
Jump to navigation Jump to search

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$

By Intersection is Subset:

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

By Supremum of Subset:

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

Retrieved from "https://proofwiki.org/w/index.php?title=Set_of_Upper_Closures_of_Compact_Elements_is_Basis_implies_Complete_Scott_Topological_Lattice_is_Algebraic&oldid=629290"