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

From ProofWiki
Jump to navigation Jump to search


This article needs to be tidied.
In particular: haven't got the patience tonight
Please fix formatting and $\LaTeX$ errors and inconsistencies. It may also need to be brought up to our standard house style.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Tidy}} from the code.


Theorem

Let $L = \struct {S, \preceq, \tau}$ be a complete Scott Definition:Topological Lattice.

Let $\BB = \left\{ {x^\succeq: x \in K\left({L}\right)}\right\}$ be a basis of $L$

where

$x^\succeq$ denotes the upper closure of $x$,
$K\left({L}\right)$ 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:

$\sup \left({x^\preceq}\right) \preceq x$

By Compact Closure is Intersection of Lower Closure and Compact Subset:

$x^{\mathrm{compact} } = x^\preceq \cap K\left({L}\right)$

By Intersection is Subset:

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

By Supremum of Subset:

$\sup \left({x^{\mathrm{compact} } }\right) \preceq \sup \left({x^\preceq}\right)$

By definition of transitivity:

$\sup \left({x^{\mathrm{compact} } }\right) \preceq x$

Aiming for a contradiction, suppose

$x \ne \sup \left({x^{\mathrm{compact} } }\right)$

We will prove that

$x \notin \left({\left({x^{\mathrm{compact} } }\right) }\right)^\preceq$

Aiming for a contradiction, suppose

$x \in \left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq$

By definition of lower closure of element:

$x \preceq \sup \left({x^{\mathrm{compact} } }\right)$

Thus by definition of antisymmetry:

this contrasicts $x \ne \sup \left({x^{\mathrm{compact} } }\right)$

$\Box$

By definition of relative complement:

$x \in \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)$

By Complement of Lower Closure of Element is Open in Scott Topological Ordered Set:

$\complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)$ is open.

By definition of basis:

$\complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right) = \bigcup\left\{ {G \in \BB: G \subseteq \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)}\right\}$

By definition of union

$\exists X \in \left\{ {G \in \BB: G \subseteq \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)}\right\}: x \in X$

Then

$X \in \BB \land X \subseteq \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)$

By definition of $\BB$:

$\exists k \in K\left({L}\right): 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 \sup \left({x^{\mathrm{compact} } }\right)$

By definition of upper closure of element:

$\sup \left({x^{\mathrm{compact} } }\right) \in X$

By gefinition of subset:

$\sup \left({x^{\mathrm{compact} } }\right) \in \complement_S\left({\left({\sup \left({x^{\mathrm{compact} } }\right) }\right)^\preceq}\right)$

By definition of difference:

$\sup \left({x^{\mathrm{compact} } }\right) \notin \left({\sup \left({x^{\mathrm{compact} } }\right)}\right)^\preceq$

Thus by definition of lower closure of element:

this contradicts $\sup \left({x^{\mathrm{compact} } }\right) \in \left({\sup \left({x^{\mathrm{compact} } }\right)}\right)^\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=572199"