Exercise 3.16 (Scott 1981, PRG-19, §3) — the infinite iterate 𝒟^∞

Scott: for a neighbourhood system 𝒟 over Δ, let Δ^∞ = ⋃ₙ 1ⁿ0Δ be infinitely many disjoint copies of Δ, and let 𝒟^∞ be the least family of subsets with

1. Δ^∞ ∈ 𝒟^∞, and
2. X ∈ 𝒟, Y ∈ 𝒟^∞ ⟹ 0X ∪ 1Y ∈ 𝒟^∞.

He asks to show 𝒟^∞ is a neighbourhood system over Δ^∞, that 𝒟^∞ ≅ 𝒟 × 𝒟^∞, and that the elements of |𝒟^∞| are in one-one correspondence with arbitrary infinite sequences ⟨xₙ⟩ of elements xₙ ∈ |𝒟|, via the combinations of neighbourhoods

0X₀ ∪ 10X₁ ∪ ⋯ ∪ 1ⁿ0Xₙ ∪ ⋯ (with all but finitely many Xₘ = Δ).

Model. We take the token type to be ℕ × α, where (n, a) is "the token a ∈ Δ sitting in the n-th copy" (i.e. Scott's 1ⁿ0a). A neighbourhood 0X₀ ∪ 1ⁿ0Xₙ ∪ ⋯ is then exactly the set {(i, a) ∣ a ∈ Xᵢ}, recovered from W by its fibers fiber W i = {a ∣ (i, a) ∈ W}. The "least family" description is equivalent to: W ∈ 𝒟^∞ iff every fiber is a neighbourhood and all but finitely many fibers equal Δ. (Closure under (2) and the base (1) generate exactly these, and no fewer, because (2) is the one-step "cons" and the cofinite-Δ condition is its iterate.)

The element-level payoff is the clean order-isomorphism

iterSeqEquiv : |𝒟^∞| ≃o (ℕ → |𝒟|)

(Scott's "one-one correspondence with infinite sequences"), from which 𝒟^∞ ≅ 𝒟 × 𝒟^∞ falls out by the shift (ℕ → E) ≃o E × (ℕ → E).

Everything is choice-free in spirit; the classical content is only what is inherited from the project's Element.ext/prodEquiv machinery, as elsewhere in §3.

Fibers of a set of (copy index, token) pairs.

def Domain.Neighborhood.fiber {α : Type u_1} (W : Set (ℕ × α)) (i : ℕ) : Set α

The i-th fiber of a set W ⊆ ℕ × α: the tokens appearing in copy i.

Equations

• Domain.Neighborhood.fiber W i = {a : α | (i, a) ∈ W}

@[simp]

theorem Domain.Neighborhood.mem_fiber {α : Type u_1} {W : Set (ℕ × α)} {i : ℕ} {a : α} : a ∈ fiber W i ↔ (i, a) ∈ W

theorem Domain.Neighborhood.fiber_mono {α : Type u_1} {W W' : Set (ℕ × α)} (h : W ⊆ W') (i : ℕ) : fiber W i ⊆ fiber W' i

theorem Domain.Neighborhood.fiber_inter {α : Type u_1} (W W' : Set (ℕ × α)) (i : ℕ) : fiber (W ∩ W') i = fiber W i ∩ fiber W' i

theorem Domain.Neighborhood.eq_of_fiber_eq {α : Type u_1} {W W' : Set (ℕ × α)} (h : ∀ (i : ℕ), fiber W i = fiber W' i) : W = W'

theorem Domain.Neighborhood.subset_of_fiber_subset {α : Type u_1} {W W' : Set (ℕ × α)} (h : ∀ (i : ℕ), fiber W i ⊆ fiber W' i) : W ⊆ W'

The pinning neighbourhood single n X (Scott's 1ⁿ0X, rest Δ).

def Domain.Neighborhood.single {α : Type u_1} (V : NeighborhoodSystem α) (n : ℕ) (X : Set α) : Set (ℕ × α)

The 𝒟^∞-neighbourhood pinning copy n to X and leaving all other copies at Δ: Scott's Δ^∞ ∩ (1ⁿ0X), i.e. the combination with Xₙ = X and Xₘ = Δ for m ≠ n.

Equations

• Domain.Neighborhood.single V n X = {p : ℕ × α | if p.1 = n then p.2 ∈ X else p.2 ∈ V.master}

@[simp]

theorem Domain.Neighborhood.fiber_single_self {α : Type u_1} {V : NeighborhoodSystem α} (n : ℕ) (X : Set α) : fiber (single V n X) n = X

theorem Domain.Neighborhood.fiber_single_ne {α : Type u_1} {V : NeighborhoodSystem α} {n i : ℕ} (h : i ≠ n) (X : Set α) : fiber (single V n X) i = V.master

theorem Domain.Neighborhood.single_mono {α : Type u_1} {V : NeighborhoodSystem α} {n : ℕ} {X X' : Set α} (h : X ⊆ X') : single V n X ⊆ single V n X'

theorem Domain.Neighborhood.single_inter {α : Type u_1} {V : NeighborhoodSystem α} {n : ℕ} (X X' : Set α) : single V n X ∩ single V n X' = single V n (X ∩ X')

The system 𝒟^∞.

def Domain.Neighborhood.iterSys {α : Type u_1} (V : NeighborhoodSystem α) : NeighborhoodSystem (ℕ × α)

Exercise 3.16 (Scott 1981, PRG-19). The infinite iterate 𝒟^∞ over Δ^∞ = ℕ × Δ: W ∈ 𝒟^∞ iff every fiber is a neighbourhood of 𝒟 and all but finitely many fibers equal Δ.

Equations

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

@[simp]

theorem Domain.Neighborhood.iterSys_master {α : Type u_1} {V : NeighborhoodSystem α} : (iterSys V).master = {p : ℕ × α | p.2 ∈ V.master}

theorem Domain.Neighborhood.fiber_iterSys_master {α : Type u_1} {V : NeighborhoodSystem α} (i : ℕ) : fiber (iterSys V).master i = V.master

@[simp]

theorem Domain.Neighborhood.mem_iterSys {α : Type u_1} {V : NeighborhoodSystem α} {W : Set (ℕ × α)} : (iterSys V).mem W ↔ (∀ (i : ℕ), V.mem (fiber W i)) ∧ ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → fiber W i = V.master

theorem Domain.Neighborhood.single_mem {α : Type u_1} {V : NeighborhoodSystem α} {n : ℕ} {X : Set α} (hX : V.mem X) : (iterSys V).mem (single V n X)

single V n X is a 𝒟^∞-neighbourhood whenever X ∈ 𝒟.

theorem Domain.Neighborhood.single_master {α : Type u_1} {V : NeighborhoodSystem α} (n : ℕ) : single V n V.master = (iterSys V).master

theorem Domain.Neighborhood.subset_single {α : Type u_1} {V : NeighborhoodSystem α} {W : Set (ℕ × α)} (hW : (iterSys V).mem W) (i : ℕ) : W ⊆ single V i (fiber W i)

Every 𝒟^∞-neighbourhood is contained in the pinning of its own i-th fiber.

theorem Domain.Neighborhood.interUpTo_subset_master {α : Type u_1} {V : NeighborhoodSystem α} (F : ℕ → Set (ℕ × α)) (N : ℕ) : (iterSys V).interUpTo F N ⊆ (iterSys V).master

theorem Domain.Neighborhood.reconstruct_subset {α : Type u_1} {V : NeighborhoodSystem α} {W : Set (ℕ × α)} (_hW : (iterSys V).mem W) {N : ℕ} (hN : ∀ (i : ℕ), N ≤ i → fiber W i = V.master) : (iterSys V).interUpTo (fun (i : ℕ) => single V i (fiber W i)) N ⊆ W

The finite intersection ⋂_{i<N} single i (fiber W i) reconstructs W from below, once N exceeds the cofinite-Δ bound of W.

Components and sequences.

def Domain.Neighborhood.component {α : Type u_1} {V : NeighborhoodSystem α} (z : (iterSys V).Element) (n : ℕ) : V.Element

The n-th component xₙ ∈ |𝒟| of a 𝒟^∞-element z (Scott's coordinate at copy n).

Equations

• Domain.Neighborhood.component z n = { mem := fun (X : Set α) => V.mem X ∧ z.mem (Domain.Neighborhood.single V n X), sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

@[simp]

theorem Domain.Neighborhood.mem_component {α : Type u_1} {V : NeighborhoodSystem α} {z : (iterSys V).Element} {n : ℕ} {X : Set α} : (component z n).mem X ↔ V.mem X ∧ z.mem (single V n X)

def Domain.Neighborhood.ofSeq {α : Type u_1} {V : NeighborhoodSystem α} (seq : ℕ → V.Element) : (iterSys V).Element

The 𝒟^∞-element determined by an infinite sequence ⟨xₙ⟩ of 𝒟-elements: the neighbourhoods W whose every fiber lies in the corresponding xᵢ.

Equations

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

@[simp]

theorem Domain.Neighborhood.mem_ofSeq {α : Type u_1} {V : NeighborhoodSystem α} {seq : ℕ → V.Element} {W : Set (ℕ × α)} : (ofSeq seq).mem W ↔ (iterSys V).mem W ∧ ∀ (i : ℕ), (seq i).mem (fiber W i)

theorem Domain.Neighborhood.ofSeq_mono {α : Type u_1} {V : NeighborhoodSystem α} {seq seq' : ℕ → V.Element} (h : ∀ (n : ℕ), seq n ≤ seq' n) : ofSeq seq ≤ ofSeq seq'

The two round-trips.

@[simp]

theorem Domain.Neighborhood.component_ofSeq {α : Type u_1} {V : NeighborhoodSystem α} (seq : ℕ → V.Element) (n : ℕ) : component (ofSeq seq) n = seq n

@[simp]

theorem Domain.Neighborhood.ofSeq_component {α : Type u_1} {V : NeighborhoodSystem α} (z : (iterSys V).Element) : (ofSeq fun (n : ℕ) => component z n) = z

theorem Domain.Neighborhood.le_of_component_le {α : Type u_1} {V : NeighborhoodSystem α} {z z' : (iterSys V).Element} (h : ∀ (n : ℕ), component z n ≤ component z' n) : z ≤ z'

z ⊑ z' is detected component-wise.

Scott's two conclusions.

def Domain.Neighborhood.iterSeqEquiv {α : Type u_1} (V : NeighborhoodSystem α) : (iterSys V).Element ≃o (ℕ → V.Element)

Exercise 3.16 (Scott 1981, PRG-19). The elements of |𝒟^∞| are in one-one, order-preserving correspondence with infinite sequences ⟨xₙ⟩ of elements of |𝒟|.

Equations

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

def Domain.Neighborhood.natShiftEquiv (E : Type u_2) [Preorder E] : (ℕ → E) ≃o E × (ℕ → E)

The shift order-isomorphism (ℕ → E) ≃o E × (ℕ → E), f ↦ (f 0, f ∘ succ).

Equations

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

def Domain.Neighborhood.iterProdIso {α : Type u_1} (V : NeighborhoodSystem α) : (iterSys V).Element ≃o (prod V (iterSys V)).Element

Exercise 3.16 (Scott 1981, PRG-19). The isomorphism |𝒟^∞| ≃o |𝒟 × 𝒟^∞|, obtained from the sequence correspondence and the shift.

Equations

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

theorem Domain.Neighborhood.iter_isomorphic {α : Type u_1} (V : NeighborhoodSystem α) : iterSys V ≅ᴰ prod V (iterSys V)

Exercise 3.16 (Scott 1981, PRG-19). 𝒟^∞ ≅ 𝒟 × 𝒟^∞.

The coordinate projections 𝒟^∞ → 𝒟 (used in Exercise 3.24(ii)).

def Domain.Neighborhood.projN {α : Type u_1} (V : NeighborhoodSystem α) (n : ℕ) : ApproximableMap (iterSys V) V

The n-th coordinate projection projN n : 𝒟^∞ → 𝒟, W (projN n) X ↔ fiber W n ⊆ X.

Equations

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

@[simp]

theorem Domain.Neighborhood.projN_rel {α : Type u_1} {V : NeighborhoodSystem α} {n : ℕ} {W : Set (ℕ × α)} {X : Set α} : (projN V n).rel W X ↔ (iterSys V).mem W ∧ V.mem X ∧ fiber W n ⊆ X

@[simp]

theorem Domain.Neighborhood.toElementMap_projN {α : Type u_1} {V : NeighborhoodSystem α} (z : (iterSys V).Element) (n : ℕ) : (projN V n).toElementMap z = component z n

projN n extracts the n-th component: projN n (z) = component z n.