Exercise 3.24(ii) (Scott 1981, PRG-19, §3) — (𝒟₀ → 𝒟₁^∞) ≅ (𝒟₀ → 𝒟₁)^∞

Using the infinite iterate 𝒟^∞ of Exercise 3.16 and the function space (𝒟₀ → 𝒟₁) of Definition 3.8 / Theorem 3.10, we establish Scott's isomorphism (ii):

(𝒟₀ → 𝒟₁^∞) ≅ (𝒟₀ → 𝒟₁)^∞.

The crux is the order-isomorphism on approximable maps

funIterEquiv : Hom(𝒟₀, 𝒟₁^∞) ≃o (ℕ → Hom(𝒟₀, 𝒟₁)),

f ↦ (n ↦ projₙ ∘ f) with inverse the "infinite pairing" g ↦ mapOfSeq g, whose value is the sequence mapOfSeq g (x) = ⟨gₙ(x)⟩ₙ. Transporting through Theorem 3.10's funSpaceEquiv (twice, the second time pointwise via OrderIso.piCongrRight) and Exercise 3.16's iterSeqEquiv yields the domain isomorphism.

Everything is choice-free in spirit; the only classical input is inherited from Element.ext, funSpaceEquiv and the choose in the ∃/∀-swap lemma, exactly as elsewhere in §3.

def Domain.Neighborhood.mapOfSeq {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (g : ℕ → ApproximableMap V₀ V₁) : ApproximableMap V₀ (iterSys V₁)

The "infinite pairing" map 𝒟₀ → 𝒟₁^∞ of a sequence g : ℕ → Hom(𝒟₀, 𝒟₁): X (mapOfSeq g) W ↔ X ∈ 𝒟₀, W ∈ 𝒟₁^∞, and X gᵢ (fiber W i) for all i.

Equations

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

theorem Domain.Neighborhood.exists_forall_swap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {x : V₀.Element} {W : Set (ℕ × β)} {g : ℕ → ApproximableMap V₀ V₁} (hW : (iterSys V₁).mem W) : (∃ (X : Set α), x.mem X ∧ ∀ (i : ℕ), (g i).rel X (fiber W i)) ↔ ∀ (i : ℕ), ∃ (X : Set α), x.mem X ∧ (g i).rel X (fiber W i)

The ∃/∀-swap behind mapOfSeq: a single input neighbourhood X ∈ x works for all coordinates iff each coordinate has its own (intersect the finitely many non-trivial ones).

theorem Domain.Neighborhood.toElementMap_mapOfSeq {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (g : ℕ → ApproximableMap V₀ V₁) (x : V₀.Element) : (mapOfSeq g).toElementMap x = ofSeq fun (i : ℕ) => (g i).toElementMap x

The value of mapOfSeq g is the sequence of values ⟨gᵢ(x)⟩.

theorem Domain.Neighborhood.projComp_mono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f f' : ApproximableMap V₀ (iterSys V₁)} (h : f ≤ f') (n : ℕ) : (projN V₁ n).comp f ≤ (projN V₁ n).comp f'

projₙ ∘ f is monotone in f.

theorem Domain.Neighborhood.le_of_projComp_le {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f f' : ApproximableMap V₀ (iterSys V₁)} (h : ∀ (n : ℕ), (projN V₁ n).comp f ≤ (projN V₁ n).comp f') : f ≤ f'

A map 𝒟₀ → 𝒟₁^∞ is detected coordinate-wise: f ⊑ f' iff projₙ ∘ f ⊑ projₙ ∘ f' for all n.

def Domain.Neighborhood.funIterEquiv {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : ApproximableMap V₀ (iterSys V₁) ≃o (ℕ → ApproximableMap V₀ V₁)

Exercise 3.24(ii) (Scott 1981, PRG-19). The order-isomorphism on approximable maps Hom(𝒟₀, 𝒟₁^∞) ≃o (ℕ → Hom(𝒟₀, 𝒟₁)), f ↦ (n ↦ projₙ ∘ f).

Equations

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

def Domain.Neighborhood.piCongrOrderIso {ι : Type u_3} {A : ι → Type u_4} {B : ι → Type u_5} [(i : ι) → Preorder (A i)] [(i : ι) → Preorder (B i)] (e : (i : ι) → A i ≃o B i) : ((i : ι) → A i) ≃o ((i : ι) → B i)

A pointwise family of order-isomorphisms induces one on the dependent product.

Equations

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

def Domain.Neighborhood.funIterIso {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : (funSpace V₀ (iterSys V₁)).Element ≃o (iterSys (funSpace V₀ V₁)).Element

Exercise 3.24(ii) (Scott 1981, PRG-19). The domain isomorphism |𝒟₀ → 𝒟₁^∞| ≃o |(𝒟₀ → 𝒟₁)^∞|.

Equations

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

theorem Domain.Neighborhood.funIter_isomorphic {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : funSpace V₀ (iterSys V₁) ≅ᴰ iterSys (funSpace V₀ V₁)

Exercise 3.24(ii). (𝒟₀ → 𝒟₁^∞) ≅ (𝒟₀ → 𝒟₁)^∞.