2.13. 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 ggf=f)
Im f = Fix f ⇔ (Im f ⊂ Dom fff=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)

General example. Any relation RX×Y defines a (⊥,⊤) ∈ Gal(℘(X),℘(Y)) by
AX, ⊥(A) ={yY | ∀xA, x R y} = xA R(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:

More on Galois connections

Set theory and Foundations of Mathematics
1. First foundations of mathematics
2. Set theory
2.1. Formalization of set theory
2.2. Set generation principle
2.3. Tuples, families
2.4. Boolean operators on families of sets
2.5. Products, graphs and composition
2.6. Uniqueness quantifiers, functional graphs
2.7. The powerset
2.8. Injectivity and inversion
2.9. Binary relations ; order
2.10. Canonical bijections
2.11. Equivalence relations and partitions
2.12. Axiom of choice
2.13. Galois connection
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
3. Algebra - 4. Arithmetic - 5. Second-order foundations