Differences

This shows you the differences between two versions of the page.

--- sav08:galois_connection_on_lattices [2008/05/07 10:14]
vkuncak
+++ sav08:galois_connection_on_lattices [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-==== Galois Connection ====
-Galois connection is defined by two monotonic functions $\alpha : C \to A$ and $\gamma : A \to C$ between [[:partial order]]s $\leq$ on $C$ and $\sqsubseteq$ on $A$, such that
-\begin{equation*}
-  \alpha(c) \sqsubseteq a\ \iff\ c \leq \gamma(a) \qquad (*)
-\end{equation*}
-for all $c$ and $a$ (intuitively, the condition means that $c$ is approximated by $a$).
-**Lemma:** The condition $(*)$ holds iff the conjunction of these two conditions:
-\begin{eqnarray*}
-  c &\leq& \gamma(\alpha(c)) \\
-  \alpha(\gamma(a)) &\sqsubseteq& a
-\end{eqnarray*}
-holds for all $c$ and $a$.
-**Lemma:** Let $\alpha$ and $\gamma$ satisfy the condition of Galois connection.  Then the following three conditions are equivalent:
-  * $\alpha(\gamma(a)) = a$ for all $a$
-  * $\alpha$ is a [[wk>surjective function]]
-  * $\gamma$ is an [[wk>injective function]]
-===== Using Galois Connection =====
-Define $sp^\#$ using $\alpha$ and $\gamma$:
-++++|
-\[
-    sp^\#(a,r) = \alpha(sp(\gamma(a),r)
-\]
-++++
-===== Best Abstract Transformer =====