Exercise 2.14 (Scott 1981, PRG-19, §2) — the neighbourhood correspondence φ of

an isomorphism

EXERCISE 2.14. Let f : |𝒟₀| → |𝒟₁| be an isomorphism between domains. Let φ : 𝒟₀ → 𝒟₁ be the one-one correspondence between neighbourhoods provided by Theorem 2.7 where f(↑X) = ↑φ(X) for all X ∈ 𝒟₀. Show that the approximable mapping determined by f is just the relationship φ(X) ⊆ Y. In addition prove that if X, X' ∈ 𝒟₀ are consistent, then φ(X ∩ X') = φ(X) ∩ φ(X'). Remark that the isomorphisms between domains correspond exactly to the isomorphisms between neighbourhood systems (in the sense of one-one inclusion preserving correspondences).

Theorem 2.7 (exists_principal_eq_apply_principal) says a domain isomorphism e : |𝒟₀| ≃o |𝒟₁| carries each finite element ↑X to a finite element ↑Y. We extract the witness Y by Classical.choose, getting φ with φ_spec : e(↑X) = ↑φ(X):

• phi e hX, phi_mem, phi_spec — the neighbourhood correspondence φ of e.
• rel_ofIso_iff — the approximable mapping of e is exactly φ(X) ⊆ Y: (ofIso e).rel X Y ↔ 𝒟₁ Y ∧ φ(X) ⊆ Y (for X ∈ 𝒟₀).
• phi_inter — φ(X ∩ X') = φ(X) ∩ φ(X') for consistent X, X' (i.e. X ∩ X' ∈ 𝒟₀). The proof goes through the order structure: ↑(X ∩ X') is the least upper bound (join) of ↑X, ↑X' in |𝒟₀| (note the inclusion order is reversed); e and e.symm are monotone, so they preserve this join, and the join of two consistent principals ↑A, ↑B in |𝒟₁| is ↑(A ∩ B).

φ is Classical.choose-based, hence noncomputable and classical; the order-theoretic proofs of rel_ofIso_iff/phi_inter are otherwise choice-free (propext, Quot.sound).

noncomputable def Domain.Neighborhood.phi {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) {X : Set α} (hX : V₀.mem X) : Set β

Exercise 2.14 — the correspondence φ. For a domain isomorphism e and X ∈ 𝒟₀, φ(X) is the neighbourhood with e(↑X) = ↑φ(X) provided by Theorem 2.7.

Equations

• Domain.Neighborhood.phi e hX = Classical.choose ⋯

theorem Domain.Neighborhood.phi_mem {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) {X : Set α} (hX : V₀.mem X) : V₁.mem (phi e hX)

φ(X) ∈ 𝒟₁.

theorem Domain.Neighborhood.phi_spec {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) {X : Set α} (hX : V₀.mem X) : e (V₀.principal hX) = V₁.principal ⋯

Theorem 2.7 defining equation: e(↑X) = ↑φ(X).

theorem Domain.Neighborhood.rel_ofIso_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) {X : Set α} (hX : V₀.mem X) {Y : Set β} : (ApproximableMap.ofIso e).rel X Y ↔ V₁.mem Y ∧ phi e hX ⊆ Y

Exercise 2.14 — the approximable mapping of e is φ(X) ⊆ Y. For X ∈ 𝒟₀, (ofIso e).rel X Y ↔ Y ∈ 𝒟₁ ∧ φ(X) ⊆ Y. (Immediate from phi_spec and mem_principal.)

theorem Domain.Neighborhood.phi_inter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (e : V₀.Element ≃o V₁.Element) {X X' : Set α} (hX : V₀.mem X) (hX' : V₀.mem X') (hXX' : V₀.mem (X ∩ X')) : phi e hXX' = phi e hX ∩ phi e hX'

Exercise 2.14 — φ preserves consistent intersections. If X, X' are consistent (X ∩ X' ∈ 𝒟₀), then φ(X ∩ X') = φ(X) ∩ φ(X').

↑(X ∩ X') is the join of ↑X, ↑X' in |𝒟₀| (the order is inclusion-reversed). e/e.symm preserve this least upper bound, and the join of the consistent principals ↑φ(X), ↑φ(X') is ↑(φ(X) ∩ φ(X')).