Shift Mapping is Lower Adjoint iff Meet is Distributive with Supremum
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq}$ be a complete lattice.
Then:
- $\forall x \in S, f: S \to S: \paren {\forall y \in S: \map f y = x \wedge y} \implies f$ is lower adjoint of a Galois connection
- $\forall x \in S, X \subseteq S: x \wedge \sup X = \sup \set {x \wedge y: y \in X}$
Proof
Sufficient Condition
Assume that
- $\forall x \in S, f: S \to S: \paren {\forall y \in S: \map f y = x \wedge y} \implies f$ is lower adjoint of a Galois connection
Let $x \in S, X \subseteq S$.
Define a mapping $f: S \to S$:
- $\forall y \in S: \map f y := x \wedge y$
By assumption:
By Lower Adjoint Preserves All Suprema:
By definition of mapping preserves all suprema
- $f$ preserves the supremum of $X$.
By definition of complete lattice:
- $X$ admits a supremum.
Thus
\(\ds x \wedge \sup X\) | \(=\) | \(\ds \map f {\sup X}\) | Definition of $f$ | |||||||||||
\(\ds \) | \(=\) | \(\ds \map \sup {\map {f^\to} X}\) | Definition of Mapping Preserves Supremum | |||||||||||
\(\ds \) | \(=\) | \(\ds \sup \set {\map f y: y \in X}\) | Definition of Image of Subset under Mapping | |||||||||||
\(\ds \) | \(=\) | \(\ds \sup \set {x \wedge y: y \in X}\) | Definition of $f$ |
$\Box$
Necessary Condition
Assume that
- $\forall x \in S, X \subseteq S: x \wedge \sup X = \sup \set {x \wedge y: y \in X}$
Let $x \in S$, $f: S \to S$ such that
- $\forall y \in S: \map f y = x \wedge y$
We will prove that
Let $X \subseteq S$ such that
- $X$ admits a supremum.
Thus by definition of complete lattice:
- $\map {f^\to} X$ admits a supremum.
Thus
\(\ds \map \sup {\map {f^\to} X}\) | \(=\) | \(\ds \sup \set {\map f y: y \in X}\) | Definition of Image of Subset under Mapping | |||||||||||
\(\ds \) | \(=\) | \(\ds \sup \set {x \wedge y: y \in X}\) | Definition of $f$ | |||||||||||
\(\ds \) | \(=\) | \(\ds x \wedge \sup X\) | by hypothesis | |||||||||||
\(\ds \) | \(=\) | \(\ds \map f {\sup X}\) | Definition of $f$ |
Thus by definition
- $f$ preserves the supremum of $X$.
$\Box$
Thus by All Suprema Preserving Mapping is Lower 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_1:64