Upper Adjoint of Galois Connection is Surjection implies Lower Adjoint at Element is Minimum of Preimage of Singleton of Element

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $L = \struct {S, \preceq}, R = \paren {T, \precsim}$ be ordered sets.

Let $g: S \to T, d:T \to S$ be mappings such that:

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

and

$g$ is a surjection.


Then

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


Proof

By definition of Galois connection:

$g$ is an increasing mapping.

Let $t \in T$.

By definition of surjection:

$\Img g = T$

By Image of Preimage under Mapping: Corollary:

$g \sqbrk {g^{-1} \sqbrk {t^\succeq} } = t^\succeq$

By Galois Connection is Expressed by Minimum:

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

By definition of min operation:

$\map d t = \inf \set {g^{-1} \sqbrk {t^\succeq} }$ and $\map d t \in g^{-1} \sqbrk {t^\succeq}$

By definition of image of set:

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

By definition of upper closure of element:

$t \precsim \map g {\map d t}$

By definition of minimum element:

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

By definition of infimum:

$\map d t$ is lower bound for $g^{-1} \sqbrk {t^\succeq}$

By definition of surjection:

$\exists s \in S: t = \map g s$

By definition of singleton:

$t \in \set t$

By Set is Subset of Upper Closure

$\set t \subseteq \set t^\succeq$

By Upper Closure of Singleton:

$\set t^\succeq = t^\succeq$

By definition of image of set:

$s \in g^{-1} \sqbrk {t^\succeq}$

By definition of lower bound:

$\map d t \preceq s$

By definition of increasing mapping:

$\map g {\map d t} \precsim t$

By definition of antisymmetry:

$\map g {\map d t} = t$

By definition of preimage of set:

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

By Preimage of Subset is Subset of Preimage:

$g^{-1} \sqbrk {\set t} \subseteq g^{-1} \sqbrk {t^\succeq}$

We will prove that

$\map d t$ is an infimum of $g^{-1} \sqbrk {\set t}$

Thus by Lower Bound is Lower Bound for Subset:

$\map d t$ is lower bound for $g^{-1} \sqbrk {\set t}$

Thus by definition:

$\forall s \in S: s$ is lower bound for $g^{-1} \sqbrk {\set t} \implies s \preceq \map d t$

$\Box$


Thus by definition of min operation:

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

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Upper_Adjoint_of_Galois_Connection_is_Surjection_implies_Lower_Adjoint_at_Element_is_Minimum_of_Preimage_of_Singleton_of_Element&oldid=628864"