Lecture VI — Proposition 6.11 (Scott 1981, PRG-19): the subsystems of E form a

domain

Proposition 6.11. For a given neighbourhood system E, the set of subsystems

{D ∣ D ◁ E}

forms a domain in its own right.

Scott derives this as a one-line corollary of the remark preceding it: the union of a directed family of subdomains of E is again a subdomain. We make this precise using the project's abstract representation theorem (Exercise 2.22, Exercise222.reprIso): a family C of sets that is closed under (i) non-empty intersection and (ii) directed union is order-isomorphic to a domain |reprSystem C| — exactly the route used for "the open sets form a domain" (Exercise 3.25) and "the function space is a domain" (Exercise 3.27).

The faithful translation runs as follows. A subsystem D ◁ E is, by NeighborhoodSystem.ext and the standing D.master = E.master, completely determined by its family of neighbourhoods {X ∣ D.mem X}. So we represent the poset ({D ∣ D ◁ E}, ◁) by the family

subFam E = { {X ∣ D.mem X} ∣ D ◁ E } ⊆ 𝒫(𝒫(Δ)),

ordered by ⊆. By Scott's remark (Subsystem.subsystem_iff_subset_of_common) the subdomain relation ◁ between two subsystems of E is just inclusion of their neighbourhood families, so ({D ∣ D ◁ E}, ◁) ≃o (subFam E, ⊆) (subIso). The two closure properties hold:

• non-empty intersections (subFam_sInter_mem): the intersection of a non-empty family of subdomains is the subdomain interSys whose neighbourhoods are the common neighbourhoods;
• directed unions (subFam_sUnion_mem): the union of a directed family of subdomains is the subdomain unionSys (Scott's remark) — directedness is used exactly to verify closure under consistent intersection.

The capstone subsystemReprIso : {D ∣ D ◁ E} ≃o |reprSystem (subFam E) …| composes subIso with Exercise222.reprIso, witnessing that the subsystems of E are (isomorphic to) a domain.

Axioms. The combinatorial heart — subFam and its closure under intersection/union, the subsystem constructions interSys/unionSys, and subIso — is choice-free (#print axioms ⊆ {propext, Quot.sound}). The final subsystemReprIso inherits Classical.choice solely through Exercise 2.22's representation isomorphism (the "for set theorists" exercise, which picks witnesses of non-emptiness and uses finite-set induction), exactly as Exercise 3.27 does.

The representing family of neighbourhood-sets.

def Domain.Neighborhood.Proposition611.subFam {α : Type u_1} (E : NeighborhoodSystem α) : Set (Set (Set α))

The family of neighbourhood-sets of subdomains of E: a set of subsets of Δ lies in subFam E exactly when it is {X ∣ D.mem X} for some subsystem D ◁ E. This is the concrete family of sets that, by Exercise 2.22, represents {D ∣ D ◁ E} as a domain.

Equations

• Domain.Neighborhood.Proposition611.subFam E = {𝒮 : Set (Set α) | ∃ (D : Domain.Neighborhood.NeighborhoodSystem α), D ◁ E ∧ 𝒮 = {X : Set α | D.mem X}}

theorem Domain.Neighborhood.Proposition611.subFam_master_mem {α : Type u_1} (E : NeighborhoodSystem α) {𝒮 : Set (Set α)} (h : 𝒮 ∈ subFam E) : E.master ∈ 𝒮

The master Δ = E.master belongs to the neighbourhood-set of any subdomain (a subsystem shares E's master and contains it).

theorem Domain.Neighborhood.Proposition611.subFam_mem_E {α : Type u_1} (E : NeighborhoodSystem α) {𝒮 : Set (Set α)} {X : Set α} (h : 𝒮 ∈ subFam E) (hX : X ∈ 𝒮) : E.mem X

Every member of a subdomain's neighbourhood-set is an E-neighbourhood (D ⊆ E).

theorem Domain.Neighborhood.Proposition611.subFam_inter_closed {α : Type u_1} (E : NeighborhoodSystem α) {𝒮 : Set (Set α)} {X Y : Set α} (h : 𝒮 ∈ subFam E) (hX : X ∈ 𝒮) (hY : Y ∈ 𝒮) (hXY : E.mem (X ∩ Y)) : X ∩ Y ∈ 𝒮

Consistency is inherited from E (Definition 6.10's essential clause): if X, Y lie in a subdomain's neighbourhood-set and X ∩ Y ∈ E, then X ∩ Y lies in it too.

theorem Domain.Neighborhood.Proposition611.subFam_nonempty {α : Type u_1} (E : NeighborhoodSystem α) : (subFam E).Nonempty

subFam E is non-empty: E itself is a subsystem (Subsystem.refl), so its own neighbourhood-set {X ∣ E.mem X} is a member.

Closure under non-empty intersection.

def Domain.Neighborhood.Proposition611.interSys {α : Type u_1} (E : NeighborhoodSystem α) (ℱ : Set (Set (Set α))) (hne : ℱ.Nonempty) (hℱ : ℱ ⊆ subFam E) : NeighborhoodSystem α

The intersection subdomain of a non-empty family ℱ of subdomain neighbourhood-sets: its neighbourhoods are the sets common to every member of ℱ.

Equations

• Domain.Neighborhood.Proposition611.interSys E ℱ hne hℱ = { mem := fun (X : Set α) => ∀ 𝒮 ∈ ℱ, X ∈ 𝒮, master := E.master, master_mem := ⋯, inter_mem := ⋯, sub_master := ⋯ }

theorem Domain.Neighborhood.Proposition611.interSys_subsystem {α : Type u_1} (E : NeighborhoodSystem α) (ℱ : Set (Set (Set α))) (hne : ℱ.Nonempty) (hℱ : ℱ ⊆ subFam E) : interSys E ℱ hne hℱ ◁ E

The intersection subdomain is a subsystem of E.

theorem Domain.Neighborhood.Proposition611.interSys_nbset {α : Type u_1} (E : NeighborhoodSystem α) (ℱ : Set (Set (Set α))) (hne : ℱ.Nonempty) (hℱ : ℱ ⊆ subFam E) : {X : Set α | (interSys E ℱ hne hℱ).mem X} = ⋂₀ ℱ

The neighbourhood-set of the intersection subdomain is exactly ⋂₀ ℱ.

theorem Domain.Neighborhood.Proposition611.subFam_sInter_mem {α : Type u_1} (E : NeighborhoodSystem α) (ℱ : Set (Set (Set α))) (hne : ℱ.Nonempty) (hℱ : ℱ ⊆ subFam E) : ⋂₀ ℱ ∈ subFam E

Closure under non-empty intersection (Exercise 2.22's hypothesis (i)).

Closure under directed union (Scott's remark).

def Domain.Neighborhood.Proposition611.unionSys {α : Type u_1} (E : NeighborhoodSystem α) (ℱ : Set (Set (Set α))) (hne : ℱ.Nonempty) (hℱ : ℱ ⊆ subFam E) (hdir : DirectedOn (fun (x1 x2 : Set (Set α)) => x1 ⊆ x2) ℱ) : NeighborhoodSystem α

The union subdomain of a directed family ℱ of subdomain neighbourhood-sets: its neighbourhoods are those lying in some member of ℱ. Directedness is what makes this closed under consistent intersection.

Equations

• Domain.Neighborhood.Proposition611.unionSys E ℱ hne hℱ hdir = { mem := fun (X : Set α) => ∃ 𝒮 ∈ ℱ, X ∈ 𝒮, master := E.master, master_mem := ⋯, inter_mem := ⋯, sub_master := ⋯ }

theorem Domain.Neighborhood.Proposition611.unionSys_subsystem {α : Type u_1} (E : NeighborhoodSystem α) (ℱ : Set (Set (Set α))) (hne : ℱ.Nonempty) (hℱ : ℱ ⊆ subFam E) (hdir : DirectedOn (fun (x1 x2 : Set (Set α)) => x1 ⊆ x2) ℱ) : unionSys E ℱ hne hℱ hdir ◁ E

The union subdomain is a subsystem of E (Scott's remark: the directed union of subdomains is again a subdomain).

theorem Domain.Neighborhood.Proposition611.unionSys_nbset {α : Type u_1} (E : NeighborhoodSystem α) (ℱ : Set (Set (Set α))) (hne : ℱ.Nonempty) (hℱ : ℱ ⊆ subFam E) (hdir : DirectedOn (fun (x1 x2 : Set (Set α)) => x1 ⊆ x2) ℱ) : {X : Set α | (unionSys E ℱ hne hℱ hdir).mem X} = ⋃₀ ℱ

The neighbourhood-set of the union subdomain is exactly ⋃₀ ℱ.

theorem Domain.Neighborhood.Proposition611.subFam_sUnion_mem {α : Type u_1} (E : NeighborhoodSystem α) (ℱ : Set (Set (Set α))) (hne : ℱ.Nonempty) (hℱ : ℱ ⊆ subFam E) (hdir : DirectedOn (fun (x1 x2 : Set (Set α)) => x1 ⊆ x2) ℱ) : ⋃₀ ℱ ∈ subFam E

Closure under directed union (Exercise 2.22's hypothesis (ii)) — Scott's remark.

The poset of subsystems and its representation.

@[implicit_reducible]

instance Domain.Neighborhood.Proposition611.subPartialOrder {α : Type u_1} (E : NeighborhoodSystem α) : PartialOrder { D : NeighborhoodSystem α // D ◁ E }

The subsystems of E, ordered by the subdomain relation ◁, form a partial order (reflexive, transitive, antisymmetric — Definition 6.10's API).

Equations

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

def Domain.Neighborhood.Proposition611.ofMem {α : Type u_1} (E : NeighborhoodSystem α) (𝒮 : Set (Set α)) (h : 𝒮 ∈ subFam E) : NeighborhoodSystem α

Rebuild a subsystem of E from its neighbourhood-set 𝒮 ∈ subFam E. The data (the mem predicate · ∈ 𝒮 and the master E.master) depends only on 𝒮; the proof obligations are discharged from subFam membership.

Equations

• Domain.Neighborhood.Proposition611.ofMem E 𝒮 h = { mem := fun (X : Set α) => X ∈ 𝒮, master := E.master, master_mem := ⋯, inter_mem := ⋯, sub_master := ⋯ }

theorem Domain.Neighborhood.Proposition611.ofMem_subsystem {α : Type u_1} (E : NeighborhoodSystem α) (𝒮 : Set (Set α)) (h : 𝒮 ∈ subFam E) : ofMem E 𝒮 h ◁ E

ofMem lands in the subsystems of E.

def Domain.Neighborhood.Proposition611.subIso {α : Type u_1} (E : NeighborhoodSystem α) : { D : NeighborhoodSystem α // D ◁ E } ≃o { 𝒮 : Set (Set α) // 𝒮 ∈ subFam E }

The poset of subsystems is the family subFam E. The subsystems of E, ordered by ◁, are order-isomorphic to subFam E ordered by ⊆. A subsystem is sent to its family of neighbourhoods {X ∣ D.mem X}, and recovered by ofMem; order is preserved and reflected by Scott's remark Subsystem.subsystem_iff_subset_of_common.

Equations

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

def Domain.Neighborhood.Proposition611.subsystemReprIso {α : Type u_1} (E : NeighborhoodSystem α) : { D : NeighborhoodSystem α // D ◁ E } ≃o (Exercise222.reprSystem (subFam E) ⋯ ⋯).Element

Proposition 6.11 (Scott 1981, PRG-19). For a neighbourhood system E, the set of subsystems {D ∣ D ◁ E}, ordered by the subdomain relation ◁, forms a domain in its own right: it is order-isomorphic to the domain |reprSystem (subFam E) …| produced by the abstract representation theorem (Exercise 2.22), using that subFam E is closed under non-empty intersections (subFam_sInter_mem) and directed unions (Scott's remark, subFam_sUnion_mem).

Equations

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