Exercise 3.25 (Scott 1981, PRG-19, §3) — the open sets of |𝒟| form a domain

(For topologists.) Exercises 1.21/1.22 and 2.13 regard a domain |𝒟| as a topological space (the basic opens [X] = {x ∣ X ∈ x}, basicOpen) on which the approximable maps are exactly the continuous functions. Scott asks, "using 3.10", to show that the family of open subsets of |𝒟| is isomorphic to a domain.

The route is the standard "open sets = maps to Sierpiński space". Let 𝒪 be the Sierpiński domain (sierpinski): the two-token-state system whose neighbourhoods are Δ = univ and ∅, so |𝒪| is the two-element domain ⊥ ⊏ ⊤. The correspondence

• mapOfOpen U : 𝒟 → 𝒪, relating X to ∅ (the "defined"/top neighbourhood of 𝒪) exactly when [X] ⊆ U, and to univ always;
• openOfMap f = {x ∣ f(x) = ⊤} = ⋃ {[X] ∣ X f ∅};

are mutually inverse and inclusion-preserving (openIso), so by Theorem 3.10 (funSpaceEquiv, |𝒟 → 𝒪| ≃ ApproximableMap) the lattice of open sets is order-isomorphic to the domain |𝒟 → 𝒪| (opensReprIso). The one place topology (openness of U) is used is the round trip openOfMap (mapOfOpen U) = U and the ← half of order reflection: an open set is recovered from its basic neighbourhoods.

def Domain.Neighborhood.Exercise325.sierpinski : NeighborhoodSystem Unit

The Sierpiński domain 𝒪: the system over a one-token type whose neighbourhoods are Δ (univ) and ∅. Its elements are ⊥ (only Δ) and ⊤ (also ∅), i.e. the two-point domain.

Equations

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

From an open set to an approximable map 𝒟 → 𝒪.

def Domain.Neighborhood.Exercise325.mapOfOpen {α : Type u_1} (V : NeighborhoodSystem α) (U : Set V.Element) : ApproximableMap V sierpinski

mapOfOpen U : 𝒟 → 𝒪. It always relates X to the blunt neighbourhood univ of 𝒪, and relates X to the sharp neighbourhood ∅ exactly when the basic open [X] lies inside U. As an elementwise map it sends x to ⊤ iff x ∈ U.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise325.mapOfOpen_rel {α : Type u_1} (V : NeighborhoodSystem α) (U : Set V.Element) (X : Set α) (Y : Set Unit) : (mapOfOpen V U).rel X Y ↔ V.mem X ∧ (Y = Set.univ ∨ Y = ∅ ∧ V.basicOpen X ⊆ U)

theorem Domain.Neighborhood.Exercise325.mapOfOpen_rel_empty {α : Type u_1} (V : NeighborhoodSystem α) (U : Set V.Element) (X : Set α) : (mapOfOpen V U).rel X ∅ ↔ V.mem X ∧ V.basicOpen X ⊆ U

The decisive special case: X (mapOfOpen U) ∅ ↔ [X] ⊆ U (for a neighbourhood X).

From an approximable map 𝒟 → 𝒪 to an open set.

def Domain.Neighborhood.Exercise325.openOfMap {α : Type u_1} (V : NeighborhoodSystem α) (f : ApproximableMap V sierpinski) : Set V.Element

openOfMap f = {x ∣ f(x) = ⊤} = ⋃ {[X] ∣ X f ∅}: the points sent by f to the top of 𝒪.

Equations

• Domain.Neighborhood.Exercise325.openOfMap V f = {x : V.Element | ∃ (X : Set α), x.mem X ∧ f.rel X ∅}

theorem Domain.Neighborhood.Exercise325.openOfMap_isOpen {α : Type u_1} (V : NeighborhoodSystem α) (f : ApproximableMap V sierpinski) : IsOpen (openOfMap V f)

openOfMap f is open: it is a union of basic opens [X].

The order-isomorphism Opens(|𝒟|) ≃o (𝒟 → 𝒪).

def Domain.Neighborhood.Exercise325.openIso {α : Type u_1} (V : NeighborhoodSystem α) : { U : Set V.Element // IsOpen U } ≃o ApproximableMap V sierpinski

Exercise 3.25 (core). The open subsets of |𝒟| (ordered by ⊆) are order-isomorphic to the approximable maps 𝒟 → 𝒪.

Equations

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

def Domain.Neighborhood.Exercise325.opensReprIso {α : Type u_1} (V : NeighborhoodSystem α) : { U : Set V.Element // IsOpen U } ≃o (funSpace V sierpinski).Element

Exercise 3.25. The family of open subsets of |𝒟|, ordered by inclusion, is order-isomorphic to the domain |𝒟 → 𝒪| of the Sierpiński function space — hence is (isomorphic to) a domain. This uses Theorem 3.10 (funSpaceEquiv) exactly as Scott directs.

Equations

• Domain.Neighborhood.Exercise325.opensReprIso V = (Domain.Neighborhood.Exercise325.openIso V).trans (Domain.Neighborhood.funSpaceEquiv V Domain.Neighborhood.Exercise325.sierpinski).symm