Lecture II (§2) — Exercises 2.8–2.12 and 2.19 (the algebra of approximable

mappings)

Following Dana Scott, PRG-19 (1981), Lecture II. This file collects the structural exercises about approximable mappings, all built on Approximable.lean:

• Exercise 2.8 — an approximable map is determined by its action on finite (principal) elements (eq_of_toElementMap_principal); and any monotone function on finite elements extends to an approximable map (ofMono, toElementMap_ofMono_principal).
• Exercise 2.9 — Scott's formula f(x) = ⋃ {f(↑X) ∣ X ∈ x} (toElementMap_mem_iff_principal).
• Exercise 2.10 — the pointwise meet of two maps: h(x) = f(x) ∩ g(x) (interMap).
• Exercise 2.11 — |𝒟| is closed under directed unions (iSupDirected, with mem_iSupDirected/le_iSupDirected/iSupDirected_le), and approximable maps preserve them (toElementMap_iSupDirected).
• Exercise 2.12 — a directed family of approximable maps has a pointwise union that is again approximable (iSupMap, mem_toElementMap_iSupMap).
• Exercise 2.19 — two-variable approximable maps f : 𝒟₀ × 𝒟₁ → 𝒟₂ as ternary relations (ApproximableMap₂), with the Proposition 2.2 analogue (toElementMap₂, rel₂_iff_mem_principal).

All constructions are choice-free (#print axioms ⊆ {propext, Quot.sound}); the two eq_of_…/uniqueness lemmas decide membership by by_cases and are therefore classical, exactly like ext_of_toElementMap.

def Domain.Neighborhood.NeighborhoodSystem.iSupDirected {α : Type u_4} {V : NeighborhoodSystem α} {I : Type u_5} [Nonempty I] (a : I → V.Element) (hdir : ∀ (i j : I), ∃ (k : I), a i ≤ a k ∧ a j ≤ a k) : V.Element

Exercise 2.11 — directed union (indexed form). For a directed family a : I → |𝒟| (any two a i, a j have a common upper bound a k), the union ⋃ᵢ a i is again an element of |𝒟|. Built on sSupDirected over the range.

Equations

• Domain.Neighborhood.NeighborhoodSystem.iSupDirected a hdir = V.sSupDirected (Set.range a) ⋯ ⋯

theorem Domain.Neighborhood.NeighborhoodSystem.mem_iSupDirected {α : Type u_4} {V : NeighborhoodSystem α} {I : Type u_5} [Nonempty I] (a : I → V.Element) (hdir : ∀ (i j : I), ∃ (k : I), a i ≤ a k ∧ a j ≤ a k) {Z : Set α} : (iSupDirected a hdir).mem Z ↔ ∃ (i : I), (a i).mem Z

theorem Domain.Neighborhood.NeighborhoodSystem.le_iSupDirected {α : Type u_4} {V : NeighborhoodSystem α} {I : Type u_5} [Nonempty I] (a : I → V.Element) (hdir : ∀ (i j : I), ∃ (k : I), a i ≤ a k ∧ a j ≤ a k) (i : I) : a i ≤ iSupDirected a hdir

theorem Domain.Neighborhood.NeighborhoodSystem.iSupDirected_le {α : Type u_4} {V : NeighborhoodSystem α} {I : Type u_5} [Nonempty I] (a : I → V.Element) (hdir : ∀ (i j : I), ∃ (k : I), a i ≤ a k ∧ a j ≤ a k) {y : V.Element} (hy : ∀ (i : I), a i ≤ y) : iSupDirected a hdir ≤ y

Exercise 2.8 — determination by, and extension from, finite elements.

theorem Domain.Neighborhood.ApproximableMap.eq_of_toElementMap_principal {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f g : ApproximableMap V₀ V₁} (h : ∀ (X : Set α) (hX : V₀.mem X), f.toElementMap (V₀.principal hX) = g.toElementMap (V₀.principal hX)) : f = g

Exercise 2.8 (uniqueness). An approximable mapping is uniquely determined by its elementwise effect on finite elements: if f(↑X) = g(↑X) for every neighbourhood X, then f = g. (Off 𝒟₀ both relations are empty; on 𝒟₀ use rel_iff_mem_principal.)

def Domain.Neighborhood.ApproximableMap.ofMono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (m : (X : Set α) → V₀.mem X → V₁.Element) (hmono : ∀ (X X' : Set α) (hX : V₀.mem X) (hX' : V₀.mem X'), X' ⊆ X → m X hX ≤ m X' hX') : ApproximableMap V₀ V₁

Exercise 2.8 (extension). Any monotone function on finite elements comes from an approximable map. Here a "monotone function on finite elements" is a map m sending each neighbourhood X (a finite element ↑X) to an element m X hX : |𝒟₁|, monotone in the sense X' ⊆ X → m X hX ≤ m X' hX' (i.e. ↑X ⊑ ↑X' ⟹ m(↑X) ⊑ m(↑X')). The induced relation is X f Y ↔ Y ∈ m(↑X).

Equations

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

theorem Domain.Neighborhood.ApproximableMap.toElementMap_ofMono_principal {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (m : (X : Set α) → V₀.mem X → V₁.Element) (hmono : ∀ (X X' : Set α) (hX : V₀.mem X) (hX' : V₀.mem X'), X' ⊆ X → m X hX ≤ m X' hX') (X : Set α) (hX : V₀.mem X) : (ofMono m hmono).toElementMap (V₀.principal hX) = m X hX

Exercise 2.8 (extension, computed). The map ofMono m realizes m on finite elements: (ofMono m)(↑X) = m(↑X).

Exercise 2.9 — the elementwise map as a union over finite approximants.

theorem Domain.Neighborhood.ApproximableMap.toElementMap_mem_iff_principal {α : 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 α), ∃ (hx : x.mem X), (f.toElementMap (V₀.principal ⋯)).mem Y

Exercise 2.9 (Scott 1981, PRG-19). f(x) = ⋃ {f(↑X) ∣ X ∈ x}: a neighbourhood Y lies in f(x) iff it lies in f(↑X) for some X ∈ x. (Immediate from rel_iff_mem_principal.)

Exercise 2.10 — the pointwise meet of two approximable maps.

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

Exercise 2.10 (Scott 1981, PRG-19). The pointwise intersection h of two approximable maps: X h Z ↔ X f Z ∧ X g Z. It is approximable, and (mem_toElementMap_interMap) h(x) = f(x) ∩ g(x).

Equations

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

theorem Domain.Neighborhood.ApproximableMap.mem_toElementMap_interMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f g : ApproximableMap V₀ V₁) (x : V₀.Element) {Z : Set β} : ((f.interMap g).toElementMap x).mem Z ↔ (f.toElementMap x).mem Z ∧ (g.toElementMap x).mem Z

Exercise 2.10. h(x) = f(x) ∩ g(x) (the meet in |𝒟₁|). The non-trivial direction combines witnesses X ∈ x (for f) and X' ∈ x (for g) through X ∩ X' ∈ x using mono.

Exercise 2.11 — approximable maps preserve directed unions.

theorem Domain.Neighborhood.ApproximableMap.toElementMap_iSupDirected {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) {I : Type u_4} [Nonempty I] (a : I → V₀.Element) (hdir : ∀ (i j : I), ∃ (k : I), a i ≤ a k ∧ a j ≤ a k) : f.toElementMap (NeighborhoodSystem.iSupDirected a hdir) = NeighborhoodSystem.iSupDirected (fun (i : I) => f.toElementMap (a i)) ⋯

Exercise 2.11 (Scott 1981, PRG-19). Approximable mappings preserve directed unions: f(⋃ᵢ a i) = ⋃ᵢ f(a i). Both sides have member Y iff ∃ i X, X ∈ a i ∧ X f Y.

Exercise 2.12 — the pointwise union of a directed family of maps.

def Domain.Neighborhood.ApproximableMap.iSupMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {I : Type u_4} [Nonempty I] (f : I → ApproximableMap V₀ V₁) (hdir : ∀ (i j : I), ∃ (k : I), (∀ (X : Set α) (Y : Set β), (f i).rel X Y → (f k).rel X Y) ∧ ∀ (X : Set α) (Y : Set β), (f j).rel X Y → (f k).rel X Y) : ApproximableMap V₀ V₁

Exercise 2.12 (Scott 1981, PRG-19). The pointwise union of a directed family of approximable maps is approximable. Directedness is stated on the relations: any two f i, f j are dominated by some f k. The union relation is X g Z ↔ ∃ i, X (f i) Z.

Equations

• Domain.Neighborhood.ApproximableMap.iSupMap f hdir = { rel := fun (X : Set α) (Z : Set β) => ∃ (i : I), (f i).rel X Z, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

theorem Domain.Neighborhood.ApproximableMap.mem_toElementMap_iSupMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {I : Type u_4} [Nonempty I] (f : I → ApproximableMap V₀ V₁) (hdir : ∀ (i j : I), ∃ (k : I), (∀ (X : Set α) (Y : Set β), (f i).rel X Y → (f k).rel X Y) ∧ ∀ (X : Set α) (Y : Set β), (f j).rel X Y → (f k).rel X Y) (x : V₀.Element) {Y : Set β} : ((iSupMap f hdir).toElementMap x).mem Y ↔ ∃ (i : I), ((f i).toElementMap x).mem Y

Exercise 2.12. The induced elementwise map is the pointwise union: g(x) = ⋃ᵢ f i (x).

Exercise 2.19 — approximable mappings of two variables.

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

Exercise 2.19 (Scott 1981, PRG-19). An approximable mapping of two variables f : 𝒟₀ × 𝒟₁ → 𝒟₂ is a ternary relation X, Y f Z confined to 𝒟₀ × 𝒟₁ × 𝒟₂ with the natural generalization of Definition 2.1: (i) Δ₀, Δ₁ f Δ₂; (ii) intersectivity on the output; (iii) monotonicity jointly in both inputs (sharper) and the output (blunter).

• rel : Set α → Set β → Set γ → Prop

  The underlying ternary relation X, Y f Z.

• rel_dom₀ {X : Set α} {Y : Set β} {Z : Set γ} : self.rel X Y Z → V₀.mem X
• rel_dom₁ {X : Set α} {Y : Set β} {Z : Set γ} : self.rel X Y Z → V₁.mem Y
• rel_cod {X : Set α} {Y : Set β} {Z : Set γ} : self.rel X Y Z → V₂.mem Z
• master_rel : self.rel V₀.master V₁.master V₂.master

  (i) Δ₀, Δ₁ f Δ₂.

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

  (ii) intersectivity on the output.

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

  (iii) joint monotonicity: sharper inputs X' ⊆ X, Y' ⊆ Y; blunter output Z ⊆ Z'.

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

Exercise 2.19 (Proposition 2.2 analogue). A two-variable approximable mapping determines an elementwise function of two arguments: f(x, y) = {Z ∣ ∃ X ∈ x, ∃ Y ∈ y, X, Y f Z}. The filter laws use all three conditions: inter_mem pulls both outputs back to (X ∩ X', Y ∩ Y') via mono then inter_right.

Equations

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

@[simp]

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

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

Exercise 2.19 (recovery of the relation). X, Y f Z ↔ Z ∈ f(↑X, ↑Y), the two-variable analogue of Proposition 2.2(ii).

theorem Domain.Neighborhood.ApproximableMap₂.toElementMap₂_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (f : ApproximableMap₂ V₀ V₁ V₂) {x x' : V₀.Element} {y y' : V₁.Element} (hx : x ≤ x') (hy : y ≤ y') : f.toElementMap₂ x y ≤ f.toElementMap₂ x' y'

Exercise 2.19 (monotonicity). The two-variable elementwise map is monotone in each argument jointly: x ⊑ x', y ⊑ y' imply f(x, y) ⊑ f(x', y').