Exercise 3.27 (Scott 1981, PRG-19, §3) — (𝒟₀ → 𝒟₁) is a domain, via Exercise

2.22

(For set theorists.) Scott asks for another proof that the family of approximable mappings f : 𝒟₀ → 𝒟₁ is isomorphic to a domain, "by employing the general argument of Exercise 2.22" (the abstract representation theorem: any family of sets closed under non-empty intersections and directed unions is inclusion-isomorphic to a domain).

The set-theoretic content: identify each approximable map f with its graph graph f = {(X, Y) ∣ X f Y} ⊆ 𝒫(Δ₀) × 𝒫(Δ₁), and let C = {graph f} be the family of all such graphs. Then

• C is closed under non-empty intersections — the pointwise meet ⋀ 𝒮 of a family of approximable maps (relate X to Y iff every member does) is again approximable (meetMap);
• C is closed under directed unions — the join ⋁ 𝒮 of a directed family (relate X to Y iff some member does) is again approximable, the consistency condition using directedness (joinMap).

So Exercise 2.22 (reprIso) re-presents C — hence, via graph and Theorem 3.10 (funSpaceEquiv), the whole function space |𝒟₀ → 𝒟₁| — as the domain of a neighbourhood system, without writing down the step-set neighbourhoods of Definition 3.8 explicitly. This is exactly Scott's "compare with 3.9/3.10" alternative.

Axioms. As flagged by Scott ("for set theorists"), this inherits Classical.choice from Exercise 2.22 and from the graph-inversion.

def Domain.Neighborhood.Exercise327.graph {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) : Set (Set α × Set β)

The graph of an approximable map, as a set of neighbourhood pairs.

Equations

• Domain.Neighborhood.Exercise327.graph f = {p : Set α × Set β | f.rel p.1 p.2}

@[simp]

theorem Domain.Neighborhood.Exercise327.mem_graph {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f : ApproximableMap V₀ V₁} {p : Set α × Set β} : p ∈ graph f ↔ f.rel p.1 p.2

theorem Domain.Neighborhood.Exercise327.graph_injective {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : Function.Injective graph

def Domain.Neighborhood.Exercise327.C {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : Set (Set (Set α × Set β))

Scott's family C: all graphs of approximable maps 𝒟₀ → 𝒟₁.

Equations

• Domain.Neighborhood.Exercise327.C V₀ V₁ = Set.range Domain.Neighborhood.Exercise327.graph

theorem Domain.Neighborhood.Exercise327.C_nonempty {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : (C V₀ V₁).Nonempty

The meet of a non-empty family of maps.

def Domain.Neighborhood.Exercise327.meetMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (𝒮 : Set (Set (Set α × Set β))) (h𝒮 : 𝒮 ⊆ C V₀ V₁) (hne : 𝒮.Nonempty) : ApproximableMap V₀ V₁

The pointwise meet ⋀ 𝒮 of a family of approximable maps (drawn from C): X (⋀𝒮) Y iff (X, Y) lies in every member of 𝒮.

Equations

• Domain.Neighborhood.Exercise327.meetMap 𝒮 h𝒮 hne = { rel := fun (X : Set α) (Y : Set β) => ∀ S ∈ 𝒮, (X, Y) ∈ S, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

theorem Domain.Neighborhood.Exercise327.sInter_eq_graph_meetMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (𝒮 : Set (Set (Set α × Set β))) (h𝒮 : 𝒮 ⊆ C V₀ V₁) (hne : 𝒮.Nonempty) : ⋂₀ 𝒮 = graph (meetMap 𝒮 h𝒮 hne)

theorem Domain.Neighborhood.Exercise327.C_inter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (𝒮 : Set (Set (Set α × Set β))) : 𝒮.Nonempty → 𝒮 ⊆ C V₀ V₁ → ⋂₀ 𝒮 ∈ C V₀ V₁

Exercise 2.22 hypothesis (i). C is closed under non-empty intersections.

The join of a directed family of maps.

def Domain.Neighborhood.Exercise327.joinMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (𝒮 : Set (Set (Set α × Set β))) (h𝒮 : 𝒮 ⊆ C V₀ V₁) (hne : 𝒮.Nonempty) (hdir : DirectedOn (fun (x1 x2 : Set (Set α × Set β)) => x1 ⊆ x2) 𝒮) : ApproximableMap V₀ V₁

The join ⋁ 𝒮 of a directed family of approximable maps: X (⋁𝒮) Y iff (X, Y) lies in some member. Directedness is what restores the intersectivity condition (ii).

Equations

• Domain.Neighborhood.Exercise327.joinMap 𝒮 h𝒮 hne hdir = { rel := fun (X : Set α) (Y : Set β) => ∃ S ∈ 𝒮, (X, Y) ∈ S, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

theorem Domain.Neighborhood.Exercise327.sUnion_eq_graph_joinMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (𝒮 : Set (Set (Set α × Set β))) (h𝒮 : 𝒮 ⊆ C V₀ V₁) (hne : 𝒮.Nonempty) (hdir : DirectedOn (fun (x1 x2 : Set (Set α × Set β)) => x1 ⊆ x2) 𝒮) : ⋃₀ 𝒮 = graph (joinMap 𝒮 h𝒮 hne hdir)

theorem Domain.Neighborhood.Exercise327.C_dir {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (𝒮 : Set (Set (Set α × Set β))) : 𝒮.Nonempty → 𝒮 ⊆ C V₀ V₁ → DirectedOn (fun (x1 x2 : Set (Set α × Set β)) => x1 ⊆ x2) 𝒮 → ⋃₀ 𝒮 ∈ C V₀ V₁

Exercise 2.22 hypothesis (ii). C is closed under directed unions.

C ≅ Hom(𝒟₀, 𝒟₁) ≅ |𝒟₀ → 𝒟₁|.

noncomputable def Domain.Neighborhood.Exercise327.graphEquiv {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : ApproximableMap V₀ V₁ ≃o { X : Set (Set α × Set β) // X ∈ C V₀ V₁ }

graph is an order-isomorphism of approximable maps (under ⊑) onto the family C (under ⊆).

Equations

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

Exercise 3.27.

noncomputable def Domain.Neighborhood.Exercise327.funSpaceReprIso {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : (Exercise222.reprSystem (C V₀ V₁) ⋯ ⋯).Element ≃o (funSpace V₀ V₁).Element

Exercise 3.27. The function space |𝒟₀ → 𝒟₁| is (order-)isomorphic to the domain produced by the abstract representation theorem (Exercise 2.22) applied to the family C of graphs of approximable maps. This re-proves that approximable mappings form a domain without appealing to the explicit step-set neighbourhood system of Definition 3.8 — composing Exercise 2.22's reprIso with the graph isomorphism (graphEquiv) and Theorem 3.10 (funSpaceEquiv).

Equations

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