Lecture II (§2) — approximable mappings: Definitions 2.1, 2.2 and Theorems

2.5–2.7

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture II, Approximable mappings. A mapping of domains that "preserves the spirit of approximation" is given not by a function on ideal elements but by a relation between neighbourhoods: X f Y reads "if the input is approximated at least as well as by X, then the output is approximated at least as well as by Y."

This file formalizes the §2 core:

• Definition 2.1 — ApproximableMap V₀ V₁: a relation f ⊆ 𝒟₀ × 𝒟₁ with (i) Δ₀ f Δ₁ (master_rel), (ii) X f Y → X f Y' → X f (Y ∩ Y') (inter_right, the consistency/intersectivity condition), (iii) X f Y → X' ⊆ X → Y ⊆ Y' → X' f Y' (mono, monotonicity: sharper input, blunter output). We carry rel_dom/rel_cod recording f ⊆ 𝒟₀ × 𝒟₁.
• Proposition 2.2 — every approximable mapping determines an elementwise function toElementMap f : |𝒟₀| → |𝒟₁|, f(x) = {Y ∣ ∃ X ∈ x, X f Y}, which is a filter (i)–(iii) are all used); the relation is recovered by rel_iff_mem_principal (X f Y ↔ Y ∈ f(↑X)); the map is monotone (toElementMap_mono); and two approximable maps are equal iff they induce the same elementwise map (ext_of_toElementMap).
• Theorem 2.5 — neighbourhood systems and approximable maps form a category: identity idMap (X I_D Y ↔ X ⊆ Y), composition comp g f (X (g∘f) Z ↔ ∃ Y, X f Y ∧ Y g Z), with the identity laws idMap_comp/comp_idMap and associativity comp_assoc.
• Proposition 2.6 — the elementwise action is a functor to sets and functions: toElementMap_idMap (I_D(x) = x) and toElementMap_comp ((g∘f)(x) = g(f(x))).
• Theorem 2.7 — every domain isomorphism e : |𝒟₀| ≃o |𝒟₁| (Definition 1.9) comes from an approximable map: ofIso e with toElementMap_ofIso ((ofIso e)(x) = e(x)), packaged as exists_approximable_of_iso; moreover e carries finite (principal) elements to finite elements (exists_principal_eq_apply_principal), via the directed-union construction sSupDirected.

Everything in this file is choice-free (#print axioms ⊆ {propext, Quot.sound}); the only classical lemma is ext_of_toElementMap, which decides neighbourhood membership by by_cases (Classical.em).

def Domain.Neighborhood.NeighborhoodSystem.sSupDirected {α : Type u_1} (V : NeighborhoodSystem α) (S : Set V.Element) (hne : S.Nonempty) (hdir : ∀ (a : V.Element), a ∈ S → ∀ (b : V.Element), b ∈ S → ∃ (c : V.Element), c ∈ S ∧ a ≤ c ∧ b ≤ c) : V.Element

Directed union of filters. The union ⋃ S = {Z ∣ ∃ s ∈ S, Z ∈ s} of a non-empty directed family S of elements (any two members have an upper bound in S) is again an element. The only non-trivial law is inter_mem: given Z ∈ a and Z' ∈ b, an upper bound c ⊇ a, b contains both, hence Z ∩ Z' ∈ c. (Generalizes chainUnion of Exercise 1.24 from chains to directed sets; this is the construction behind Exercise 2.11 and Scott's finiteness argument in Theorem 2.7.)

Equations

• V.sSupDirected S hne hdir = { mem := fun (Z : Set α) => ∃ (s : V.Element), s ∈ S ∧ s.mem Z, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

theorem Domain.Neighborhood.NeighborhoodSystem.le_sSupDirected {α : Type u_1} (V : NeighborhoodSystem α) (S : Set V.Element) (hne : S.Nonempty) (hdir : ∀ (a : V.Element), a ∈ S → ∀ (b : V.Element), b ∈ S → ∃ (c : V.Element), c ∈ S ∧ a ≤ c ∧ b ≤ c) {a : V.Element} (ha : a ∈ S) : a ≤ V.sSupDirected S hne hdir

Each member of a directed family approximates the directed union.

theorem Domain.Neighborhood.NeighborhoodSystem.sSupDirected_le {α : Type u_1} (V : NeighborhoodSystem α) (S : Set V.Element) (hne : S.Nonempty) (hdir : ∀ (a : V.Element), a ∈ S → ∀ (b : V.Element), b ∈ S → ∃ (c : V.Element), c ∈ S ∧ a ≤ c ∧ b ≤ c) {y : V.Element} (hy : ∀ (s : V.Element), s ∈ S → s ≤ y) : V.sSupDirected S hne hdir ≤ y

The directed union is the least upper bound: an upper bound of every member dominates it.

structure Domain.Neighborhood.ApproximableMap {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : Type (max u_1 u_2)

Definition 2.1 (Scott 1981, PRG-19). An approximable mapping f : 𝒟₀ → 𝒟₁ is a relation rel between neighbourhoods (rel X Y, Scott's X f Y) confined to 𝒟₀ × 𝒟₁ and satisfying Scott's three conditions:

• (i) Δ₀ f Δ₁ — master_rel;
• (ii) X f Y and X f Y' imply X f (Y ∩ Y') — inter_right;
• (iii) X f Y, X' ⊆ X, Y ⊆ Y' imply X' f Y' — mono (the targets X', Y' must be neighbourhoods, as Scott's relation lives on 𝒟₀ × 𝒟₁).

• rel : Set α → Set β → Prop

  The underlying neighbourhood relation X f Y.

• rel_dom {X : Set α} {Y : Set β} : self.rel X Y → V₀.mem X

  f ⊆ 𝒟₀ × 𝒟₁ (domain side): related inputs are neighbourhoods.

• rel_cod {X : Set α} {Y : Set β} : self.rel X Y → V₁.mem Y

  f ⊆ 𝒟₀ × 𝒟₁ (codomain side): related outputs are neighbourhoods.

• master_rel : self.rel V₀.master V₁.master

  (i) Δ₀ f Δ₁.

• inter_right {X : Set α} {Y Y' : Set β} : self.rel X Y → self.rel X Y' → self.rel X (Y ∩ Y')

  (ii) intersectivity on the output: X f Y → X f Y' → X f (Y ∩ Y').

• mono {X X' : Set α} {Y Y' : Set β} : self.rel X Y → X' ⊆ X → Y ⊆ Y' → V₀.mem X' → V₁.mem Y' → self.rel X' Y'

  (iii) monotonicity: a sharper input X' ⊆ X with a blunter output Y ⊆ Y' is still related, provided X', Y' are neighbourhoods.

theorem Domain.Neighborhood.ApproximableMap.ext {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f g : ApproximableMap V₀ V₁} (h : ∀ (X : Set α) (Y : Set β), f.rel X Y ↔ g.rel X Y) : f = g

Extensionality for the relation. Two approximable maps with the same neighbourhood relation are equal (the remaining fields are propositions).

def Domain.Neighborhood.ApproximableMap.toElementMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) (x : V₀.Element) : V₁.Element

Proposition 2.2(i) (Scott 1981, PRG-19). The elementwise function determined by an approximable mapping: f(x) = {Y ∈ 𝒟₁ ∣ ∃ X ∈ x, X f Y}. The four filter laws use all of Definition 2.1: master_mem uses (i); inter_mem uses (ii) together with (iii) (to pull both outputs back along the common input X ∩ X'); up_mem uses (iii).

Equations

• f.toElementMap x = { mem := fun (Y : Set β) => ∃ (X : Set α), x.mem X ∧ f.rel X Y, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

@[simp]

theorem Domain.Neighborhood.ApproximableMap.mem_toElementMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) (x : V₀.Element) {Y : Set β} : (f.toElementMap x).mem Y ↔ ∃ (X : Set α), x.mem X ∧ f.rel X Y

theorem Domain.Neighborhood.ApproximableMap.rel_iff_mem_principal {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) {X : Set α} (hX : V₀.mem X) {Y : Set β} : f.rel X Y ↔ (f.toElementMap (V₀.principal hX)).mem Y

Proposition 2.2(ii) (Scott 1981, PRG-19). The relation is recovered from the elementwise map: for X ∈ 𝒟₀, X f Y ↔ Y ∈ f(↑X). (→ since X ∈ ↑X; ← since any Z ∈ ↑X has X ⊆ Z, so Z f Y monotonically yields X f Y.)

theorem Domain.Neighborhood.ApproximableMap.toElementMap_mono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) {x y : V₀.Element} (hxy : x ≤ y) : f.toElementMap x ≤ f.toElementMap y

Proposition 2.2(iii) (Scott 1981, PRG-19). Approximable maps are monotone on elements: x ⊑ y ⟹ f(x) ⊑ f(y).

theorem Domain.Neighborhood.ApproximableMap.ext_of_toElementMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f g : ApproximableMap V₀ V₁} (h : ∀ (x : V₀.Element), f.toElementMap x = g.toElementMap x) : f = g

Proposition 2.2(iv) (Scott 1981, PRG-19). Two approximable maps are identical as relations iff they induce the same elementwise function: (∀ x, f(x) = g(x)) ⟹ f = g. For neighbourhoods X the relation is read off f(↑X) (rel_iff_mem_principal); off 𝒟₀ both relations are empty.

Theorem 2.5 — the category of neighbourhood systems and approximable

mappings.

def Domain.Neighborhood.ApproximableMap.idMap {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap V V

Theorem 2.5(i) (Scott 1981, PRG-19) — the identity mapping I_D. X I_D Y ↔ X ⊆ Y (confined to 𝒟 × 𝒟). It is approximable: (i) Δ ⊆ Δ; (ii) X ⊆ Y, X ⊆ Y' give X ⊆ Y ∩ Y' with witness X; (iii) is transitivity X' ⊆ X ⊆ Y ⊆ Y'.

Equations

• Domain.Neighborhood.ApproximableMap.idMap V = { rel := fun (X Y : Set α) => V.mem X ∧ V.mem Y ∧ X ⊆ Y, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

@[simp]

theorem Domain.Neighborhood.ApproximableMap.idMap_rel {α : Type u_1} {V : NeighborhoodSystem α} {X Y : Set α} : (idMap V).rel X Y ↔ V.mem X ∧ V.mem Y ∧ X ⊆ Y

def Domain.Neighborhood.ApproximableMap.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap V₁ V₂) (f : ApproximableMap V₀ V₁) : ApproximableMap V₀ V₂

Theorem 2.5(ii) (Scott 1981, PRG-19) — composition g ∘ f. X (g∘f) Z ↔ ∃ Y, X f Y ∧ Y g Z. Approximability is Scott's verification: (i) use Y = Δ₁; (ii) intersect both witnesses via f.inter_right then g.inter_right (narrowing the inner neighbourhood with g.mono); (iii) narrow the input with f.mono and widen the output with g.mono, keeping the same witness.

Equations

• g.comp f = { rel := fun (X : Set α) (Z : Set γ) => ∃ (Y : Set β), f.rel X Y ∧ g.rel Y Z, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

@[simp]

theorem Domain.Neighborhood.ApproximableMap.comp_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {g : ApproximableMap V₁ V₂} {f : ApproximableMap V₀ V₁} {X : Set α} {Z : Set γ} : (g.comp f).rel X Z ↔ ∃ (Y : Set β), f.rel X Y ∧ g.rel Y Z

theorem Domain.Neighborhood.ApproximableMap.idMap_comp {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) : (idMap V₁).comp f = f

Theorem 2.5 — left identity law. I_{D₁} ∘ f = f. (→: a witness Y ⊆ Z widens the output of f by f.mono; ←: take Y = Z.)

theorem Domain.Neighborhood.ApproximableMap.comp_idMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) : f.comp (idMap V₀) = f

Theorem 2.5 — right identity law. f ∘ I_{D₀} = f. (→: a witness X ⊆ Y sharpens the input of f by f.mono; ←: take Y = X.)

theorem Domain.Neighborhood.ApproximableMap.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {V₃ : NeighborhoodSystem δ} (h : ApproximableMap V₂ V₃) (g : ApproximableMap V₁ V₂) (f : ApproximableMap V₀ V₁) : (h.comp g).comp f = h.comp (g.comp f)

Theorem 2.5 — associativity. h ∘ (g ∘ f) = (h ∘ g) ∘ f. Pure reassociation of the existential witnesses.

Proposition 2.6 — the functor to sets and functions.

@[simp]

theorem Domain.Neighborhood.ApproximableMap.toElementMap_idMap {α : Type u_1} {V₀ : NeighborhoodSystem α} (x : V₀.Element) : (idMap V₀).toElementMap x = x

Proposition 2.6(i) (Scott 1981, PRG-19). The identity mapping acts as the identity on elements: I_D(x) = x. (→: X ∈ x, X ⊆ Y ∈ 𝒟 gives Y ∈ x by up_mem; ←: take X = Y.)

theorem Domain.Neighborhood.ApproximableMap.toElementMap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap V₁ V₂) (f : ApproximableMap V₀ V₁) (x : V₀.Element) : (g.comp f).toElementMap x = g.toElementMap (f.toElementMap x)

Proposition 2.6(ii) (Scott 1981, PRG-19). Composition of approximable mappings becomes composition of the elementwise functions: (g ∘ f)(x) = g(f(x)). Both sides unfold to ∃ Y X, x.mem X ∧ X f Y ∧ Y g Z; the proof is a reassociation of existentials.

Theorem 2.7 — every domain isomorphism comes from an approximable mapping.

def Domain.Neighborhood.ApproximableMap.ofIso {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) : ApproximableMap V₀ V₁

Theorem 2.7 (Scott 1981, PRG-19) — the approximable map of an isomorphism. Given a domain isomorphism e : |𝒟₀| ≃o |𝒟₁| (Definition 1.9), Scott's "only way to define a neighbourhood mapping" is the relation X f Y ↔ Y ∈ e(↑X). The conditions of 2.1 hold because e is monotone: (i) Δ₁ ∈ e(⊥₀) is master_mem; (ii) is inter_mem of the filter e(↑X); (iii) sharpening X' ⊆ X means ↑X ⊑ ↑X', so e(↑X) ⊑ e(↑X') and the output transports along, then widens by up_mem.

Equations

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

theorem Domain.Neighborhood.ApproximableMap.toElementMap_ofIso {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) (x : V₀.Element) : (ofIso e).toElementMap x = e x

Theorem 2.7 — the relation re-defines the function. The elementwise map of ofIso e is e itself: (ofIso e)(x) = e(x) for every x. The forward inclusion uses that X ∈ x implies ↑X ⊑ x, hence e(↑X) ⊑ e(x); the reverse uses surjectivity of e (via e.symm) exactly as in Scott's proof — one shows x = e⁻¹((ofIso e)(x)) by antisymmetry.

theorem Domain.Neighborhood.ApproximableMap.exists_approximable_of_iso {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) : ∃ (f : ApproximableMap V₀ V₁), ∀ (x : V₀.Element), f.toElementMap x = e x

Theorem 2.7 (statement) (Scott 1981, PRG-19). "Every isomorphism between domains results from an approximable mapping." For any domain isomorphism e, there is an approximable mapping whose elementwise action is exactly e.

theorem Domain.Neighborhood.ApproximableMap.exists_principal_eq_apply_principal {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) {X : Set α} (hX : V₀.mem X) : ∃ (Y : Set β), ∃ (hY : V₁.mem Y), e (V₀.principal hX) = V₁.principal hY

Theorem 2.7 (Scott 1981, PRG-19) — finite elements go to finite elements. A domain isomorphism e carries the finite (principal) element ↑X to a finite element ↑Y of the other domain. Following Scott: with w = e(↑X), the set S = {e⁻¹(↑Y) ∣ Y ∈ w} is directed (intersections of members of w give upper bounds), so its union z = ⋃ S is an element (sSupDirected). One shows z = ↑X (each e⁻¹(↑Y) ⊑ e⁻¹(w) = ↑X, and conversely w ⊑ e(z) forces ↑X = e⁻¹(w) ⊑ z); then X ∈ z lands in some e⁻¹(↑Y), giving w ⊑ ↑Y, while ↑Y ⊑ w is automatic — so w = ↑Y.