Shift Mapping is Lower Adjoint iff Appropriate Maxima Exist
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq}$ be a meet semilattice.
Then the following two conditions are equivalent:
- $(1): \quad \forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is lower adjoint
- $(2): \quad \forall x, t \in S: \max \set {s \in S: x \wedge s \preceq t}$ exists.
Proof
$(1) \implies (2)$
Assume that
- $\forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is lower adjoint
Let $x, t \in S$.
Define $f: S \to S$:
- $\forall s \in S: \map f s = x \wedge s$
By assumption:
- $f$ is lower adjoint
By definition of lower adjoint:
- $\exists g: S \to S: \struct {g, f}$ is Galois connection
By Galois Connection is Expressed by Maximum:
- $\forall s \in S: \map g s = \map \max {f^{-1} \sqbrk {s^\preceq} }$
Then:
- $\map \max {f^{-1} \sqbrk {t^\preceq} }$ exists.
By definition of image of set:
- $\max \set {s \in S: \map f s \in t^\preceq}$ exists.
By definition of lower closure of element:
- $\max \set {s \in S: x \wedge s \preceq t}$ exists.
$\Box$
$(2) \implies (1)$
Assume that:
- $\forall x, t \in S: \max \set {s \in S: x \wedge s \preceq t}$ exists.
Let $x \in S, f: S \to S$ such that:
- $\forall s \in S: \map f s = x \wedge s$
As maxima exist define a mapping $g: S \to S$:
- $\forall s \in S: \map g s = \map \max {f^{-1} \sqbrk {s^\preceq} }$
We will prove that:
- $f$ is an increasing mapping
Let $y, z \in S$ such that:
- $y \preceq z$
By definition of $f$:
- $\map f y = x \wedge y$ and $\map f z = x \wedge z$
Thus by Meet Semilattice is Ordered Structure:
- $\map f y \preceq \map f z$
By Galois Connection is Expressed by Maximum:
- $\struct {g, f}$ is a Galois connection
By definition:
- $f$ is a lower adjoint.
$\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:62