2.11. Notion of Galois connection

The set of fixed points of a function f is written

Fix f ={x∈Dom f | f(x)=x} ⊂ Im f
Then,
Im f ⊂ Fix g ⇔ ((Im f ⊂ Dom g)∧(gf=f))
Im f= Fix f ⇔ ((Im f ⊂ Dom f)∧(ff=f)) : such a function f is called idempotent.

Definition. For any ordered sets E, F, denoting F the set F with the transposed order, the sets of (antitone) Galois connections between E and F, and monotone Galois connections from E to F, are defined by
Gal(E,F) = {(⊥,⊤) ∈ FE×EF|∀xE, ∀yF, xE⊤(y) ⇔ yF ⊥(x)} = tGal(F,E)
Gal+(E,F) = {(u,v) ∈ FE×EF|∀xE, ∀yF, xE v(y) ⇔ u(x) ≤F y} = Gal(E,F)

Fundamental example. Any relation RX×Y defines a (⊥, ⊤) ∈ Gal(℘(X),℘(Y)) by
AX, ⊥(A) ={yY |∀xA, x R y}= xAR(x)
BY, ⊤(B) ={xX |∀yB, x R y}={xX | BR(x)}
Then, ⊥(∅)=Y and ⊤(∅)=X.

Proof : ∀AX, ∀BFA ⊂ ⊤(B) ⇔ A×BRB ⊂ ⊥(A).∎
This will later be shown to be a bijection : Gal(℘(X),℘(Y)) ≅ ℘(X×Y).

Lemma. ∀⊥ ∈ FE, !⊤ ∈ EF,(⊥,⊤) ∈ Gal(E,F).
Proof: ∀⊤ ∈ EF, (⊥,⊤) ∈ Gal(E,F) ⇔ E০⊤ =⊥*F, but E is injective.∎

Properties. For all (⊥,⊤) ∈ Gal(E,F), the closures Cl =⊤০⊥ ∈ EE and Cl′=⊥০⊤ ∈ FF satisfy
1) Cl and Cl′ are extensive.
2) ⊥ and ⊤ are antitone
3) Cl and Cl′ are monotone
4) ⊥০⊤০⊥ = ⊥, and similarly ⊤০⊥০⊤ = ⊤
5) Im ⊤ = Im Cl = Fix Cl, called the set of closed elements of E
6) Cl০Cl = Cl
7) (⊥ strictly antitone) ⇔ Inj⊥ ⇔ Cl = IdE ⇔ Im⊤ =E
8) ∀x,x′ ∈ E, ⊥(x) ≤ ⊥(x′) ⇔ (Im⊤∩ ≤(x) ⊂ ≤(x′)).
9) Denoting K=Im⊤, ⊤০⊥|K= IdK thus ⊥|K is strictly antitone and ⊥|K−1 = ⊤|Im⊥.

Proofs:
1) ⊥(x) ≤ ⊥(x) ∴ x(⊥(x)).
1) ⇒2) ∀x,yE, xy ≤ ⊤(⊥(y))⇒⊥(y) ≤ ⊥(x).
1)∧2) ⇒4) IdE ≤ Cl ⇒⊥০Cl ≤ ⊥ ≤ Cl′০⊥ = ⊥০⊤০⊥.
4)⇒5) Cl = ⊤০⊥ ∴ Im Cl ⊂ Im⊤ ;
Cl০⊤ = ⊤ ∴ Im⊤ ⊂ Fix Cl ⊂ Im Cl.
2)⇒3) and 4)⇒6) are obvious.
7) (Inj⊥∧⊥০Cl =⊥) ⇔ Cl = IdE ⇔ (Im⊤ =E∧Cl০⊤ = ⊤);
Cl = IdE ⇒ ⊥ strictly antitone ⇒ Inj ⊥.
8) ⊥(x) ≤ ⊥(x′) ⇔ (∀yF, x≤⊤(y) ⇒ x′≤ ⊤(y)).
9) K= Fix(⊤০⊥) ⇒ ⊤০⊥০IdK=IdK.
Other proof : (⊥|K,⊤) ∈ Gal(K,F) with ⊤ surjective.
In ⊤|Im⊥০⊥|K=IdK the roles of ⊤ and ⊥ are symmetrical. ∎

Remark. Properties 1) and 2) conversely imply that (⊥,⊤) ∈ Gal(E,F).
Proof: ∀xE, ∀yF, x ≤ ⊤(y) ⇒ y ≤ ⊥(⊤(y)) ≤ ⊥(x).∎
Analogues of the above properties for monotone Galois connections are obtained by reversing the order in F: if (u,v) ∈ Gal+(E,F) then u and v are monotone, vu is extensive and uv ≤ IdF.

Closure. A closure of an ordered set E is an fEE such that, equivalently:
1) There exists a set F and an (u,v) ∈ Gal(E,F) or Gal+(E,F) such that vu=f
2) f is monotone, idempotent and extensive
3) ∀xE,∀y∈ Im f, xyf(x) ≤ y, i.e. (f, IdK) ∈ Gal+(E,K) where K=Im f

Proof of equivalence:

3)⇒1) ⇒2);
for 2) ⇒3), ∀xE,∀yK, xf(x) ≤ yxyf(x) ≤ f(y) = y. ∎

Notes:

To go further on Galois connections

1. First foundations of mathematics
2. Set theory (continued)
2.1. Tuples, families
2.2. Boolean operators on families of sets
2.3. Products, graphs and composition
2.4. Uniqueness quantifiers, functional graphs
2.5. The powerset axiom
2.6. Injectivity and inversion
2.7. Properties of binary relations ; ordered sets
2.8. Canonical bijections
2.9. Equivalence relations and partitions
2.10. Axiom of choice
2.11. Notion of Galois connection
3. Model theory