Galois connection
In mathematics, 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.A Galois connection is rather weaker than an isomorphism between the involved posets, but every Galois connection gives rise to an isomorphism of certain sub-posets, as will be explained below.
| Table of contents |
|
2 Examples 3 Properties 4 Category theoretic approach 5 Applications in the theory of programming 6 References |
Suppose (A, ≤) and (B, <=) are two partially ordered sets. A Galois connection between these posets consists of two monotone functionss: F : A → B and G : B → A, such that for all a in A and b in B, we have
Definition
In this situation, F is called the lower adjoint of G and G is called the upper adjoint of F. This terminology relates to the connections to category theory discussed below.
The above definition is common in many applications today, and prominent in lattice and domain theory. However, a slightly different notion has originally been derived in Galois theory. In this alternative definition, a Galois connection is a pair of antitone, i.e. order-reversing, functions F : A → B and G : B → A between two posets A and B, such that
The implications of both definitions are in fact very similar, since an antitone Galois connection between A and B is just a monotone Galois connection between A and the order dual Bop of B. All of the below statements on Galois connections can thus easily be converted into statements about antitone Galois connections.
Note however that for an antitone Galois connection, it does not make sense to talk about the lower and upper adjoint: the situation is completely symmetrical.
Here we assume that F : A → B is the lower adjoint and G : B → A is the upper adjoint of a monotone Galois connection between (A,≤) and (B,<=).
The upper adjoint G preserves infima (meets) of arbitrary subsets of B, and the lower adjoint F preserves suprema (joins) of arbitrary subsets of A.
We have a ≤ G(F(a)) and F(G(b)) <= b for all a in A and b in B.
For every a, F(a) is the least x such that a ≤ G(x). For every b, G(b) is the largest y such that F(y) <= b.
This latter statement shows that a monotonic function F : A → B forms the lower adjoint of a Galois connection if and only if for every b in B, the set {y in A : F(y) <= b} has a largest element. If this is the case, then the upper adjoint G is uniquely determined by F: it just picks out this largest element.
In particular, this shows that if A is a complete lattice, then a function F : A → B forms the lower adjoint of a Galois connection if and only if F transforms suprema into suprema.
Importantly, every Galois connection gives rise to a closure operator and a corresponding notion of "closed elements" in A and B. F and G induce inverse monotone bijections between these sets of closed elements. The details:
We have FGF(a) = F(a) for every a in A and GFG(b) = G(b) for every b in B. We can use this to show that GF has the formal properties of a closure operator on A, and FG is a closure operator on B. An element a in A is called closed if a = G(F(a)), or equivalently, if a is in the range of G.
Closed elements of B are defined analogously. So F maps the closed elements of A to the closed elements of B, and G maps the closed elements of B to those of A. These two maps are monotone and inverse to each other.
Galois connection can be composed: if (F,G) is a Galois connection between the posets A and B, and (H,K) is a Galois connection between B and C, then (HoF,KoG) is a Galois connection between A and C (the lower adjoints are composed to yield the new lower adjoint, the upper adjoints are composed to yield the new upper adjoint).
Every partially ordered set can be viewed as a category in a natural way: there's a unique morphism from x to y iff x ≤ y. A Galois connection is then nothing but a pair of adjoint functors between two categories that arise from partially ordered sets. In this context, the upper adjoint is the right adjoint while the lower adjoint is the left adjoint. However, this terminology is avoided for Galois connections, since there has been a time when posets where transformed into categories in a dual fashion, i.e. with arrows pointing in the opposite direction. This led to a complementary notation concering left and right adjoints, which today is ambiguous.
Galois connections may be used to described many forms of abstractions in the theory of abstract interpretation of programming languages.
Alternative Definition
Both notions of a Galois connection are still present in the literature. In Wikipedia the term (monotone) Galois connection will always refer to a Galois connection in the former sense. If the alternative definition is applied, the term antitone Galois connection or order-reversing Galois connection is used. Examples
Properties
Category theoretic approach
Applications in the theory of programming
References
A freely available introduction to Galois connections, presenting many examples and results. Also includes notes on the different notations and definitions that arose in this area:
The following standard reference books also include Galois connections using modern notation and definitions:
Finally, some publications of historical interest are given below: