Supremum of Ideals is Upper Adjoint implies Lattice is Continuous

From ProofWiki
Jump to navigation Jump to search

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