Exercise 3.24 (Scott 1981, PRG-19, §3) — function-space isomorphisms

Scott asks to establish further isomorphisms. We formalize (i):

(𝒟₀ → (𝒟₁ × 𝒟₂)) ≅ (𝒟₀ → 𝒟₁) × (𝒟₀ → 𝒟₂).

The crux is the order-isomorphism on the approximable maps themselves, funProdEquiv : Hom(𝒟₀, 𝒟₁ × 𝒟₂) ≃o Hom(𝒟₀, 𝒟₁) × Hom(𝒟₀, 𝒟₂), given by h ↦ (p₀ ∘ h, p₁ ∘ h) with inverse ⟨a, b⟩ ↦ ⟨a, b⟩ (Definition 3.3's paired/proj, and the round-trips paired_proj / proj_comp_paired). Transporting through Theorem 3.10's funSpaceEquiv and Proposition 3.2's prodEquiv gives the domain isomorphism funProdIso.

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

def Domain.Neighborhood.funProdEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : ApproximableMap V₀ (prod V₁ V₂) ≃o ApproximableMap V₀ V₁ × ApproximableMap V₀ V₂

Exercise 3.24(i) (Scott 1981, PRG-19). The order-isomorphism on approximable maps Hom(𝒟₀, 𝒟₁ × 𝒟₂) ≃o Hom(𝒟₀, 𝒟₁) × Hom(𝒟₀, 𝒟₂), h ↦ (p₀ ∘ h, p₁ ∘ h).

Equations

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

def Domain.Neighborhood.funProdIso {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : (funSpace V₀ (prod V₁ V₂)).Element ≃o (prod (funSpace V₀ V₁) (funSpace V₀ V₂)).Element

Exercise 3.24(i) (Scott 1981, PRG-19). The domain isomorphism |𝒟₀ → (𝒟₁ × 𝒟₂)| ≃o |(𝒟₀ → 𝒟₁) × (𝒟₀ → 𝒟₂)|.

Equations

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

theorem Domain.Neighborhood.funProd_isomorphic {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} : funSpace V₀ (prod V₁ V₂) ≅ᴰ prod (funSpace V₀ V₁) (funSpace V₀ V₂)

Exercise 3.24(i). (𝒟₀ → (𝒟₁ × 𝒟₂)) ≅ (𝒟₀ → 𝒟₁) × (𝒟₀ → 𝒟₂).