Editing Galois connection (section)

=== (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>