# All Infima Preserving Mapping is Upper Adjoint of Galois Connection

## Theorem

Let $\struct {S, \preceq}$ be a complete lattice.

Let $\struct {T, \precsim}$ be an ordered set.

Let $g: S \to T$ be all infima preserving mapping.

Then there exists a mapping $d: T \to S$ such that $\tuple {g, d}$ is Galois connection and:

- $\forall t \in T: \map d t = \map \min {g^{-1} \sqbrk {t^\succsim} }$

where:

- $\min$ denotes the minimum
- $g^{-1} \sqbrk {t^\succsim}$ denotes the image of $t^\succsim$ under relation $g^{-1}$
- $t^\succsim$ denotes the upper closure of $t$

## Proof

Define a mapping $d: T \to S$:

- $\forall t \in T: \map d t := \map \inf {g^{-1} \sqbrk {t^\succsim} }$

We will prove as lemma $1$ that

- $g$ is an increasing mapping.

Let $x, y \in S$ such that

- $x \preceq y$

By Upper Closure is Decreasing:

- $y^\succeq \subseteq x^\succeq$

By Infimum of Upper Closure of Element:

- $\map \inf {x^\succeq} = x$ and $\map \inf {y^\succeq} = y$

By definition of mapping preserves all infima:

- $g$ preserves the infimum on $x^\succeq$ and $g$ preserves the infimum on $y^\succeq$

By definition of mapping preserves the infimum of set:

- $\map \inf {\map {g^\to} {x^\succeq} } = \map g x$ and $\map \inf {\map {g^\to} {y^\succeq} } = \map g y$

By Image of Subset under Relation is Subset of Image/Corollary 2:

- $\map {g^\to} {y^\succeq} \subseteq \map {g^\to} {x^\succeq}$

Thus by Infimum of Subset:

- $\map g x \precsim \map g y$

This ends the proof of lemma $1$.

We will prove as lemma $2$ that

- $\forall t \in T: \map d t = \map \min {g^{-1} \sqbrk {t^\succsim} }$

Let $t \in T$.

By definition of $d$:

- $\map d t = \map \inf {g^{-1} \sqbrk {t^\succsim} }$

- $g \sqbrk {g^{-1} \sqbrk {t^\succsim} } \subseteq t^\succsim$

By Infimum of Subset and Infimum of Upper Closure of Element:

- $t = \map \inf {t^\succsim} \precsim \map \inf {g \sqbrk {g^{-1} \sqbrk {t^\succsim} } }$

By definition of upper closure of element:

- $\map \inf {g \sqbrk {g^{-1} \sqbrk {t^\succsim} } } \in t^\succsim$

By definition of complete lattice:

- $g^{-1} \sqbrk {t^\succsim}$ admits an infimum

By definitions mapping preserves the infimum:

- $\map \inf {g \sqbrk {g^{-1} \sqbrk {t^\succsim} } } = \map g {\map d t}$

Thus by definition of image of set:

- $\map d t \in g^{-1} \sqbrk {t^\succsim}$

Thus

- $\map d t = \map \min {g^{-1} \sqbrk {t^\succsim} }$

This ends the proof of lemma $2$.

Thus by Galois Connection is Expressed by Minimum:

- $\tuple {g, d}$ is a Galois connection.

Thus by lemma $2$:

- $\forall t \in T: \map d t = \map \min {g^{-1} \sqbrk {t^\succsim} }$

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