Galois connection

In mathematics, especially in order theory, a Galois connection is a particular correspondence between two partially ordered sets ("posets"). Galois connections generalize the correspondence between subgroups and subfields investigated in Galois theory. They find applications in various mathematical theories as well as in the theory of programming.

Properties

In the following, we consider a (monotone) Galois connection f = (f ∗, f ∗), where f ∗: A → B is the lower adjoint as introduced above. Some helpful and instructive basic properties can be obtained immediately. By the defining property of Galois connections, f ∗(x) ≤ f ∗(x) is equivalent to x ≤ f ∗( f ∗(x)), for all x in A. By a similar reasoning (or just by applying the duality principle for order theory), one finds that f ∗( f ∗(y)) ≤ y, for all y in B. These properties can be described by saying the composite f ∗circf ∗ is deflationary, while f ∗circf ∗ is inflationary (or extensive).

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Now if one considers any elements x and y of A such that x ≤ y, then one can clearly use the above findings to obtain

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

x ≤ f ∗(f ∗(y)). Applying the basic property of Galois connections, one can now conclude that f ∗(x) ≤ f ∗(y). But this just shows that f ∗ preserves the order of any two elements, i.e. it is monotone. Again, a similar reasoning yields monotonicity of f ∗. Thus monotonicity does not have to be included in the definition explicitly. However, mentioning monotonicity helps to avoid confusion about the two alternative notions of Galois connections.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Another basic property of Galois connections is the fact that f ∗(f ∗(f ∗(x))) = f ∗(x), for all x in B. Clearly we find that

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:f ∗(f ∗(f ∗(x))) ≥ f ∗(x)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

because f ∗circf ∗ is inflationary as shown above. Similarly, since f ∗circf ∗ is deflationary, one finds that

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:f ∗ f ∗ f ∗ f ∗(x) ≤ f ∗ f ∗(x) ≤ x,

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

which is equivalent to

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:f ∗(f ∗(f ∗(x))) ≤ f ∗(x).

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

This shows the desired equality. Furthermore, we can use this property to conclude that

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:f ∗(f ∗(f ∗(f ∗(x)))) = f ∗(f ∗(x)),

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

i.e., f ∗circf ∗ is idempotent.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~