Exercise 3.18 (Scott 1981, PRG-19, §3) — the sum (coproduct) system

Scott's sum of 𝒟₀ (over Δ₀) and 𝒟₁ (over Δ₁), assuming no neighbourhood is empty:

𝒟₀ + 𝒟₁ = {{Λ} ∪ 0Δ₀ ∪ 1Δ₁} ∪ {0X ∣ X ∈ 𝒟₀} ∪ {1Y ∣ Y ∈ 𝒟₁},

a neighbourhood system over {Λ} ∪ 0Δ₀ ∪ 1Δ₁. We model the tokens as Option (α ⊕ β): Λ = none, 0a = some (inl a), 1b = some (inr b); then 0X = il '' X and 1Y = ir '' Y.

The non-emptiness assumption (h₀, h₁) is exactly what makes the system closed under intersection: the two tagged copies are disjoint (inj₀ X ∩ inj₁ Y = ∅), so a cross pair 0X, 1Y is inconsistent (no non-empty neighbourhood lies in ∅), and same-tag intersections reduce to those of the factors.

We then build the injections inMapᵢ : 𝒟ᵢ → 𝒟₀ + 𝒟₁ and projections `outMapᵢ : 𝒟₀

• 𝒟₁ → 𝒟ᵢ, and prove outMapᵢ ∘ inMapᵢ = I_{𝒟ᵢ}`. (The non-emptiness assumption is what makes the system a neighbourhood system; the section/retraction identities hold for the resulting maps.)

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

def Domain.Neighborhood.il {α : Type u_1} {β : Type u_2} (a : α) : Option (α ⊕ β)

Left tag 0a = some (inl a).

Equations

• Domain.Neighborhood.il a = some (Sum.inl a)

def Domain.Neighborhood.ir {α : Type u_1} {β : Type u_2} (b : β) : Option (α ⊕ β)

Right tag 1b = some (inr b).

Equations

• Domain.Neighborhood.ir b = some (Sum.inr b)

def Domain.Neighborhood.inj₀ {α : Type u_1} {β : Type u_2} (X : Set α) : Set (Option (α ⊕ β))

The tagged left copy 0X = {some (inl a) ∣ a ∈ X}.

Equations

• Domain.Neighborhood.inj₀ X = Domain.Neighborhood.il '' X

def Domain.Neighborhood.inj₁ {α : Type u_1} {β : Type u_2} (Y : Set β) : Set (Option (α ⊕ β))

The tagged right copy 1Y = {some (inr b) ∣ b ∈ Y}.

Equations

• Domain.Neighborhood.inj₁ Y = Domain.Neighborhood.ir '' Y

@[simp]

theorem Domain.Neighborhood.il_mem_inj₀ {α : Type u_1} {β : Type u_2} {X : Set α} {a : α} : il a ∈ inj₀ X ↔ a ∈ X

@[simp]

theorem Domain.Neighborhood.ir_mem_inj₀ {α : Type u_1} {β : Type u_2} {X : Set α} {b : β} : ¬ir b ∈ inj₀ X

@[simp]

theorem Domain.Neighborhood.none_mem_inj₀ {α : Type u_1} {β : Type u_2} {X : Set α} : ¬none ∈ inj₀ X

@[simp]

theorem Domain.Neighborhood.ir_mem_inj₁ {α : Type u_1} {β : Type u_2} {Y : Set β} {b : β} : ir b ∈ inj₁ Y ↔ b ∈ Y

@[simp]

theorem Domain.Neighborhood.il_mem_inj₁ {α : Type u_1} {β : Type u_2} {Y : Set β} {a : α} : ¬il a ∈ inj₁ Y

@[simp]

theorem Domain.Neighborhood.none_mem_inj₁ {α : Type u_1} {β : Type u_2} {Y : Set β} : ¬none ∈ inj₁ Y

theorem Domain.Neighborhood.inj₀_inter {α : Type u_1} {β : Type u_2} (X X' : Set α) : inj₀ X ∩ inj₀ X' = inj₀ (X ∩ X')

theorem Domain.Neighborhood.inj₁_inter {α : Type u_1} {β : Type u_2} (Y Y' : Set β) : inj₁ Y ∩ inj₁ Y' = inj₁ (Y ∩ Y')

theorem Domain.Neighborhood.inj₀_inter_inj₁ {α : Type u_1} {β : Type u_2} (X : Set α) (Y : Set β) : inj₀ X ∩ inj₁ Y = ∅

theorem Domain.Neighborhood.inj₀_nonempty {α : Type u_1} {β : Type u_2} {X : Set α} (hX : X.Nonempty) : (inj₀ X).Nonempty

theorem Domain.Neighborhood.inj₁_nonempty {α : Type u_1} {β : Type u_2} {Y : Set β} (hY : Y.Nonempty) : (inj₁ Y).Nonempty

theorem Domain.Neighborhood.inj₀_subset_inj₀ {α : Type u_1} {β : Type u_2} {X X' : Set α} : inj₀ X ⊆ inj₀ X' ↔ X ⊆ X'

theorem Domain.Neighborhood.inj₁_subset_inj₁ {α : Type u_1} {β : Type u_2} {Y Y' : Set β} : inj₁ Y ⊆ inj₁ Y' ↔ Y ⊆ Y'

theorem Domain.Neighborhood.inj₀_injective {α : Type u_1} {β : Type u_2} {X X' : Set α} (h : inj₀ X = inj₀ X') : X = X'

theorem Domain.Neighborhood.inj₁_injective {α : Type u_1} {β : Type u_2} {Y Y' : Set β} (h : inj₁ Y = inj₁ Y') : Y = Y'

def Domain.Neighborhood.sumMaster {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : Set (Option (α ⊕ β))

The master neighbourhood of the sum: {Λ} ∪ 0Δ₀ ∪ 1Δ₁.

Equations

• Domain.Neighborhood.sumMaster V₀ V₁ = insert none (Domain.Neighborhood.inj₀ V₀.master ∪ Domain.Neighborhood.inj₁ V₁.master)

@[simp]

theorem Domain.Neighborhood.none_mem_sumMaster {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : none ∈ sumMaster V₀ V₁

theorem Domain.Neighborhood.inj₀_subset_sumMaster {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} (hX : V₀.mem X) : inj₀ X ⊆ sumMaster V₀ V₁

theorem Domain.Neighborhood.inj₁_subset_sumMaster {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set β} (hY : V₁.mem Y) : inj₁ Y ⊆ sumMaster V₀ V₁

theorem Domain.Neighborhood.sumMaster_inter_inj₀ {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} (hX : V₀.mem X) : sumMaster V₀ V₁ ∩ inj₀ X = inj₀ X

theorem Domain.Neighborhood.sumMaster_inter_inj₁ {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set β} (hY : V₁.mem Y) : sumMaster V₀ V₁ ∩ inj₁ Y = inj₁ Y

def Domain.Neighborhood.sum {α : 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) : NeighborhoodSystem (Option (α ⊕ β))

Exercise 3.18 (Scott 1981, PRG-19). The sum system 𝒟₀ + 𝒟₁ over {Λ} ∪ 0Δ₀ ∪ 1Δ₁, under the standing assumption that no neighbourhood of 𝒟₀ or 𝒟₁ is empty.

Equations

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

The injections inᵢ and projections outᵢ.

theorem Domain.Neighborhood.il_injective {α : Type u_1} {β : Type u_2} : Function.Injective il

theorem Domain.Neighborhood.ir_injective {α : Type u_1} {β : Type u_2} : Function.Injective ir

@[simp]

theorem Domain.Neighborhood.il_preimage_inj₀ {α : Type u_1} {β : Type u_2} (X : Set α) : il ⁻¹' inj₀ X = X

@[simp]

theorem Domain.Neighborhood.ir_preimage_inj₁ {α : Type u_1} {β : Type u_2} (Y : Set β) : ir ⁻¹' inj₁ Y = Y

def Domain.Neighborhood.leftPart {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (W : Set (Option (α ⊕ β))) : Set α

The left content leftPart W ⊆ Δ₀ of a sum-neighbourhood W: the 0-tagged tokens of W, plus all of Δ₀ whenever W reaches into the right copy or the basepoint (so non-left neighbourhoods contribute only Δ₀, i.e. project to ⊥). This is a genuine (choice-free) function of W.

Equations

• Domain.Neighborhood.leftPart V₀ W = Domain.Neighborhood.il ⁻¹' W ∪ {a : α | a ∈ V₀.master ∧ ((∃ (b : β), Domain.Neighborhood.ir b ∈ W) ∨ none ∈ W)}

def Domain.Neighborhood.rightPart {α : Type u_1} {β : Type u_2} (V₁ : NeighborhoodSystem β) (W : Set (Option (α ⊕ β))) : Set β

The right content rightPart W ⊆ Δ₁, symmetric to leftPart.

Equations

• Domain.Neighborhood.rightPart V₁ W = Domain.Neighborhood.ir ⁻¹' W ∪ {b : β | b ∈ V₁.master ∧ ((∃ (a : α), Domain.Neighborhood.il a ∈ W) ∨ none ∈ W)}

@[simp]

theorem Domain.Neighborhood.mem_leftPart {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {W : Set (Option (α ⊕ β))} {a : α} : a ∈ leftPart V₀ W ↔ il a ∈ W ∨ a ∈ V₀.master ∧ ((∃ (b : β), ir b ∈ W) ∨ none ∈ W)

@[simp]

theorem Domain.Neighborhood.mem_rightPart {α : Type u_1} {β : Type u_2} {V₁ : NeighborhoodSystem β} {W : Set (Option (α ⊕ β))} {b : β} : b ∈ rightPart V₁ W ↔ ir b ∈ W ∨ b ∈ V₁.master ∧ ((∃ (a : α), il a ∈ W) ∨ none ∈ W)

theorem Domain.Neighborhood.leftPart_mono {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) {W W' : Set (Option (α ⊕ β))} (h : W ⊆ W') : leftPart V₀ W ⊆ leftPart V₀ W'

theorem Domain.Neighborhood.rightPart_mono {α : Type u_1} {β : Type u_2} (V₁ : NeighborhoodSystem β) {W W' : Set (Option (α ⊕ β))} (h : W ⊆ W') : rightPart V₁ W ⊆ rightPart V₁ W'

@[simp]

theorem Domain.Neighborhood.leftPart_inj₀ {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (X : Set α) : leftPart V₀ (inj₀ X) = X

@[simp]

theorem Domain.Neighborhood.rightPart_inj₁ {α : Type u_1} {β : Type u_2} (V₁ : NeighborhoodSystem β) (Y : Set β) : rightPart V₁ (inj₁ Y) = Y

theorem Domain.Neighborhood.leftPart_sumMaster {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : leftPart V₀ (sumMaster V₀ V₁) = V₀.master

theorem Domain.Neighborhood.leftPart_inj₁ {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) {Y : Set β} (hY : Y.Nonempty) : leftPart V₀ (inj₁ Y) = V₀.master

theorem Domain.Neighborhood.rightPart_sumMaster {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : rightPart V₁ (sumMaster V₀ V₁) = V₁.master

theorem Domain.Neighborhood.rightPart_inj₀ {α : Type u_1} {β : Type u_2} (V₁ : NeighborhoodSystem β) {X : Set α} (hX : X.Nonempty) : rightPart V₁ (inj₀ X) = V₁.master

theorem Domain.Neighborhood.leftPart_mem {α : 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) : V₀.mem (leftPart V₀ W)

theorem Domain.Neighborhood.rightPart_mem {α : 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) : V₁.mem (rightPart V₁ W)

def Domain.Neighborhood.inMap₀ {α : 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} : ApproximableMap V₀ (sum V₀ V₁ h₀ h₁)

Exercise 3.18 (Scott 1981, PRG-19). The left injection in₀ : 𝒟₀ → 𝒟₀ + 𝒟₁, X (in₀) W ↔ 0X ⊆ W.

Equations

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

def Domain.Neighborhood.inMap₁ {α : 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} : ApproximableMap V₁ (sum V₀ V₁ h₀ h₁)

Exercise 3.18 (Scott 1981, PRG-19). The right injection in₁ : 𝒟₁ → 𝒟₀ + 𝒟₁.

Equations

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

def Domain.Neighborhood.outMap₀ {α : 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} : ApproximableMap (sum V₀ V₁ h₀ h₁) V₀

Exercise 3.18 (Scott 1981, PRG-19). The left projection out₀ : 𝒟₀ + 𝒟₁ → 𝒟₀, W (out₀) X ↔ leftPart W ⊆ X (right/basepoint neighbourhoods relate only to Δ₀).

Equations

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

def Domain.Neighborhood.outMap₁ {α : 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} : ApproximableMap (sum V₀ V₁ h₀ h₁) V₁

Exercise 3.18 (Scott 1981, PRG-19). The right projection out₁ : 𝒟₀ + 𝒟₁ → 𝒟₁.

Equations

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

theorem Domain.Neighborhood.outMap₀_comp_inMap₀ {α : 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} : outMap₀.comp inMap₀ = ApproximableMap.idMap V₀

Exercise 3.18 (Scott 1981, PRG-19). out₀ ∘ in₀ = I_{𝒟₀}.

theorem Domain.Neighborhood.outMap₁_comp_inMap₁ {α : 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} : outMap₁.comp inMap₁ = ApproximableMap.idMap V₁

Exercise 3.18 (Scott 1981, PRG-19). out₁ ∘ in₁ = I_{𝒟₁}.