Upper Adjoint Preserves All Infima
Theorem
Let $\left({S, \preceq}\right)$, $\left({T, \precsim}\right)$ be ordered sets.
Let $g: S \to T$ be an upper adjoint of Galois connection.
Then $g$ preserves all infima.
Proof
By definition of upper adjoint
- $\exists d: T \to S: \left({g, d}\right)$ is a Galois connection
Let $X$ be a subset of $S$ such that
- $X$ admits an infimum.
We will prove as lemma 1 that
- $\forall t \in T: t$ is lower bound for $g^\to\left({X}\right) \implies t \precsim g\left({\inf X}\right)$
Let $t \in T$ such that
- $t$ is lower bound for $g^\to\left({X}\right)$
We will prove as sublemma that
- $d\left({t}\right)$ is lower bound for $X$
Let $s \in X$.
By definition of image of set:
- $g\left({s})\right) \in g^\to\left({X}\right)$
By definition of lower bound:
- $t \precsim g\left({s}\right)$
Thus by definition of Galois connection:
- $d\left({t}\right) \preceq s$
This ends the proof of sublemma.
By definition of infimum:
- $d\left({t}\right) \preceq \inf X$
Thus by definition of Galois connection:
- $t \precsim g\left({\inf X}\right)$
This ends the proof of lemma 1.
We will prove as lemma 2 that
- $g\left({\inf X}\right)$ is lower bound for $g^\to\left({X}\right)$
Let $t \in g^\to\left({X}\right)$.
By definition of image of set:
- $\exists s \in S: s \in X \land g\left({s}\right) = t$
By definition of infimum:
- $\inf X$ is lower bound for $X$
By definition of lower bound:
- $\inf X \preceq s$
By definition of Galois connection:
- $g$ is increasing mapping.
Thus by definition of increasing mapping:
- $g\left({\inf X}\right) \precsim t$
This ends the proof of lemma 2.
Thus by definition of infimum:
- $g^\to\left({X}\right)$ admits an infimum
and
- $\inf\left({g^\to\left({X}\right)}\right) = g\left({\inf X}\right)$
Thus by definition:
- $g$ preserves infimum on $X$
Thus by definition:
- $g$ preserves all infima.
$\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_1:12