Exercise 3.21 (Scott 1981, PRG-19, §3) — when does [Y, Z] determine Y and

Z?

In the proof of Theorem 3.12 it is tacitly assumed that the function-space neighbourhood [Y, Z] (the set step Y Z = {f ∣ Y f Z} of approximable mappings) uniquely determines its endpoints Y, Z. Scott's Exercise 3.21 asks to make this precise.

• If Z ≠ Δ₂ the pair is determined: [Y, Z] = [Y', Z'] forces Y = Y' and Z = Z' (step_eq_of_ne_master). The hint is to use the least element of [Y, Z] — here the single-step map leastMap [(Y, Z)] of Proposition 3.9.
• If Z = Δ₂ then [Y, Δ₂] = |𝒟₁ → 𝒟₂| is the whole space for every Y (step_master_right), so Y is not determined; nevertheless the biconditional of Theorem 3.12 stays valid because Δ₁ g Δ₂ always holds.
• General criterion (step_eq_iff): [Y, Z] = [Y', Z'] iff either both outputs are Δ₂, or Y = Y' and Z = Z'.

Everything is choice-free (#print axioms ⊆ {propext, Quot.sound}).

The intersection interYs of a single step.

theorem Domain.Neighborhood.interYs_single_subset_eq {α : Type u_1} {β : Type u_2} {V₁ : NeighborhoodSystem β} {YX : Set α} {Z : Set β} {X : Set α} (hZ : V₁.mem Z) (hXY : X ⊆ YX) : interYs V₁.master [(YX, Z)] X = Z

For a single step [Y, Z] and a sharp enough input X ⊆ Y, the intersection is just Z.

theorem Domain.Neighborhood.interYs_single_not_subset_eq {α : Type u_1} {β : Type u_2} {V₁ : NeighborhoodSystem β} {YX : Set α} {Z : Set β} {X : Set α} (hXY : ¬X ⊆ YX) : interYs V₁.master [(YX, Z)] X = V₁.master

For a single step [Y, Z] and an input X ⊄ Y, the intersection is the whole master Δ₂.

The least element of a single step neighbourhood.

theorem Domain.Neighborhood.stepCons {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set α} {Z : Set β} (hZ : V₁.mem Z) {X : Set α} : V₀.mem X → V₁.mem (interYs V₁.master [(Y, Z)] X)

Consistency (hcons) for a single step [Y, Z]: the intersection over the relevant outputs is either Z (sharp input) or Δ₂ (blunt input), both neighbourhoods.

def Domain.Neighborhood.leastStep {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (Y : Set α) (Z : Set β) (hY : V₀.mem Y) (hZ : V₁.mem Z) : ApproximableMap V₀ V₁

The single-step least map f₀ ∈ [Y, Z]: leastMap [(Y, Z)], the minimal approximable mapping relating Y to Z.

Equations

• Domain.Neighborhood.leastStep Y Z hY hZ = Domain.Neighborhood.leastMap [(Y, Z)] ⋯

theorem Domain.Neighborhood.leastStep_mem {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set α} {Z : Set β} (hY : V₀.mem Y) (hZ : V₁.mem Z) : leastStep Y Z hY hZ ∈ step Y Z

theorem Domain.Neighborhood.leastStep_le {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set α} {Z : Set β} (hY : V₀.mem Y) (hZ : V₁.mem Z) {f : ApproximableMap V₀ V₁} (hf : f ∈ step Y Z) : leastStep Y Z hY hZ ≤ f

theorem Domain.Neighborhood.leastStep_rel {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set α} {Z : Set β} (hY : V₀.mem Y) (hZ : V₁.mem Z) {Y' : Set α} {Z' : Set β} (hY' : V₀.mem Y') (hZ' : V₁.mem Z') : (leastStep Y Z hY hZ).rel Y' Z' ↔ interYs V₁.master [(Y, Z)] Y' ⊆ Z'

f₀ = leastStep Y Z relates Y' to Z' iff (Y' ⊆ Y and Z ⊆ Z') or Z' = Δ₂.

[Y, Z] is the whole space exactly when Z = Δ₂.

theorem Domain.Neighborhood.step_master_right {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (Y : Set α) (hY : V₀.mem Y) : step Y V₁.master = Set.univ

Exercise 3.21. If the output is the master, [Y, Δ₂] is the whole function space.

theorem Domain.Neighborhood.step_eq_univ_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set α} {Z : Set β} (hY : V₀.mem Y) (hZ : V₁.mem Z) : step Y Z = Set.univ ↔ Z = V₁.master

Uniqueness when Z ≠ Δ₂.

theorem Domain.Neighborhood.leastStep_eq_of_step_eq {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set α} {Z : Set β} (hY : V₀.mem Y) (hZ : V₁.mem Z) {Y' : Set α} {Z' : Set β} (hY' : V₀.mem Y') (hZ' : V₁.mem Z') (h : step Y Z = step Y' Z') : leastStep Y Z hY hZ = leastStep Y' Z' hY' hZ'

The least elements of equal step neighbourhoods coincide.

theorem Domain.Neighborhood.step_eq_of_ne_master {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set α} {Z : Set β} (hY : V₀.mem Y) (hZ : V₁.mem Z) {Y' : Set α} {Z' : Set β} (hY' : V₀.mem Y') (hZ' : V₁.mem Z') (hZne : Z ≠ V₁.master) (h : step Y Z = step Y' Z') : Y = Y' ∧ Z = Z'

Exercise 3.21 (Scott 1981, PRG-19). If Z ≠ Δ₂, the neighbourhood [Y, Z] determines both endpoints: [Y, Z] = [Y', Z'] implies Y = Y' and Z = Z'.

The general identity criterion.

theorem Domain.Neighborhood.step_eq_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set α} {Z : Set β} (hY : V₀.mem Y) (hZ : V₁.mem Z) {Y' : Set α} {Z' : Set β} (hY' : V₀.mem Y') (hZ' : V₁.mem Z') : step Y Z = step Y' Z' ↔ Z = V₁.master ∧ Z' = V₁.master ∨ Y = Y' ∧ Z = Z'

Exercise 3.21 (Scott 1981, PRG-19). The simple criterion for identity of function-space neighbourhoods: [Y, Z] = [Y', Z'] iff both outputs are the master Δ₂, or the pairs coincide.