# Galois Connection

## Constructing Partial Orders using Maps

Example: Let be the set of all propositional formulas containing only variables . For a formula define

i.e. denotes the set of assignments for which is true. Note that is a tautology iff . Define ordering on formulas by

Is a partial order? Which laws does satisfy? End of example.

Lemma: Let be an lattice and a set. Let be an injective function. Define oder on by . Then is a partial order.

Note: even if had top and bottom element and was a lattice, the constructed order need not have top and bottom or be a lattice. For example, we take to be a subset of and define to be identity.

How can we ensure that we obtain a “nice” partial order?

## Galois Connection

Galois connection (named after Évariste Galois) is defined by two monotonic functions and between partial orders on and on , such that

for all and (intuitively, the condition means that is approximated by ).

Lemma: The condition holds iff the conjunction of these two conditions:

holds for all and .