| |||||||||
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.
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.
Suppose (A, ≤) and (B, <=) are two partially ordered sets. A Galois connection between these posets consists of two monotone functions: F : A → B and G : B → A, such that for all a in A and b in B, we have
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. As detailed below, each part of a Galois connection uniquely determines the other mapping. Viewing two functions that form a Galois connections as two specifications of the same object, it is convenient to denote a pair of corresponding lower and upper adjoints by f* and f*, respectively. Note that the asterisk is placed above the function symbol to denote the lower adjoint.
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
Both notions of a Galois connection are still present in the literature. In BambooWeb 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.
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.
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* o f* is deflationary, while f* o f* 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* o f* is inflationary as shown above. Similarly, since f* o f* 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* o f* is idempotent.
The above findings can be summarized as follows: for a Galois connection, the composite f* o f* is monotone (being the composite of monotone functions), inflationary, and idempotent. This states the f* o f* is in fact a closure operator on A. Dually, f* o f* is monotone, deflationary, and idempotent. Such mappings are sometimes called kernel operators.
Conversely, any closure operator c on some poset A gives rise to the Galois connection with lower adjoint f* being just the corestriction of c to the image of c (i.e. as a surjective mapping the closure system c(A)). The upper adjoint f* is then given by the inclusion of c(A) into A, that maps each closed element to itself, considered as an element of A. In this way, closure operators and Galois connections are seen to be closely related, each specifying an instance of the other. Similar conclusions hold true for kernel operators.
The above considerations also show that closed elements of A (elements x with f*(f*(x)) = x) are mapped to elements within the range of the kernel operator f* o f*, and vice versa.
Another important property of Galois connections is that lower adjoints preserve all suprema that exist within their domain. Dually, upper adjoints preserve all existing infima. From these properties, one can also conclude monotonicity of the adjoints immediately. The complete lattices that preserves all suprema is the lower adjoint of a Galois connection.
In this situation, an important feature of Galois connections is that one adjoint uniquely determines the other. Hence one can strengthen the above statement to guarantee that any supremum-preserving map between complete lattices is the lower adjoint of a unique Galois connection. The main property to derive this uniqueness is the following: For every x in A, f*(x) is the least element y of B such that x ≤ f*(y). Dually, for every y in B, f*(y) is the greatest x in A such that f*(x) <= y. The existence of a certain Galois connection now implies the existence of the respective least or greatest elements, no matter whether the corresponding posets satisfy any completeness properties. Thus, when one adjoint of a Galois connection is given, the other can be defined via this property. On the other hand, some arbitrary function f is a lower adjoint iff each set of the form { x in A | f(x) <= b }, b in B, contains a greatest element. Again, this can be dualized for the upper adjoint.
Galois connections also provide an interesting class of mappings between posets which can be used to obtain categories of posets. Especially, it is possible to compose Galois connections: given Galois connections (f*, f*) between posets A and B and (g*, g*) between B and C, the composite (g* o f*, f* o g*) is also a Galois connection. When considering categories of complete lattices, this can be simplified to consindering just mappings preserving all suprema (or, alternatively, infima). Mapping complete lattices to their duals, this categories display auto duality, that are quite fundamental for obtaining other duality theorems. More special kinds of morphisms that induce adjoint mappings in the other direction are the morphisms usually considered for frames (or locales).
Every partially ordered set can be viewed as a category in a natural way: there is 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 was a time when posets were transformed into categories in a dual fashion, i.e. with arrows pointing in the opposite direction. This led to a complementary notation concerning 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.
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 using the original (antitone) definition: