Lecture VI — Proposition 6.12 (Scott 1981, PRG-19): a subdomain yields a

projection pair

Proposition 6.12. If D ◁ E, then there exists a projection pair of approximable mappings

i : D → E and j : E → D

with j ∘ i = I_D and i ∘ j ⊆ I_E, determined as element-wise functions by

i(x) = {Y ∈ E ∣ ∃ X ∈ x, X ⊆ Y} and j(y) = y ∩ D.

Scott leaves the proof "for the exercises". We give it directly at the level of the neighbourhood relations (Definition 2.1), which keeps everything choice-free.

• The injection i (Subsystem.inj) is the relation X i Y ↔ X ∈ D ∧ Y ∈ E ∧ X ⊆ Y — it sends a D-neighbourhood to all the E-neighbourhoods it refines.
• The projection j (Subsystem.proj) is the relation Y j X ↔ Y ∈ E ∧ X ∈ D ∧ Y ⊆ X — it intersects an E-element with D.

The two laws are then short relational calculations:

• Subsystem.proj_comp_inj : j ∘ i = I_D. Both round trips factor as X ⊆ Y ⊆ Z, giving exactly the identity relation X ⊆ Z on D. (Proved with the choice-free relational extensionality ApproximableMap.ext.)
• Subsystem.inj_comp_proj_le : i ∘ j ⊆ I_E. A round trip Y ⊆ X ⊆ Y' through a common D-neighbourhood X is in particular Y ⊆ Y' on E — but not conversely, so this direction is only an inclusion. The crucial clause of D ◁ E (consistency inherited from E) is what makes j's output-intersection law hold (inter_right).

The element-wise descriptions Scott records are Subsystem.toElementMap_inj and Subsystem.toElementMap_proj.

Everything here is choice-free (#print axioms ⊆ {propext, Quot.sound}).

def Domain.Neighborhood.Subsystem.inj {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) : ApproximableMap D E

The injection i : D → E of Proposition 6.12. As a neighbourhood relation, X i Y ↔ X ∈ D ∧ Y ∈ E ∧ X ⊆ Y. Element-wise (see toElementMap_inj) it is Scott's i(x) = {Y ∈ E ∣ ∃ X ∈ x, X ⊆ Y}.

Equations

• h.inj = { rel := fun (X Y : Set α) => D.mem X ∧ E.mem Y ∧ X ⊆ Y, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

@[simp]

theorem Domain.Neighborhood.Subsystem.inj_rel {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) {X Y : Set α} : h.inj.rel X Y ↔ D.mem X ∧ E.mem Y ∧ X ⊆ Y

def Domain.Neighborhood.Subsystem.proj {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) : ApproximableMap E D

The projection j : E → D of Proposition 6.12. As a neighbourhood relation, Y j X ↔ Y ∈ E ∧ X ∈ D ∧ Y ⊆ X. Element-wise (see toElementMap_proj) it is Scott's j(y) = y ∩ D. The inter_right law is exactly where Definition 6.10's consistency clause (inter_closed) is used.

Equations

• h.proj = { rel := fun (Y X : Set α) => E.mem Y ∧ D.mem X ∧ Y ⊆ X, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

@[simp]

theorem Domain.Neighborhood.Subsystem.proj_rel {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) {Y X : Set α} : h.proj.rel Y X ↔ E.mem Y ∧ D.mem X ∧ Y ⊆ X

theorem Domain.Neighborhood.Subsystem.toElementMap_inj {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) (x : D.Element) {Y : Set α} : (h.inj.toElementMap x).mem Y ↔ E.mem Y ∧ ∃ (X : Set α), x.mem X ∧ X ⊆ Y

Element-wise description of i (Scott's equation). i(x) = {Y ∈ E ∣ ∃ X ∈ x, X ⊆ Y}.

theorem Domain.Neighborhood.Subsystem.toElementMap_proj {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) (y : E.Element) {X : Set α} : (h.proj.toElementMap y).mem X ↔ y.mem X ∧ D.mem X

Element-wise description of j (Scott's equation). j(y) = y ∩ D: the neighbourhoods of j(y) are exactly the D-neighbourhoods that already belong to y.

theorem Domain.Neighborhood.Subsystem.proj_comp_inj {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) : h.proj.comp h.inj = ApproximableMap.idMap D

Proposition 6.12, first law: j ∘ i = I_D. Each side relates X and Z exactly when X, Z ∈ D and X ⊆ Z: a round trip X ⊆ Y ⊆ Z through an E-neighbourhood Y collapses to X ⊆ Z (forward), and X ⊆ Z factors through Y = Z (backward). Proved relationally, so choice-free.

theorem Domain.Neighborhood.Subsystem.inj_comp_proj_le {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) : h.inj.comp h.proj ≤ ApproximableMap.idMap E

Proposition 6.12, second law: i ∘ j ⊆ I_E. A round trip Y ⊆ X ⊆ Y' through a common D-neighbourhood X is in particular Y ⊆ Y' on E. The reverse inclusion fails (not every consistent E-pair factors through D), so this is an inclusion of relations, not an equality.

structure Domain.Neighborhood.Subsystem.ProjectionPair {α : Type u_1} (D E : NeighborhoodSystem α) : Type u_1

A projection pair (Definition 6.13 vocabulary). Bundles Scott's i, j together with the two laws, ready for reuse in monotone/continuous-on-domains functors and the existence Theorem 6.14.

• inj : ApproximableMap D E

  The injection i : D → E.

• proj : ApproximableMap E D

  The projection j : E → D.

• proj_comp_inj : self.proj.comp self.inj = ApproximableMap.idMap D

  j ∘ i = I_D.

• inj_comp_proj_le : self.inj.comp self.proj ≤ ApproximableMap.idMap E

  i ∘ j ⊆ I_E.

def Domain.Neighborhood.Subsystem.projectionPair {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) : ProjectionPair D E

Proposition 6.12 (Scott 1981, PRG-19). Every subdomain relation D ◁ E gives rise to a projection pair i : D → E, j : E → D with j ∘ i = I_D and i ∘ j ⊆ I_E.

Equations

• h.projectionPair = { inj := h.inj, proj := h.proj, proj_comp_inj := ⋯, inj_comp_proj_le := ⋯ }