View source for Galois connection

{{Short description|Particular correspondence between two partially ordered sets}}
In [[mathematics]], especially in [[order theory]], a '''Galois connection''' is a particular correspondence (typically) between two [[partially ordered set]]s (posets).  Galois connections find applications in various mathematical theories. They generalize the [[fundamental theorem of Galois theory]] about the correspondence between [[subgroup]]s and [[field extension|subfields]], discovered by the French mathematician [[Évariste Galois]].

A Galois connection can also be defined on [[preordered set]]s or [[preordered class|classes]]; this article presents the common case of posets.
The literature contains two closely related notions of "Galois connection". In this article, we will refer to them as '''(monotone) Galois connections''' and '''antitone Galois connections'''.

A Galois connection is rather weak compared to an [[order isomorphism]] between the involved posets, but every Galois connection gives rise to an isomorphism of certain sub-posets, as will be explained below.
The term '''Galois correspondence''' is sometimes used to mean a [[bijective]] ''Galois connection''; this is simply an [[order isomorphism]] (or dual order isomorphism, depending on whether we take monotone or antitone Galois connections).

== Definitions ==

=== (Monotone) Galois connection ===
Let {{math|(''A'', ≤)}} and {{math|(''B'', ≤)}} be two [[partially ordered set]]s. A ''monotone Galois connection'' between these posets consists of two [[monotone function|monotone]]<ref>Monotonicity follows from the following condition. See the discussion of the [[#Properties|properties]]. It is only explicit in the definition to distinguish it from the alternative ''antitone'' definition. One can also define Galois connections as a pair of monotone functions that satisfy the laxer condition that for all {{mvar|x}} in {{mvar|A}}, {{math|''x'' ≤ ''g''(&thinsp;''f''&thinsp;(''x''))}} and for all {{mvar|y}} in {{mvar|B}}, {{math|''f''&thinsp;(''g''(''y'')) ≤ ''y''}}.</ref> [[function (mathematics)|functions]], {{math|''F'' : ''A'' → ''B''}} and {{math|''G'' : ''B'' → ''A''}}, such that for all {{mvar|a}} in {{mvar|A}} and {{mvar|b}} in {{mvar|B}}, we have

:{{math|''F''(''a'') ≤ ''b''}} [[if and only if]] {{math|''a'' ≤ ''G''(''b'')}}.

In this situation, {{mvar|F}} is called the '''lower adjoint''' of {{mvar|G}} and {{mvar|G}} is called the '''upper adjoint''' of ''F''. Mnemonically, the upper/lower terminology refers to where the function application appears relative to ≤.{{sfn|Gierz|Hofmann|Keimel|Lawson|2003| p= 23}} The term "adjoint" refers to the fact that monotone Galois connections are special cases of pairs of [[adjoint functors]] in [[category theory]] as discussed further below. Other terminology encountered here is '''left adjoint''' (respectively '''right adjoint''') for the lower (respectively upper) adjoint.

An essential property of a Galois connection is that an upper/lower adjoint of a Galois connection ''uniquely'' determines the other:

:{{math|''F''(''a'')}} is the least element {{math|{{overset|~|''b''}} }} with {{math|''a'' ≤ ''G''({{overset|~|''b''}})}}, and 
:{{math|''G''(''b'')}} is the largest element {{mvar|{{overset|~|''a''}}}} with {{math|''F''({{overset|~|''a''}}) ≤ ''b''}}.

A consequence of this is that if {{mvar|F}} or {{mvar|G}} is [[bijective]] then each is the [[inverse function|inverse]] of the other, i.e. {{math|1=''F'' = ''G''<sup> −1</sup>}}.

Given a Galois connection with lower adjoint {{mvar|F}} and upper adjoint {{mvar|G}}, we can consider the [[function composition|compositions]] {{math|''GF'' : ''A'' → ''A''}}, known as the associated [[closure operator]], and {{math|''FG'' : ''B'' → ''B''}}, known as the associated kernel operator. Both are monotone and [[idempotent]], and we have {{math|''a'' ≤ ''GF''(''a'')}} for all {{mvar|a}} in {{mvar|A}} and {{math|''FG''(''b'') ≤ ''b''}} for all {{mvar|b}} in {{mvar|B}}.

A '''Galois insertion''' of {{mvar|B}} into {{mvar|A}} is a Galois connection in which the kernel operator {{mvar|FG}} is the [[identity function|identity]] on {{mvar|B}}, and hence {{mvar|G}} is an order isomorphism of {{mvar|B}} [[surjective|onto]] the set of closed elements {{mvar|GF}}&hairsp;[{{mvar|A}}] of {{mvar|A}}.<ref>{{cite book | title=Semirings for Soft Constraint Solving and Programming | volume=2962 | series=Lecture Notes in Computer Science | issn=0302-9743 | first=Stefano | last=Bistarelli | chapter=8. Soft Concurrent Constraint Programming | publisher=[[Springer-Verlag]] | year=2004 | isbn=3-540-21181-0 | page=102 | doi=10.1007/978-3-540-25925-1_8 | arxiv=cs/0208008 }}</ref>

=== Antitone Galois connection ===
The above definition is common in many applications today, and prominent in [[lattice (order)|lattice]] and [[domain theory]]. However the original notion in Galois theory is slightly different. In this alternative definition, a Galois connection is a pair of ''antitone'', i.e. order-reversing, functions {{math|''F'' : ''A'' → ''B''}} and {{math|''G'' : ''B'' → ''A''}} between two posets {{mvar|A}} and {{mvar|B}}, such that

:{{math|''b'' ≤ ''F''(''a'')}} if and only if {{math|''a'' ≤ ''G''(''b'')}}.

The symmetry of {{mvar|F}} and {{mvar|G}} in this version erases the distinction between upper and lower, and the two functions are then called '''polarities''' rather than adjoints.{{sfn|Galatos|Jipsen|Kowalski|Ono|2007|p= 145}} Each polarity uniquely determines the other, since

:{{math|''F''(''a'')}} is the largest element {{mvar|b}} with {{math|''a'' ≤ ''G''(''b'')}}, and 
:{{math|''G''(''b'')}} is the largest element {{mvar|a}} with {{math|''b'' ≤ ''F''(''a'')}}.

The compositions {{math|''GF'' : ''A'' → ''A''}} and {{math|''FG'' : ''B'' → ''B''}} are the associated closure operators; they are monotone idempotent maps with the property {{math|''a'' ≤ ''GF''(''a'')}} for all {{mvar|a}} in {{mvar|A}} and {{math|''b'' ≤ ''FG''(''b'')}} for all {{mvar|b}} in {{mvar|B}}.

The implications of the two definitions of Galois connections are very similar, since an antitone Galois connection between {{mvar|A}} and {{mvar|B}} is just a monotone Galois connection between {{mvar|A}} and the [[duality (order theory)|order dual]] {{math|''B''<sup>op</sup>}} of {{mvar|B}}. All of the below statements on Galois connections can thus easily be converted into statements about antitone Galois connections.

== Examples ==

===Bijections===
The [[bijection]] of a pair of functions <math>f:X\to Y</math> and <math>g:Y\to X,</math> each other's inverse, forms a (trivial) Galois connection, as follows. Because the [[equality relation]] is reflexive, transitive and antisymmetric, it is, trivially, a [[partial order]], making <math>(X,=)</math> and <math>(Y,=)</math> partially ordered sets. Since <math>f(x)=y</math> if and only if <math>x=g(y),</math> we have a Galois connection.

===Monotone Galois connections===

====Floor; ceiling====
A monotone Galois connection between <math>\Z,</math> the set of [[integer]]s and <math>\R,</math> the set of [[real number]]s, each with its usual ordering, is given by the usual [[embedding]] function of the integers into the reals and the [[floor function]] truncating a real number to the greatest integer less than or equal to it. The embedding of integers is customarily done implicitly, but to show the Galois connection we make it explicit. So let <math>F:\Z\to\R</math> denote the embedding function, with <math>F(n)=n\in\R,</math> while <math>G:\R\to\Z</math> denotes the floor function, so <math>G(x)=\lfloor x\rfloor.</math> The equivalence <math>F(n)\leq x ~\Leftrightarrow~ n\leq G(x)</math> then translates to
:<math>n\leq x ~\Leftrightarrow~ n\leq\lfloor x\rfloor.</math>
This is valid because the variable <math>n</math> is restricted to the integers. The well-known properties of the floor function, such as <math>\lfloor x+n\rfloor=\lfloor x\rfloor+n,</math> can be derived by elementary reasoning from this Galois connection.

The dual orderings give another monotone Galois connection, now with the [[ceiling function]]:
:<math>x\leq n ~\Leftrightarrow~ \lceil x\rceil\leq n.</math>

====Power set; implication and conjunction====
For an order-theoretic example, let {{mvar|U}} be some [[set (mathematics)|set]], and let {{mvar|A}} and {{mvar|B}} both be the [[power set]] of {{mvar|U}}, ordered by [[set inclusion|inclusion]]. Pick a fixed [[subset]] {{mvar|L}} of {{mvar|U}}. Then the maps {{mvar|F}} and {{mvar|G}}, where {{math|''F''(''M''&hairsp;) {{=}} ''L'' ∩ ''M''}}, and {{math|''G''(''N''&hairsp;) {{=}} ''N'' ∪ (''U''&thinsp;\&thinsp;''L'')}}, form a monotone Galois connection, with {{mvar|F}} being the lower adjoint. A similar Galois connection whose lower adjoint is given by the meet ([[infimum]]) operation can be found in any [[Heyting algebra]]. Especially, it is present in any [[Boolean algebra (structure)|Boolean algebra]], where the two mappings can be described by {{math|''F''(''x'') {{=}} (''a'' ∧ ''x'')}} and {{math|''G''(&hairsp;''y'') {{=}} (&hairsp;''y'' ∨ ¬''a'') {{=}} (''a'' ⇒ ''y'')}}. In [[mathematical logic|logical]] terms: "implication from {{mvar|a}}" is the upper adjoint of "conjunction with {{mvar|a}}".

====Lattices====
Further interesting examples for Galois connections are described in the article on [[completeness (order theory)|completeness properties]]. Roughly speaking, it turns out that the usual functions ∨ and ∧ are lower and upper adjoints to the [[diagonal map]] {{math|''X'' → ''X'' × ''X''}}. The least and greatest elements of a partial order are given by lower and upper adjoints to the unique function {{math|''X'' → {1}.}} Going further, even [[complete lattice]]s can be characterized by the existence of suitable adjoints. These considerations give some impression of the ubiquity of Galois connections in order theory.

====Transitive group actions====
Let {{mvar|G}} [[group action|act]] [[Group action#Transitivity properties|transitively]] on {{mvar|X}} and pick some point {{mvar|x}} in {{mvar|X}}. Consider

:<math>\mathcal{B} = \{B \subseteq X : x \in B; \forall g \in G, gB = B \ \mathrm{or} \ gB \cap B = \emptyset\},</math>

the set of '''blocks''' containing {{mvar|x}}. Further, let <math>\mathcal{G}</math> consist of the [[subgroup]]s of {{mvar|G}} containing the [[Group action#Orbits and stabilizers|stabilizer]] of {{mvar|x}}.

Then, the correspondence <math>\mathcal{B} \to \mathcal{G}</math>:
:<math> B \mapsto H_B = \{g \in G : gx \in B\}</math>
is a monotone, [[injective function|one-to-one]] Galois connection.<ref>See Alperin, Bell, Groups and Representations (GTM 162), p. 32</ref> As a [[corollary]], one can establish that doubly transitive actions have no blocks other than the trivial ones (singletons or the whole of {{mvar|X}}): this follows from the stabilizers being maximal in {{mvar|G}} in that case. See [[2-transitive group|Doubly transitive group]] for further discussion.

====Image and inverse image====
If {{math|&thinsp;''f'' : ''X'' → ''Y''}} is a [[function (mathematics)|function]], then for any subset {{mvar|M}} of {{mvar|X}} we can form the [[image (mathematics)|image]] {{math|''F''(''M''&hairsp;) {{=}} &thinsp;''f''&thinsp;''M'' {{=}} {&thinsp;''f''&thinsp;(''m'') {{!}} ''m'' ∈ ''M''} }} and for any subset {{mvar|N}} of {{mvar|Y}} we can form the [[inverse image]] {{math|''G''(''N''&hairsp;) {{=}} &thinsp;''f''&nbsp;<sup>−1</sup>''N'' {{=}} {''x'' ∈ ''X'' {{!}} &thinsp;''f''&thinsp;(''x'') ∈ ''N''}.}} Then {{mvar|F}} and {{mvar|G}} form a monotone Galois connection between the power set of {{mvar|X}} and the power set of {{mvar|Y}}, both ordered by inclusion ⊆. There is a further adjoint pair in this situation: for a subset {{mvar|M}} of {{mvar|X}}, define {{math|''H''(''M'') {{=}} {''y'' ∈ ''Y'' {{!}} &thinsp;''f''&nbsp;<sup>−1</sup>{''y''} ⊆ ''M''}.}} Then {{mvar|G}} and {{mvar|H}} form a monotone Galois connection between the power set of {{mvar|Y}} and the power set of {{mvar|X}}. In the first Galois connection, {{mvar|G}} is the upper adjoint, while in the second Galois connection it serves as the lower adjoint.

In the case of a [[quotient group|quotient map]] between algebraic objects (such as [[group (mathematics)|groups]]), this connection is called the [[lattice theorem]]: subgroups of {{mvar|G}} connect to subgroups of {{math|''G''/''N''}}, and the closure operator on subgroups of {{mvar|G}} is given by {{math|{{overline|''H''}} {{=}} ''HN''}}.

====Span and closure====
Pick some mathematical object {{mvar|X}} that has an [[underlying set]], for instance a group, [[ring (mathematics)|ring]], [[vector space]], etc. For any subset {{mvar|S}} of {{mvar|X}}, let {{math|''F''(''S''&hairsp;)}} be the smallest [[subobject]] of {{mvar|X}} that contains {{mvar|S}}, i.e. the [[subgroup]], [[subring]] or [[linear subspace|subspace]] generated by {{mvar|S}}. For any subobject {{mvar|U}} of {{mvar|X}}, let {{math|''G''(''U''&hairsp;)}} be the underlying set of {{mvar|U}}. (We can even take {{mvar|X}} to be a [[topological space]], let {{math|''F''(''S''&hairsp;)}} the [[closure (topology)|closure]] of {{mvar|S}}, and take as "subobjects of {{mvar|X}}{{-"}} the [[closed subset]]s of {{mvar|X}}.) Now {{mvar|F}} and {{mvar|G}} form a monotone Galois connection between subsets of {{mvar|X}} and subobjects of {{mvar|X}}, if both are ordered by inclusion. {{mvar|F}} is the lower adjoint.

====Syntax and semantics====
A very general comment of [[William Lawvere]]<ref>[[William Lawvere]], Adjointness in foundations, Dialectica, 1969, [http://www.tac.mta.ca/tac/reprints/articles/16/tr16abs.html available here]. The notation is different nowadays; an easier introduction by Peter Smith [http://www.logicmatters.net/resources/pdfs/Galois.pdf in these lecture notes], which also attribute the concept to the article cited.</ref> is that ''syntax and semantics'' are adjoint: take {{mvar|A}} to be the set of all [[Theory (mathematical logic)|logical theories]] (axiomatizations) reverse ordered by strength, and {{mvar|B}} the power set of the set of all mathematical structures. For a theory {{math|''T'' ∈ ''A''}}, let {{math|Mod(''T''&hairsp;)}} be the set of all structures that satisfy the [[axiom]]s {{mvar|T}}&hairsp;; for a set of mathematical structures {{math|''S'' ∈ ''B''}}, let {{math|Th(''S''&hairsp;)}} be the minimum of the axiomatizations that approximate {{mvar|S}} (in [[first-order logic]], this is the set of sentences that are true in all structures in {{mvar|S}}). We can then say that {{mvar|S}} is a subset of {{math|Mod(''T''&hairsp;)}} if and only if {{math|Th(''S''&hairsp;)}} logically entails {{mvar|T}}: the "semantics functor" {{math|Mod}} and the "syntax functor" {{math|Th}} form a monotone Galois connection, with semantics being the upper adjoint.

===Antitone Galois connections===

====Galois theory====
The motivating example comes from Galois theory: suppose {{math|''L''/''K''}} is a [[field extension]]. Let {{mvar|A}} be the set of all subfields of {{mvar|L}} that contain {{mvar|K}}, ordered by inclusion ⊆. If {{mvar|E}} is  such a subfield, write {{math|Gal(''L''/''E'')}} for the group of [[field automorphism]]s of {{mvar|L}} that hold {{mvar|E}} fixed. Let {{mvar|B}} be the set of subgroups of {{math|Gal(''L''/''K'')}}, ordered by inclusion ⊆. For such a subgroup {{mvar|G}}, define {{math|Fix(''G'')}} to be the field consisting of all elements of {{mvar|L}} that are held fixed by all elements of {{mvar|G}}. Then the maps {{math|''E'' {{mapsto}} Gal(''L''/''E'')}} and {{math|''G'' {{mapsto}} Fix(''G'')}} form an antitone Galois connection.

====Algebraic topology: covering spaces====
Analogously, given a [[path-connected]] [[topological space]] {{mvar|X}}, there is an antitone Galois connection between subgroups of the [[fundamental group]] {{math|''π''<sub>1</sub>(''X'')}} and path-connected [[covering space]]s of {{mvar|X}}. In particular, if {{mvar|X}} is [[semi-locally simply connected]], then for every subgroup {{mvar|G}} of {{math|''π''<sub>1</sub>(''X'')}}, there is a covering space with {{mvar|G}} as its fundamental group.

====Linear algebra: annihilators and orthogonal complements====
Given an [[inner product space]] {{mvar|V}}, we can form the [[orthogonal complement]] {{math|''F''(''X''&hairsp;)}} of any subspace {{mvar|X}} of {{mvar|V}}. This yields an antitone Galois connection between the set of subspaces of {{mvar|V}} and itself, ordered by inclusion; both polarities are equal to {{mvar|F}}.

Given a [[vector space]] {{mvar|V}} and a subset {{mvar|X}} of {{mvar|V}} we can define its annihilator {{math|''F''(''X''&hairsp;)}}, consisting of all elements of the [[dual space]] {{math|''V''&hairsp;<sup>∗</sup>}} of {{mvar|V}} that vanish on {{mvar|X}}. Similarly, given a subset {{mvar|Y}} of {{math|''V''&hairsp;<sup>∗</sup>}}, we define its annihilator {{math|''G''(''Y''&thinsp;) {{=}} {&hairsp;''x'' ∈ ''V'' {{!}} ''φ''(''x'') {{=}} 0 ∀''φ'' ∈ ''Y''&hairsp;}.}} This gives an antitone Galois connection between the subsets of {{mvar|V}} and the subsets of {{math|''V''&hairsp;<sup>∗</sup>}}.

====Algebraic geometry====
In [[algebraic geometry]], the relation between sets of [[polynomial]]s and their zero sets is an antitone Galois connection.

Fix a [[natural number]] {{mvar|n}} and a [[field (mathematics)|field]] {{mvar|K}} and let {{mvar|A}} be the set of all subsets of the [[polynomial ring]] {{math|''K''[''X''<sub>1</sub>, ..., ''X<sub>n</sub>'']}} ordered by inclusion ⊆, and let {{mvar|B}} be the set of all subsets of {{math|''K''<sup>&hairsp;''n''</sup>}} ordered by inclusion ⊆. If {{mvar|S}} is a set of polynomials, define the [[Algebraic geometry#Affine varieties|variety]] of zeros as

:<math>V(S) = \{x \in K^n : f(x) = 0 \mbox{ for all } f \in S\},</math>

the set of common [[root of a polynomial|zeros]] of the polynomials in {{mvar|S}}. If {{mvar|U}} is a subset of {{math|''K''<sup>&hairsp;''n''</sup>}}, define {{math|''I''(''U''&hairsp;)}} as the [[ideal (ring theory)|ideal]] of polynomials vanishing on {{mvar|U}}, that is

:<math>I(U) = \{f \in K[X_1,\dots,X_n] : f(x) = 0 \mbox{ for all } x \in U\}.</math>

Then {{mvar|V}} and ''I'' form an antitone Galois connection.

The closure on {{math|''K''<sup>&hairsp;''n''</sup>}} is the closure in the [[Zariski topology]], and if the field {{mvar|K}} is [[Algebraically closed field|algebraically closed]], then the closure on the polynomial ring is the [[Radical of an ideal|radical]] of ideal generated by {{mvar|S}}.

More generally, given a [[commutative ring]] {{mvar|R}} (not necessarily a polynomial ring), there is an antitone Galois connection between radical ideals in the ring and Zariski closed subsets of the [[Algebraic geometry#Affine varieties|affine variety]] {{math|[[Spectrum of a ring|Spec]](''R'')}}.

More generally, there is an antitone Galois connection between ideals in the ring and [[subscheme]]s of the corresponding [[Algebraic geometry#Affine varieties|affine variety]].

====Connections on power sets arising from binary relations====
Suppose {{mvar|X}} and {{mvar|Y}} are arbitrary sets and a [[binary relation]] {{mvar|R}} over {{mvar|X}} and {{mvar|Y}} is given. For any subset {{mvar|M}} of {{mvar|X}}, we define {{math|''F''(''M''&hairsp;) {{=}} {&hairsp;''y'' ∈ ''Y'' {{!}} ''mRy'' ∀''m'' ∈ ''M''&hairsp;}.}} Similarly, for any subset {{mvar|N}} of {{mvar|Y}}, define {{math|''G''(''N''&hairsp;) {{=}} {&hairsp;''x'' ∈ ''X'' {{!}} ''xRn'' ∀''n'' ∈ ''N''&hairsp;}.}} Then {{mvar|F}} and {{mvar|G}} yield an antitone Galois connection between the power sets of {{mvar|X}} and {{mvar|Y}}, both ordered by inclusion ⊆.{{sfn|Birkhoff|1940|loc=§32; 3rd edition (1967): Ch. V, §7 and §8}}

Up to isomorphism ''all'' antitone Galois connections between power sets arise in this way. This follows from the "Basic Theorem on Concept Lattices".<ref>Ganter, B. and Wille, R. ''Formal Concept Analysis -- Mathematical Foundations'', Springer (1999), {{ISBN|978-3-540-627715}}</ref> Theory and applications of Galois connections arising from binary relations are studied in [[formal concept analysis]]. That field uses Galois connections for mathematical data analysis.  Many algorithms for Galois connections can be found in the respective literature, e.g., in.<ref>Ganter, B. and Obiedkov, S. ''Conceptual Exploration'', Springer (2016), {{ISBN|978-3-662-49290-1}}</ref>

The [[General Concept Lattice|general concept lattice]] in its primitive version incorporates both the monotone and antitone Galois connections to furnish its upper and lower bounds of nodes for the concept lattice, respectively.<ref name=":1">{{Cite journal |last1=Liaw |first1=Tsong-Ming |last2=Lin |first2=Simon C. |date=2020-10-12 |title=A general theory of concept lattice with tractable implication exploration |url=https://www.sciencedirect.com/science/article/pii/S0304397520302826 |url-status=live |journal=Theoretical Computer Science |language=en |volume=837 |pages=84–114 |doi=10.1016/j.tcs.2020.05.014 |issn=0304-3975 |s2cid=219514253 |archive-url=https://web.archive.org/web/20200528022615/https://www.sciencedirect.com/science/article/pii/S0304397520302826 |archive-date=2020-05-28 |access-date=2023-07-19}}</ref>

== Properties ==
In the following, we consider a (monotone) Galois connection {{math|&thinsp;''f'' {{=}} (&thinsp;''f''&nbsp;<sup>∗</sup>, &thinsp;''f''<sub>∗</sub>)}}, where {{math|&thinsp;''f''&nbsp;<sup>∗</sup> : ''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, {{math|&thinsp;''f''&nbsp;<sup>∗</sup>(''x'') ≤ &thinsp;''f''&nbsp;<sup>∗</sup>(''x'')}} is equivalent to {{math|''x'' ≤ &thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(''x''))}}, for all {{mvar|x}} in {{mvar|A}}. By a similar reasoning (or just by applying the [[duality (order theory)|duality principle for order theory]]), one finds that {{math|&thinsp;''f''&nbsp;<sup>∗</sup>(&thinsp;''f''<sub>∗</sub>(''y'')) ≤ ''y''}}, for all {{mvar|y}} in {{mvar|B}}. These properties can be described by saying the composite {{math|&thinsp;''f''&nbsp;<sup>∗</sup>∘&thinsp;''f''<sub>∗</sub>}} is ''deflationary'', while {{math|&thinsp;''f''<sub>∗</sub>∘&thinsp;''f''&nbsp;<sup>∗</sup>}} is ''inflationary'' (or ''extensive'').

Now consider {{math|''x'', ''y'' ∈ ''A''}} such that {{math|''x'' ≤ ''y''}}. Then using the above one obtains {{math|''x'' ≤ &thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(''y''))}}. Applying the basic property of Galois connections, one can now conclude that {{math|&thinsp;''f''&nbsp;<sup>∗</sup>(''x'') ≤ &thinsp;''f''&nbsp;<sup>∗</sup>(''y'')}}. But this just shows that {{math|&thinsp;''f''&nbsp;<sup>∗</sup>}} preserves the order of any two elements, i.e. it is monotone. Again, a similar reasoning yields monotonicity of {{math|&thinsp;''f''<sub>∗</sub>}}. 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 {{math|&thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(&thinsp;''f''<sub>∗</sub>(''x''))) {{=}} &thinsp;''f''<sub>∗</sub>(''x'')}}, for all {{mvar|x}} in {{mvar|B}}. Clearly we find that

:{{math|&thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(&thinsp;''f''<sub>∗</sub>(''x''))) ≥ &thinsp;''f''<sub>∗</sub>(''x'')}}.

because {{math|&thinsp;''f''<sub>∗</sub>∘&thinsp;''f''&nbsp;<sup>∗</sup>}} is inflationary as shown above. On the other hand, since {{math|&thinsp;''f''&nbsp;<sup>∗</sup>∘&thinsp;''f''<sub>∗</sub>}} is deflationary, while {{math|&thinsp;''f''<sub>∗</sub>}} is monotonic, one finds that

:{{math|&thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(&thinsp;''f''<sub>∗</sub>(''x''))) ≤ &thinsp;''f''<sub>∗</sub>(''x'')}}.

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

:{{math|&thinsp;''f''&nbsp;<sup>∗</sup>(&thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(&thinsp;''f''<sub>∗</sub>(''x'')))) {{=}} &thinsp;''f''&nbsp;<sup>∗</sup>(&thinsp;''f''<sub>∗</sub>(''x''))}}

and

:{{math|&thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(&thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(''x'')))) {{=}} &thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(''x''))}}

i.e., {{math|&thinsp;''f''&nbsp;<sup>∗</sup>∘&thinsp;''f''<sub>∗</sub>}} and {{math|&thinsp;''f''<sub>∗</sub>∘&thinsp;''f''&nbsp;<sup>∗</sup>}} are [[idempotent]].

It can be shown (see Blyth or Erné for proofs) that a function {{math|&thinsp;''f''&thinsp;}} is a lower (respectively upper) adjoint if and only if {{math|&thinsp;''f''&thinsp;}} is a [[residuated mapping]] (respectively residual mapping). Therefore, the notion of residuated mapping and monotone Galois connection are essentially the same.

== Closure operators and Galois connections ==
The above findings can be summarized as follows: for a Galois connection, the composite {{math|&thinsp;''f''<sub>∗</sub>∘&thinsp;''f''&nbsp;<sup>∗</sup>}} is monotone (being the composite of monotone functions), inflationary, and idempotent. This states that {{math|&thinsp;''f''<sub>∗</sub>∘&thinsp;''f''&nbsp;<sup>∗</sup>}} is in fact a [[closure operator]] on {{mvar|A}}. Dually, {{math|&thinsp;''f''&nbsp;<sup>∗</sup>∘&thinsp;''f''<sub>∗</sub>}} is monotone, deflationary, and idempotent. Such mappings are sometimes called '''kernel operators'''. In the context of [[frames and locales]], the composite {{math|&thinsp;''f''<sub>∗</sub>∘&thinsp;''f''&nbsp;<sup>∗</sup>}} is called the '''nucleus''' induced by {{math|&thinsp;''f''&nbsp;}}. Nuclei induce frame homomorphisms; a subset of a locale is called a sublocale if it is given by a nucleus.

[[Converse (logic)|Conversely]], any closure operator {{mvar|c}} on some poset {{mvar|A}} gives rise to the Galois connection with lower adjoint {{math|&thinsp;''f''&nbsp;<sup>∗</sup>}} being just the corestriction of {{mvar|c}} to the image of {{mvar|c}} (i.e. as a [[surjective]] mapping the closure system {{math|''c''(''A'')}}). The upper adjoint {{math|&thinsp;''f''<sub>∗</sub>}} is then given by the [[inclusion map|inclusion]] of {{math|''c''(''A'')}} into {{mvar|A}}, that maps each closed element to itself, considered as an element of {{mvar|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 {{mvar|A}} (elements {{mvar|x}} with {{math|&thinsp;''f''<sub>∗</sub>(&thinsp;''f''&nbsp;<sup>∗</sup>(''x'')) {{=}} ''x''}}) are mapped to elements within the range of the kernel operator {{math|&thinsp;''f''&nbsp;<sup>∗</sup>∘&thinsp;''f''<sub>∗</sub>}}, and vice versa.

== Existence and uniqueness of Galois connections ==
Another important property of Galois connections is that lower adjoints preserve all [[supremum|suprema]] that exist within their [[domain of a function|domain]]. Dually, upper adjoints preserve all existing [[infimum|infima]]. From these properties, one can also conclude monotonicity of the adjoints immediately. The [[adjoint functor theorem (order theory)|adjoint functor theorem for order theory]] states that the converse implication is also valid in certain cases: especially, any mapping between [[complete lattice]]s 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 {{mvar|x}} in {{mvar|A}}, {{math|&thinsp;''f''&nbsp;<sup>∗</sup>(''x'')}} is the least element {{mvar|y}} of {{mvar|B}} such that {{math|''x'' ≤ &thinsp;''f''<sub>∗</sub>(''y'')}}. Dually, for every {{mvar|y}} in {{mvar|B}}, {{math|&thinsp;''f''<sub>∗</sub>(''y'')}} is the greatest {{mvar|x}} in {{mvar|A}} such that {{math|&thinsp;''f''&nbsp;<sup>∗</sup>(''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 (order theory)|completeness properties]]. Thus, when one upper adjoint of a Galois connection is given, the other upper adjoint can be defined via this same property.

On the other hand, some monotone function {{math|&thinsp;''f''&nbsp;}} is a lower adjoint [[if and only if]] each set of the form {{math|{&hairsp;''x'' ∈ ''A'' {{!}} &thinsp;''f''&nbsp;(''x'') ≤ ''b''&hairsp;},}} for {{mvar|b}} in {{mvar|B}}, contains a greatest element. Again, this can be dualized for the upper adjoint.

== Galois connections as morphisms ==
Galois connections also provide an interesting class of mappings between posets which can be used to obtain [[category (mathematics)|categories]] of posets. Especially, it is possible to compose Galois connections: given Galois connections {{math|(&thinsp;''f''&nbsp;<sup>∗</sup>, &thinsp;''f''<sub>∗</sub>)}} between posets {{mvar|A}} and {{mvar|B}} and {{math|(''g''<sup>∗</sup>, ''g''<sub>∗</sub>)}} between {{mvar|B}} and {{mvar|C}}, the composite {{math|(''g''<sup>∗</sup> ∘ &thinsp;''f''&nbsp;<sup>∗</sup>, &thinsp;''f''<sub>∗</sub> ∘ ''g''<sub>∗</sub>)}} is also a Galois connection. When considering categories of complete lattices, this can be simplified to considering just mappings preserving all suprema (or, alternatively, infima). Mapping complete lattices to their duals, these categories display auto [[duality (category theory)|duality]], that are quite fundamental for obtaining other duality theorems. More special kinds of [[morphism]]s that induce adjoint mappings in the other direction are the morphisms usually considered for [[complete Heyting algebra|frames]] (or locales).

== Connection to category theory ==
Every partially ordered set can be viewed as a category in a natural way: there is a unique morphism from ''x'' to ''y'' if and only if {{math|''x'' ≤ ''y''}}. A monotone 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 morphisms pointing in the opposite direction. This led to a complementary notation concerning left and right adjoints, which today is ambiguous.

== Applications in the theory of programming ==
Galois connections may be used to describe many forms of abstraction in the theory of [[abstract interpretation]] of [[programming language]]s.<ref>{{cite book|author1=Patrick Cousot |author2=Radhia Cousot | chapter=Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints| title=[[ACM Symposium on Principles of Programming Languages|Proc. 4th ACM Symposium on Principles of Programming Languages (POPL)]]|date=Jan 1977| pages=238–252 |chapter-url=https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf}}<BR>For a counterexample for the false theorem in Sect.7 (p.243 top right), see: {{cite tech report|author1=Jochen Burghardt |author2=Florian Kammüller |author3=Jeff W. Sanders | title=Isomorphism of Galois Embeddings|date=Dec 2000| volume=122| page=9-14| institution=[[Gesellschaft für Mathematik und Datenverarbeitung|GMD]]| issn=1435-2702| url=http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=CAA7D4E037C54173D8EE894D00020684?doi=10.1.1.27.9114&rep=rep1&type=pdf}} (However the original article only considers complete lattices)</ref><ref>{{cite book|author1=Patrick Cousot |author2=Radhia Cousot | chapter=Systematic Design of Program Analysis Frameworks| title=Proc. 6th ACM Symp. on Principles of Programming Languages (POPL)|date=Jan 1979| pages=269–282| publisher=ACM Press| chapter-url=https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-79-ACM-p269--282-1979.pdf}}</ref>

== Notes ==
{{reflist}}

== References ==
''The following books and survey articles include Galois connections using the monotone definition:''
* Brian A. Davey and [[Hilary Priestley|Hilary A. Priestley]]: ''[[Introduction to Lattices and Order]]'', Cambridge University Press, 2002.
* {{cite book|first1=Gerhard |last1=Gierz |first2= Karl H.|last2= Hofmann|first3= Klaus|last3= Keimel|first4= Jimmie D.|last4= Lawson |first5= Michael W.|last5= Mislove|first6=Dana S. |last6=Scott|author-link6= Dana S. Scott |title= Continuous Lattices and Domains |publisher= Cambridge University Press |year= 2003}}
* Marcel Erné, Jürgen Koslowski, Austin Melton, George E. Strecker, ''A primer on Galois connections'', in: Proceedings of the 1991 Summer Conference on General Topology and Applications in Honor of Mary Ellen Rudin and Her Work, Annals of the New York Academy of Sciences, Vol. 704, 1993, pp.&nbsp;103–125. (Freely available online in various file formats [https://web.archive.org/web/20060108063506/http://www.iti.cs.tu-bs.de/TI-INFO/koslowj/RESEARCH/gal_bw.ps.gz PS.GZ] [http://www.math.ksu.edu/~strecker/primer.ps PS], it presents many examples and results, as well as  notes on the different notations and definitions that arose in this area.)

''Some publications using the original (antitone) definition:''
* {{cite book |first=Saunders |last=Mac Lane |author-link=Saunders Mac Lane|title=[[Categories for the Working Mathematician]] | edition=Second |date=September 1998 |publisher=Springer |isbn=0-387-98403-8}}
* Thomas Scott Blyth, ''Lattices and Ordered Algebraic Structures'', Springer, 2005, {{isbn|1-85233-905-5}}.
* {{cite book|first1=Nikolaos |last1=Galatos |first2=Peter |last2=Jipsen |first3=Tomasz |last3=Kowalski |first4=Hiroakira |last4=Ono |year=2007 |title=Residuated Lattices. An Algebraic Glimpse at Substructural Logics |publisher= Elsevier|isbn=978-0-444-52141-5}}
* {{cite book|first1=Garrett |last1=Birkhoff |author-link=Garrett Birkhoff |title= Lattice Theory |publisher=Amer. Math. Soc. Coll. Pub. |volume=25|year=1940}}
* {{citation|first=Øystein|last= Ore|author-link=Øystein Ore|title= Galois Connexions|journal=[[Transactions of the American Mathematical Society]]| volume=55 |issue= 3|year=1944|pages=493–513|doi=10.2307/1990305|jstor= 1990305}}

{{DEFAULTSORT:Galois Connection}}
[[Category:Galois theory]]
[[Category:Order theory]]
[[Category:Abstract interpretation]]
[[Category:Closure operators]]