Lecture VI — Lemma 6.15 (Scott 1981, PRG-19): the converse of Proposition 6.12

Proposition 6.12 says a subdomain relation D ◁ E yields a projection pair i : D → E, j : E → D with j ∘ i = I_D and i ∘ j ⊆ I_E. Lemma 6.15 is the converse: any projection pair — between two neighbourhood systems D and E over possibly different token types — exhibits D as (isomorphic to) a subdomain of E. Scott writes D ⊴ E as short for "D ≅ D' for some D' ◁ E."

Lemma 6.15. If there exist approximable maps i : D → E and j : E → D with j ∘ i = I_D and i ∘ j ⊆ I_E, then D ⊴ E.

The construction (cleaner than Scott's, fully relational)

Scott's proof works with the ideal elements (filters) and shows that i carries finite (principal) elements to finite elements. We avoid the filter-by-filter argument by isolating one relational predicate:

IsGen i j X Y := X i Y ∧ Y j X ("Y generates i(↑X)").

Everything follows from three relational facts:

• isGen_exists (uses j ∘ i = I_D): every X ∈ D has a generator Y (apply j∘i = I to the identity relation X I_D X).
• isGen_mono (uses j ∘ i = I_D) and isGen_mono' (uses i ∘ j ⊆ I_E): the generator correspondence is inclusion-monotone in both directions — Y ⊆ Y' ↔ X ⊆ X'. Their two-way use gives that generators are unique in each argument (isGen_fst_unique/isGen_snd_unique).
• isGen_inter (just mono/inter_right of i, j): if Y, Y' are generators and Y ∩ Y' ∈ E, then Y ∩ Y' generates X ∩ X'.

The image system Dprime i j has Y as a neighbourhood iff Y generates some X ∈ D; its master is E's master. isGen_inter makes it a neighbourhood system and gives the crucial inter_closed clause of ◁ (consistency inherited from E), so Dprime i j ◁ E. The order-isomorphism D ≅ Dprime i j is x ↦ {Y ∣ ∃ X ∈ x, IsGen i j X Y} with inverse y ↦ {X ∣ ∃ Y ∈ y, IsGen i j X Y}, the inverse laws and order-reflection coming from generator uniqueness.

Everything is built at the level of Definition 2.1 relations, so the whole development is choice-free (#print axioms ⊆ {propext, Quot.sound}).

def Domain.Neighborhood.Trianglelefteq {α : Type u_1} {β : Type u_2} (D : NeighborhoodSystem α) (E : NeighborhoodSystem β) : Prop

Scott's ⊴ (the prose before Lemma 6.15). D ⊴ E means D ≅ D' for some subdomain D' ◁ E: D embeds as a subdomain of E.

Equations

• (D ⊴ E) = ∃ (D' : Domain.Neighborhood.NeighborhoodSystem β), D' ◁ E ∧ (D ≅ᴰ D')

def Domain.Neighborhood.«term_⊴_» : Lean.TrailingParserDescr

Scott's ⊴ (the prose before Lemma 6.15). D ⊴ E means D ≅ D' for some subdomain D' ◁ E: D embeds as a subdomain of E.

Equations

• One or more equations did not get rendered due to their size.

def Domain.Neighborhood.IsGen {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (X : Set α) (Y : Set β) : Prop

The generator predicate: Y generates i(↑X). Relationally, X i Y and Y j X.

Equations

• Domain.Neighborhood.IsGen i j X Y = (i.rel X Y ∧ j.rel Y X)

theorem Domain.Neighborhood.isGen_master {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) : IsGen i j D.master E.master

The masters generate each other: IsGen Δ_D Δ_E (from i.master_rel, j.master_rel).

theorem Domain.Neighborhood.isGen_exists {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hji : j.comp i = ApproximableMap.idMap D) {X : Set α} (hX : D.mem X) : ∃ (Y : Set β), IsGen i j X Y

Generators exist (uses j ∘ i = I_D). Every D-neighbourhood X has a generator: apply j ∘ i = I_D to the identity relation X I_D X.

theorem Domain.Neighborhood.isGen_mono {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hji : j.comp i = ApproximableMap.idMap D) {X X' : Set α} {Z W : Set β} (h : IsGen i j X Z) (h' : IsGen i j X' W) (hZW : Z ⊆ W) : X ⊆ X'

The generator correspondence is monotone (uses j ∘ i = I_D): if Y, Y' generate X, X' and Y ⊆ Y', then X ⊆ X'. (Widen X i Y to X i Y' by mono, compose with Y' j X', and read off X ⊆ X' from j ∘ i = I_D.)

theorem Domain.Neighborhood.isGen_mono' {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hij : i.comp j ≤ ApproximableMap.idMap E) {X X' : Set α} {Z W : Set β} (h : IsGen i j X Z) (h' : IsGen i j X' W) (hXX' : X ⊆ X') : Z ⊆ W

The generator correspondence is monotone, other direction (uses i ∘ j ⊆ I_E): if Z, W generate X, X' and X ⊆ X', then Z ⊆ W. (Widen Z j X to Z j X' by mono, compose with X' i W, and read off Z ⊆ W from i ∘ j ⊆ I_E.)

theorem Domain.Neighborhood.isGen_fst_unique {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hji : j.comp i = ApproximableMap.idMap D) {X X' : Set α} {Y : Set β} (h : IsGen i j X Y) (h' : IsGen i j X' Y) : X = X'

Generators are unique in the first argument (isGen_mono both ways).

theorem Domain.Neighborhood.isGen_snd_unique {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hij : i.comp j ≤ ApproximableMap.idMap E) {X : Set α} {Y Y' : Set β} (h : IsGen i j X Y) (h' : IsGen i j X Y') : Y = Y'

Generators are unique in the second argument (isGen_mono' both ways).

theorem Domain.Neighborhood.isGen_inter {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) {X X' : Set α} {Y Y' : Set β} (h : IsGen i j X Y) (h' : IsGen i j X' Y') (hE : E.mem (Y ∩ Y')) : IsGen i j (X ∩ X') (Y ∩ Y')

Generators are closed under intersection. If Y, Y' generate X, X' and Y ∩ Y' ∈ E, then Y ∩ Y' generates X ∩ X'. Needs only mono/inter_right of i and j (the hypothesis E.mem (Y ∩ Y') is what licenses the j.mono steps).

def Domain.Neighborhood.Dprime {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) : NeighborhoodSystem β

The image subdomain D'. A β-set Y is a neighbourhood iff it generates some D-neighbourhood; the master is E's master. isGen_inter supplies condition (ii).

Equations

• Domain.Neighborhood.Dprime i j = { mem := fun (Y : Set β) => ∃ (X : Set α), Domain.Neighborhood.IsGen i j X Y, master := E.master, master_mem := ⋯, inter_mem := ⋯, sub_master := ⋯ }

@[simp]

theorem Domain.Neighborhood.mem_Dprime {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) {Y : Set β} : (Dprime i j).mem Y ↔ ∃ (X : Set α), IsGen i j X Y

theorem Domain.Neighborhood.Dprime_subsystem {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) : Dprime i j ◁ E

D' ◁ E. Same master (rfl); D' ⊆ E since a generator's Y is an E-neighbourhood; and the consistency clause inter_closed is exactly isGen_inter.

def Domain.Neighborhood.toEl {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hji : j.comp i = ApproximableMap.idMap D) (x : D.Element) : (Dprime i j).Element

Forward map of the isomorphism D ≅ D'. x ↦ {Y ∣ ∃ X ∈ x, IsGen i j X Y} — the generators of the members of x. (Needs j ∘ i = I_D for upward closure, via isGen_mono.)

Equations

• Domain.Neighborhood.toEl i j hji x = { mem := fun (Y : Set β) => ∃ (X : Set α), x.mem X ∧ Domain.Neighborhood.IsGen i j X Y, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

def Domain.Neighborhood.ofEl {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hji : j.comp i = ApproximableMap.idMap D) (hij : i.comp j ≤ ApproximableMap.idMap E) (y : (Dprime i j).Element) : D.Element

Inverse map of the isomorphism D ≅ D'. y ↦ {X ∣ ∃ Y ∈ y, IsGen i j X Y}. (Needs both laws: j ∘ i = I_D for generator existence and i ∘ j ⊆ I_E for isGen_mono'.)

Equations

• Domain.Neighborhood.ofEl i j hji hij y = { mem := fun (X : Set α) => ∃ (Y : Set β), y.mem Y ∧ Domain.Neighborhood.IsGen i j X Y, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

def Domain.Neighborhood.dprimeEquiv {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hji : j.comp i = ApproximableMap.idMap D) (hij : i.comp j ≤ ApproximableMap.idMap E) : D.Element ≃o (Dprime i j).Element

The domain isomorphism D ≅ D' (Scott's "inclusion-preserving one-one correspondence"). Built from toEl/ofEl; the inverse laws and order-reflection come from generator uniqueness.

Equations

• Domain.Neighborhood.dprimeEquiv i j hji hij = { toFun := Domain.Neighborhood.toEl i j hji, invFun := Domain.Neighborhood.ofEl i j hji hij, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem Domain.Neighborhood.trianglelefteq_of_projectionPair {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hji : j.comp i = ApproximableMap.idMap D) (hij : i.comp j ≤ ApproximableMap.idMap E) : D ⊴ E

Lemma 6.15 (Scott 1981, PRG-19). A projection pair i : D → E, j : E → D with j ∘ i = I_D and i ∘ j ⊆ I_E exhibits D as a subdomain of E: D ⊴ E. This is the converse of Proposition 6.12 (Subsystem.projectionPair).

theorem Domain.Neighborhood.Subsystem.trianglelefteq {α : Type u_1} {D E : NeighborhoodSystem α} (h : D ◁ E) : D ⊴ E

Proposition 6.12 + Lemma 6.15 packaged. A subdomain relation D ◁ E is in particular a witness of D ⊴ E (take D' = D). Together with trianglelefteq_of_projectionPair, this shows D ⊴ E holds iff there is a projection pair D ⇄ E.