Editing Galois connection (section)

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