Exercise 3.24(iii)(iv) (Scott 1981, PRG-19, §3) — sum/product "isomorphisms"

that are only maps

Scott's list of isomorphisms ends with two entries and the caveat "If some of the above are not true, perhaps at least some mapping relationships can be established." Parts (iii) and (iv) are exactly those: with Scott's separated sum 𝒟₀ + 𝒟₁ (a fresh bottom Λ glued below two disjoint copies), neither

• (iii) 𝒟₀ × (𝒟₁ + 𝒟₂) ≅ (𝒟₀ × 𝒟₁) + (𝒟₀ × 𝒟₂), nor
• (iv) (𝒟₀ + 𝒟₁) → 𝒟₂ ≅ (𝒟₀ → 𝒟₂) × (𝒟₁ → 𝒟₂)

holds as a genuine isomorphism. (For (iv): inᵢ(⊥) lies strictly above the sum's bottom, so a map h is not recoverable from h ∘ in₀ and h ∘ in₁ — the value h(⊥) is free. For (iii): the left side has, for each x ∈ |𝒟₀|, an element ⟨x, ⊥⟩ incomparable to both cones, which the right side lacks.)

What is true are the canonical mapping relationships:

• (iv) the copairing [a, b] : 𝒟₀ + 𝒟₁ → 𝒟₂ with [a,b] ∘ inᵢ = a, b (copair, copair_comp_inMap₀/₁), exhibiting (𝒟₀→𝒟₂) × (𝒟₁→𝒟₂) as a retract of (𝒟₀+𝒟₁) → 𝒟₂ (copairProj_copair); and
• (iii) the canonical distribution map (𝒟₀ × 𝒟₁) + (𝒟₀ × 𝒟₂) → 𝒟₀ × (𝒟₁ + 𝒟₂) (distribMap), inᵢ⟨x, u⟩ ↦ ⟨x, inᵢ u⟩.

The development re-uses Exercise 3.18's injections/projections and the structural extraction lemmas of Exercise 3.19.

(iv) — the copairing [a, b] : 𝒟₀ + 𝒟₁ → 𝒟₂.

def Domain.Neighborhood.copair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (a : ApproximableMap V₀ V₂) (b : ApproximableMap V₁ V₂) : ApproximableMap (sum V₀ V₁ h₀ h₁) V₂

Exercise 3.24(iv) (Scott 1981, PRG-19). The copairing [a, b] : 𝒟₀ + 𝒟₁ → 𝒟₂: a left copy 0X is routed through a, a right copy 1Y through b, and the basepoint Λ to ⊥ (so Λ relates only to Δ₂).

Equations

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

@[simp]

theorem Domain.Neighborhood.copair_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {a : ApproximableMap V₀ V₂} {b : ApproximableMap V₁ V₂} {W : Set (Option (α ⊕ β))} {Z : Set γ} : (copair a b).rel W Z ↔ (sum V₀ V₁ h₀ h₁).mem W ∧ V₂.mem Z ∧ (Z = V₂.master ∨ (∃ (X : Set α), W = inj₀ X ∧ a.rel X Z) ∨ ∃ (Y : Set β), W = inj₁ Y ∧ b.rel Y Z)

theorem Domain.Neighborhood.copair_comp_inMap₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (a : ApproximableMap V₀ V₂) (b : ApproximableMap V₁ V₂) : (copair a b).comp inMap₀ = a

Exercise 3.24(iv) (Scott 1981, PRG-19). [a, b] ∘ in₀ = a.

theorem Domain.Neighborhood.copair_comp_inMap₁ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (a : ApproximableMap V₀ V₂) (b : ApproximableMap V₁ V₂) : (copair a b).comp inMap₁ = b

Exercise 3.24(iv) (Scott 1981, PRG-19). [a, b] ∘ in₁ = b.

def Domain.Neighborhood.copairProj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (h : ApproximableMap (sum V₀ V₁ h₀ h₁) V₂) : ApproximableMap V₀ V₂ × ApproximableMap V₁ V₂

The canonical comparison Hom(𝒟₀+𝒟₁, 𝒟₂) → Hom(𝒟₀,𝒟₂) × Hom(𝒟₁,𝒟₂), h ↦ (h∘in₀, h∘in₁).

Equations

• Domain.Neighborhood.copairProj h = (h.comp Domain.Neighborhood.inMap₀, h.comp Domain.Neighborhood.inMap₁)

theorem Domain.Neighborhood.copairProj_copair {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} (a : ApproximableMap V₀ V₂) (b : ApproximableMap V₁ V₂) : copairProj (copair a b) = (a, b)

Exercise 3.24(iv) (Scott 1981, PRG-19). (𝒟₀→𝒟₂) × (𝒟₁→𝒟₂) is a retract of (𝒟₀+𝒟₁) → 𝒟₂: the copairing is a section of h ↦ (h∘in₀, h∘in₁). (It is not an isomorphism: the value of a map on the basepoint Λ is not recoverable from its restrictions to the two copies.)

(iii) — the canonical distribution map.

theorem Domain.Neighborhood.prod_mem_nonempty {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (hn₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty) (_hn₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty) (W : Set (α ⊕ β)) (hW : (prod V₀ V₁).mem W) : W.Nonempty

A product neighbourhood over non-empty factors is non-empty.

def Domain.Neighborhood.distribMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (hn₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty) (hn₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty) (hn₂ : ∀ (Z : Set γ), V₂.mem Z → Z.Nonempty) : ApproximableMap (sum (prod V₀ V₁) (prod V₀ V₂) ⋯ ⋯) (prod V₀ (sum V₁ V₂ hn₁ hn₂))

Exercise 3.24(iii) (Scott 1981, PRG-19). The canonical distribution approximable map (𝒟₀ × 𝒟₁) + (𝒟₀ × 𝒟₂) → 𝒟₀ × (𝒟₁ + 𝒟₂), inᵢ⟨x, u⟩ ↦ ⟨x, inᵢ u⟩. (This direction always exists; the reverse map / isomorphism does not, since the left side has an element ⟨x, ⊥⟩ for each x.)

Equations

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