# 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 .