LARA

This is an old revision of the document!

Galois Connection

Galois connection is defined by two monotonic functions $\alpha : C \to A$ and $\gamma : A \to C$ between partial orders $\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 $(*)$ is equivalent to the conjunction of these two conditions:

\begin{eqnarray*} c &\leq& \gamma(\alpha(c)) \\ \alpha(\gamma(a)) &\sqsubseteq& a \end{eqnarray*}

hold for all $c$ and $a$.

Lemma: Let $\alpha$ and $\gamma$ satisfy the condition of Galois connection. Then the following three conditions are equivalent: