Supremum of Ideals is Upper Adjoint implies Lattice is Continuous
Theorem
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below up-complete lattice.
Let $\map {\mathit {Ids} } L$ be the set of all ideals in $L$.
Let $P = \struct {\map {\mathit {Ids} } L, \precsim}$ be an ordered set where $\mathord \precsim = \subseteq \restriction_{\map {\mathit {Ids} } L \times \map {\mathit {Ids} } L}$
Let $f: \map {\mathit {Ids} } L \to S$ be a mapping such that
- $\forall I \in \map {\mathit {Ids} } L: f \sqbrk I = \sup I$
Let $f$ be an upper adjoint of a Galois connection.
Then $L$ is continuous.
Proof
We will prove that
- $\forall x \in S: \exists I \in \map {\mathit {Ids} } L: x \preceq \sup I \land \forall J \in \map {\mathit {Ids} } L: x \preceq \sup J \implies I \subseteq J$
Let $x \in S$.
Define $I := \map \inf {f^{-1} \sqbrk {x^\succeq} }$.
By definition of $P$:
- $I \in \map {\mathit {Ids} } L$
We will prove that
- $\forall J \in \map {\mathit {Ids} } L: x \preceq \sup J \implies I \subseteq J$
Let $J \in \map {\mathit {Ids} } L$ such that
- $x \preceq \sup J$
By definition of $f$:
- $x \preceq f \sqbrk J$
By definition of upper closure of element:
- $f \sqbrk J \in x^\succeq$
By definition of image of set:
- $J \in f^{-1} \sqbrk {x^\succeq}$
By definition of infimum:
- $I \precsim J$
Hence by definition of $\precsim$:
- $I \subseteq J$
$\Box$
By definition of upper adjoint of a Galois connection:
- there exists a mapping $d: S \to \map {\mathit {Ids} } L$: $\struct {f, d}$ is a Galois connection.
By Galois Connection is Expressed by Minimum
- $\map d x = \map \min {f^{-1} \sqbrk {x^\succeq} }$
By definition of smallest element:
- $I \in f^{-1} \sqbrk {x^\succeq}$
By definition of image of set:
- $f \sqbrk I \in x^\succeq$
By definition of upper closure of element:
- $x \preceq f \sqbrk I$
Thus by definition of $f$:
- $x \preceq \sup I$
Hence
- $\exists I \in \map {\mathit {Ids} } L: x \preceq \sup I \land \forall J \in \map {\mathit {Ids} } L: x \preceq \sup J \implies I \subseteq J$
$\Box$
Hence by Continuous iff For Every Element There Exists Ideal Element Precedes Supremum:
- $L$ is continuous.
$\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_5:4