Shift Mapping is Lower Adjoint iff Meet is Distributive with Supremum

From ProofWiki
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

if and only if:

$\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:

$f$ is lower adjoint of a Galois connection.

By Lower Adjoint Preserves All Suprema:

$f$ 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

$f$ preserves all suprema.

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:

$f$ is lower adjoint of a Galois connection.

$\blacksquare$


Sources