Relative Pseudocomplement and Shift Mapping form Galois Connection in Brouwerian Lattice
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \vee, \wedge, \preceq}$ be a Brouwerian lattice.
Let $a$ be an element of $S$.
Let $g, d: S \to S$ be mappings such that:
- $\forall s \in S: \map g s = a \to s$
and
- $\forall s \in S: \map d s = a \wedge s$
Then $\struct {g, d}$ is a Galois connection.
Proof
By Brouwerian Lattice iff Shift Mapping is Lower Adjoint:
- $d$ is lower adjoint
By definition of lower adjoint:
- $\exists g': S \to S: \struct {g', d}$ is Galois connection
By Galois Connection is Expressed by Maximum:
- $\forall s \in S: \map {g'} s = \map \max {d^{-1} \sqbrk {s^\preceq} }$
By definition of image of set:
- $\forall s \in S: \map {g'} s = \map \max {\set {x \in S: \map d x \in s^\preceq} }$
By definition of lower closure of element:
- $\forall s \in S: \map {g'} s = \map \max {\set {x \in S: \map d x \preceq s} }$
By definition of $d$:
- $\forall s \in S: \map {g'} s = \map \max {\set {x \in S: a \wedge x \preceq s} }$
By definition of relative pseudocomplement:
- $\forall s \in S: \map {g'} s = a \to s = \map g s$
- $g = g'$
Hence
- $\struct {g, d}$ is a Galois connection.
$\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:def 20