Exercise 3.19 (Scott 1981, PRG-19, §3) — the sum functor `f + g` #

Given approximable mappings f : 𝒟₀ → 𝒟₀' and g : 𝒟₁ → 𝒟₁', Scott's Exercise 3.19 also asks for the sum mapping f + g : 𝒟₀ + 𝒟₁ → 𝒟₀' + 𝒟₁', characterized (equations (iii), (iv)) by

out₀ ∘ (f + g) ∘ in₀ = f, and
out₁ ∘ (f + g) ∘ in₁ = g.

We build f + g (sumMap) directly as a relation between sum-neighbourhoods: it routes the left copy 0X through f (to 0Y'), the right copy 1Y through g (to 1Y'), and sends everything to the master neighbourhood {Λ} ∪ 0Δ₀' ∪ 1Δ₁'. The disjointness of the two tagged copies (Exercise 3.18) is exactly what makes this a well-defined approximable mapping — a left input can never produce a right-tagged output, so there is no cross-contamination through g(⊥).

Scott also asks whether (iii), (iv) uniquely determine f + g: they do not, because the behaviour on the basepoint Λ (i.e. (f + g)(⊥)) is unconstrained; our choice sends Λ to Λ.

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

Structural extraction lemmas for sum-neighbourhoods. #

source

theorem Domain.Neighborhood.mem_subset_inj₀ {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {W : Set (Option (α ⊕ β))} {X : Set α} (hW : (sum V₀ V₁ h₀ h₁).mem W) (hsub : W ⊆ inj₀ X) :

∃ (X₂ : Set α), V₀.mem X₂ ∧ W = inj₀ X₂

A sum-neighbourhood contained in a left copy 0X is itself a left copy 0X₂ (the basepoint and the right copy are excluded, using non-emptiness).

source

theorem Domain.Neighborhood.mem_subset_inj₁ {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {W : Set (Option (α ⊕ β))} {Y : Set β} (hW : (sum V₀ V₁ h₀ h₁).mem W) (hsub : W ⊆ inj₁ Y) :

∃ (Y₂ : Set β), V₁.mem Y₂ ∧ W = inj₁ Y₂

A sum-neighbourhood contained in a right copy 1Y is itself a right copy 1Y₂.

source

theorem Domain.Neighborhood.eq_sumMaster_of_subset {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {W : Set (Option (α ⊕ β))} (hW : (sum V₀ V₁ h₀ h₁).mem W) (hsub : sumMaster V₀ V₁ ⊆ W) :

W = sumMaster V₀ V₁

A sum-neighbourhood that contains the master is the master.

source

theorem Domain.Neighborhood.not_inj₀_subset_inj₁ {α : Type u_1} {β : Type u_2} {X : Set α} {Y : Set β} (hX : X.Nonempty) (hsub : inj₀ X ⊆ inj₁ Y) :

False

A nonempty left copy is never contained in a right copy.

source

theorem Domain.Neighborhood.not_inj₁_subset_inj₀ {α : Type u_1} {β : Type u_2} {X : Set α} {Y : Set β} (hY : Y.Nonempty) (hsub : inj₁ Y ⊆ inj₀ X) :

False

A nonempty right copy is never contained in a left copy.

The sum mapping `f + g`. #

source

def Domain.Neighborhood.sumMap {α : Type u_1} {β : Type u_2} {α' : Type u_3} {β' : Type u_4} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {h₀ : ∀ (X : Set α), V₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set β), V₁.mem Y → Y.Nonempty} {h₀' : ∀ (X : Set α'), V₀'.mem X → X.Nonempty} {h₁' : ∀ (Y : Set β'), V₁'.mem Y → Y.Nonempty} (f : ApproximableMap V₀ V₀') (g : ApproximableMap V₁ V₁') :

ApproximableMap (sum V₀ V₁ h₀ h₁) (sum V₀' V₁' h₀' h₁')

Exercise 3.19 (Scott 1981, PRG-19). The sum mapping f + g : 𝒟₀ + 𝒟₁ → 𝒟₀' + 𝒟₁'. As a relation between sum-neighbourhoods, W (f+g) W' holds iff W' is the codomain master, or W = 0X with W' = 0Y' and X f Y', or W = 1Y with W' = 1Y' and Y g Y'.