Lecture VI — Exercise 6.25 (Scott 1981, PRG-19): the Galois connection of a

projection pair

Exercise 6.25. For a projection pair g : 𝒟 → ℰ and h : ℰ → 𝒟 show that for x ∈ |𝒟| and y ∈ |ℰ| we have

g(x) ⊑ y ↔ x ⊑ h(y).

Thus conclude

h(y) = ⊔ {x ∈ |𝒟| ∣ g(x) ⊑ y} and g(x) = ⊓ {y ∈ |ℰ| ∣ x ⊑ h(y)},

so each of the two functions determines the other. Check that the set in the first equation is directed, and that the set in the second is non-empty. Prove also that g maps consistent sets to consistent sets and preserves ⊔ (not just directed unions).

Dictionary to the codebase

Scott's g is the injection i and his h is the projection j of Proposition 6.12; we carry them abstractly in Subsystem.ProjectionPair 𝒟 ℰ (fields inj = g, proj = h) together with the two defining laws

• proj_comp_inj : h ∘ g = I_𝒟 (P.proj.comp P.inj = idMap 𝒟), and
• inj_comp_proj_le : g ∘ h ⊆ I_ℰ (P.inj.comp P.proj ≤ idMap ℰ).

On elements (toElementMap) these read h(g(x)) = x (proj_inj_apply) and g(h(y)) ⊑ y (inj_proj_apply_le); everything below is a short consequence of these two facts plus monotonicity of approximable maps on elements (toElementMap_mono).

• galois — the adjunction g(x) ⊑ y ↔ x ⊑ h(y).
• proj_eq_sSup / lowerSet_directed — h(y) = ⊔ {x ∣ g(x) ⊑ y}; the set is a down-set of h(y), hence directed and bounded by h(y).
• inj_eq_sInf — g(x) = ⊓ {y ∣ x ⊑ h(y)}; the set is an up-set of g(x), hence non-empty (it contains g(x)).
• inj_bounded — g maps bounded ("consistent") sets to bounded sets.
• inj_sSup — g preserves all existing least upper bounds: g(⊔S) = ⊔ {g(s) ∣ s ∈ S}. This is the hallmark of a lower adjoint and is the substance of the last sentence of the exercise.

Everything here is choice-free (#print axioms ⊆ {propext, Quot.sound}): the sSup/sInf of Exercises 1.18/1.27 are the only constructions used and are themselves choice-free.

theorem Domain.Neighborhood.Subsystem.ProjectionPair.proj_inj_apply {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (x : D.Element) : P.proj.toElementMap (P.inj.toElementMap x) = x

h(g(x)) = x. The first projection-pair law h ∘ g = I_𝒟, read on elements.

theorem Domain.Neighborhood.Subsystem.ProjectionPair.inj_proj_apply_le {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (y : E.Element) : P.inj.toElementMap (P.proj.toElementMap y) ≤ y

g(h(y)) ⊑ y. The second projection-pair law g ∘ h ⊆ I_ℰ, read on elements.

theorem Domain.Neighborhood.Subsystem.ProjectionPair.galois {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (x : D.Element) (y : E.Element) : P.inj.toElementMap x ≤ y ↔ x ≤ P.proj.toElementMap y

Exercise 6.25, the Galois connection. For x ∈ |𝒟|, y ∈ |ℰ|: g(x) ⊑ y ↔ x ⊑ h(y). So g (lower adjoint) and h (upper adjoint) determine each other.

→: apply the monotone h to g(x) ⊑ y and use h(g(x)) = x. ←: apply the monotone g to x ⊑ h(y) and use g(h(y)) ⊑ y.

First extremal formula: h(y) = ⊔ {x ∣ g(x) ⊑ y}.

def Domain.Neighborhood.Subsystem.ProjectionPair.lowerSet {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (y : E.Element) : Set D.Element

The set {x ∈ |𝒟| ∣ g(x) ⊑ y} of the first formula. By the Galois connection it is the down-set {x ∣ x ⊑ h(y)} of h(y).

Equations

• P.lowerSet y = {x : D.Element | P.inj.toElementMap x ≤ y}

@[simp]

theorem Domain.Neighborhood.Subsystem.ProjectionPair.mem_lowerSet {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) {y : E.Element} {x : D.Element} : x ∈ P.lowerSet y ↔ P.inj.toElementMap x ≤ y

theorem Domain.Neighborhood.Subsystem.ProjectionPair.lowerSet_bounded {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (y : E.Element) : D.Bounded (P.lowerSet y)

The set {x ∣ g(x) ⊑ y} is bounded: h(y) is an upper bound (it is in fact the top).

theorem Domain.Neighborhood.Subsystem.ProjectionPair.lowerSet_directed {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (y : E.Element) (a : D.Element) : a ∈ P.lowerSet y → ∀ b ∈ P.lowerSet y, ∃ c ∈ P.lowerSet y, a ≤ c ∧ b ≤ c

Exercise 6.25 — "check that the set on the right is directed". Any two members of {x ∣ g(x) ⊑ y} have a common upper bound inside the set, namely h(y) itself (the down-set of h(y) has h(y) as a top, so it is trivially directed).

theorem Domain.Neighborhood.Subsystem.ProjectionPair.proj_eq_sSup {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (y : E.Element) : P.proj.toElementMap y = D.sSup (P.lowerSet y) ⋯

Exercise 6.25, first extremal formula. h(y) = ⊔ {x ∈ |𝒟| ∣ g(x) ⊑ y}.

h(y) is the greatest member of the set (g(h(y)) ⊑ y, so h(y) is in it; every member is ⊑ h(y) by the Galois connection), hence it is the least upper bound.

Second extremal formula: g(x) = ⊓ {y ∣ x ⊑ h(y)}.

def Domain.Neighborhood.Subsystem.ProjectionPair.upperSet {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (x : D.Element) : Set E.Element

The set {y ∈ |ℰ| ∣ x ⊑ h(y)} of the second formula. By the Galois connection it is the up-set {y ∣ g(x) ⊑ y} of g(x).

Equations

• P.upperSet x = {y : E.Element | x ≤ P.proj.toElementMap y}

@[simp]

theorem Domain.Neighborhood.Subsystem.ProjectionPair.mem_upperSet {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) {x : D.Element} {y : E.Element} : y ∈ P.upperSet x ↔ x ≤ P.proj.toElementMap y

theorem Domain.Neighborhood.Subsystem.ProjectionPair.upperSet_nonempty {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (x : D.Element) : (P.upperSet x).Nonempty

Exercise 6.25 — "check that the set on the right is non-empty". g(x) itself lies in {y ∣ x ⊑ h(y)}, since x ⊑ h(g(x)) = x.

theorem Domain.Neighborhood.Subsystem.ProjectionPair.inj_eq_sInf {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) (x : D.Element) : P.inj.toElementMap x = E.sInf (P.upperSet x) ⋯

Exercise 6.25, second extremal formula. g(x) = ⊓ {y ∈ |ℰ| ∣ x ⊑ h(y)}.

g(x) is the least member of the set (x ⊑ h(g(x)) = x, so g(x) is in it; every member is ⊒ g(x) by the Galois connection), hence it is the greatest lower bound.

g preserves consistency and all least upper bounds.

theorem Domain.Neighborhood.Subsystem.ProjectionPair.inj_bounded {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) {S : Set D.Element} (hS : D.Bounded S) : E.Bounded (P.inj.toElementMap '' S)

Exercise 6.25 — g maps consistent sets to consistent sets. "Consistent" for sets of elements is "bounded" (Exercise 1.27). If S is bounded by b, its image {g(s) ∣ s ∈ S} is bounded by g(b) (monotonicity).

theorem Domain.Neighborhood.Subsystem.ProjectionPair.inj_sSup {α : Type u_1} {D E : NeighborhoodSystem α} (P : ProjectionPair D E) {S : Set D.Element} (hS : D.Bounded S) : P.inj.toElementMap (D.sSup S hS) = E.sSup (P.inj.toElementMap '' S) ⋯

Exercise 6.25 — g preserves ⊔ (not just directed unions). For any bounded set S, g(⊔S) = ⊔ {g(s) ∣ s ∈ S}. This is the characteristic property of a lower adjoint.

• ⊒: g(⊔S) is an upper bound of {g(s)} since s ⊑ ⊔S and g is monotone.
• ⊑: by the Galois connection it suffices that ⊔S ⊑ h(⊔{g(s)}), i.e. that each s ⊑ h(⊔{g(s)}); by the Galois connection again this is g(s) ⊑ ⊔{g(s)}, true by le_sSup.