Shift Mapping is Lower Adjoint iff Appropriate Maxima Exist

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