Supremum of Ideals is Upper Adjoint
Theorem
Let $L = \struct {S, \vee, \preceq}$ be a bounded below continuous join semilattice.
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: \map f I = \sup I$
Then $f$ is an upper adjoint of Galois connection.
Proof
Define $d: S \to \map {\mathit {Ids} } L$
- $\forall t \in S: \map d t = \map \inf {f^{-1} \sqbrk {t^\succeq} }$
where
- $t^\succeq$ denotes the upper closure of $t$,
- $f^{-1} \sqbrk {t^\succeq} $ denotes the image of $t^\succeq$ over $f^{-1}$.
We will prove that
- $\forall t \in S: \map d t = \map \min {f^{-1} \sqbrk {t^\succeq} }$
Let $t \in S$.
By Continuous iff For Every Element There Exists Ideal Element Precedes Supremum:
- there exists an ideal $J$ in $L$ such that
- $t \preceq \sup J$ and for every ideal $K$ in $L$: $t \preceq \sup K \implies J \subseteq K$
We will prove that
- $\forall K \in \map {\mathit {Ids} } L: K$ is lower bound for $f^{-1} \sqbrk {t^\succeq} \implies K \precsim J$
Let $K \in \map {\mathit {Ids} } L$ such that
- $K$ is a lower bound for $f^{-1} \sqbrk {t^\succeq}$
By definition of $f$:
- $t \preceq \map f J$
By definition of upper closure of element:
- $\map f J \in t^\succeq$
By definition of image of set:
- $J \in f^{-1} \sqbrk {t^\succeq}$
Thus by definition of lower bound:
- $K \precsim J$
$\Box$
We will prove that:
- $J$ is a lower bound for $f^{-1} \sqbrk {t^\succeq}$
Let $K \in \map {\mathit {Ids} } L$ such that:
- $K \in f^{-1} \sqbrk {t^\succeq}$
By definition of image of set:
- $\map f K \in t^\succeq$
By definition of upper closure of element:
- $t \preceq \map f K$
By definition of $f$:
- $t \preceq \sup K$
Then
- $J \subseteq K$
Thus by definition of $\precsim$:
- $J \precsim K$
$\Box$
By definition of supremum:
- $t \preceq \map \sup {\map \inf {f^{-1} \sqbrk {t^\succeq} } }$
By definition of $f$:
- $t \preceq \map f {\map \inf {f^{-1} \sqbrk {t^\succeq} } }$
By definition of upper closure of element:
- $\map f {\map \inf {f^{-1} \sqbrk {t^\succeq} } } \in t^\succeq$
By definition of image of set:
- $\map \inf {f^{-1} \sqbrk {t^\succeq} } \in f^{-1} \sqbrk {t^\succeq}$
Thus by definition of smallest element:
- $\map d t = \map \min {f^{-1} \sqbrk {t^\succeq} }$
$\Box$
By Supremum of Ideals is Increasing:
- $f$ is an increasing mapping.
By Galois Connection is Expressed by Minimum:
- $\struct {f, d}$ is a Galois connection.
Hence $f$ is an upper adjoint of Galois connection.
$\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:3