Exercise 5.10 (Scott 1981, PRG-19, §5) — the smash product and the strict

function space

Suppose 𝒟₀ and 𝒟₁ are neighbourhood systems over disjoint sets Δ₀ and Δ₁. Define the smash product 𝒟₀ ⊗ 𝒟₁ with neighbourhoods {Δ₀ ∪ Δ₁} ∪ {X ∪ Y ∣ X ∈ 𝒟₀ ∖ {Δ₀} and Y ∈ 𝒟₁ ∖ {Δ₁}}. Show that this is a neighbourhood system. Define (𝒟₀ →⊥ 𝒟₁) so that |𝒟₀ →⊥ 𝒟₁| consists exactly of the strict functions. By introducing appropriate combinators, show that (𝒟₀ →⊥ (𝒟₁ →⊥ 𝒟₂)) and ((𝒟₀ ⊗ 𝒟₁) →⊥ 𝒟₂) are isomorphic.

We model the disjoint union of token sets by the sum type α ⊕ β, exactly as for the ordinary product (Domain/Neighborhood/Product.lean), reusing prodNbhd X Y = Sum.inl '' X ∪ Sum.inr '' Y and its algebra (prodNbhd_inter, prodNbhd_subset_iff, prodNbhd_injective).

This file is organised as follows.

• The smash product smash V₀ V₁ (§ smash): a genuine neighbourhood system. The neighbourhoods are the master Δ₀ ∪ Δ₁ together with the proper product neighbourhoods X ∪ Y whose factors are both proper (X ≠ Δ₀, Y ≠ Δ₁). Closure under consistent intersection is the new content: the consistency witness rules out the degenerate cases, and a proper factor stays proper under intersection.
• The smash collapses bottoms (§ elements): the element smashPair x y (the strict pairing) and the order-isomorphism showing |𝒟₀ ⊗ 𝒟₁| is the smash of the pointed domains — every element is either ⊥ or a pair ⟨x, y⟩ of non-⊥ elements.
• The strict function space strictFun V₀ V₁ (§ strict): a neighbourhood system whose elements are exactly the strict approximable maps (IsStrict f, i.e. f(⊥) = ⊥). We realise it as the function space generated only by step neighbourhoods [X, Y] with proper input X, and prove the representation strictFunEquiv : |𝒟₀ →⊥ 𝒟₁| ≃o {f ∣ IsStrict f}.
• The adjunction (§ iso): the "appropriate combinators" Scott asks for — a strict curry smashCurryMap and strict uncurry smashUncurryMap — assembled into the order-isomorphism smashCurryEquiv : ((𝒟₀ ⊗ 𝒟₁) →⊥ 𝒟₂) ≃o (𝒟₀ →⊥ (𝒟₁ →⊥ 𝒟₂)). The decisive computation is section_uncurry_rel: g(⟨x, y⟩⊗) = curry⊥(g)(x)(y), with the boundary (a master factor) handled by strictness — exactly the bottom-gluing the smash performs.

The data (smash, strictFun, smashCurryMap, smashUncurryMap) and the representation strictFunEquiv are choice-free (#print axioms ⊆ {propext, Quot.sound}); Classical.choice enters only the smashCurryEquiv proof, through the genuinely-classical X = Δ₀? / Y = Δ₁? boundary case analysis.

The smash product 𝒟₀ ⊗ 𝒟₁.

def Domain.Neighborhood.Exercise510.SmashProper {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (W : Set (α ⊕ β)) : Prop

A proper product neighbourhood of the smash: X ∪ Y with X ∈ 𝒟₀ ∖ {Δ₀} and Y ∈ 𝒟₁ ∖ {Δ₁} (both factors strictly below their masters).

Equations

• Domain.Neighborhood.Exercise510.SmashProper V₀ V₁ W = ∃ (X : Set α) (Y : Set β), V₀.mem X ∧ X ≠ V₀.master ∧ V₁.mem Y ∧ Y ≠ V₁.master ∧ W = Domain.Neighborhood.prodNbhd X Y

theorem Domain.Neighborhood.Exercise510.inter_ne_master_left {α : Type u_1} {V₀ : NeighborhoodSystem α} {X X' : Set α} (hX : V₀.mem X) (hXne : X ≠ V₀.master) : X ∩ X' ≠ V₀.master

A neighbourhood that is ⊆ Δ₀ and equals Δ₀ exactly when it contains Δ₀. A proper factor X ≠ Δ₀ stays proper after intersecting with anything: X ∩ X' ≠ Δ₀.

theorem Domain.Neighborhood.Exercise510.inter_ne_master_right {β : Type u_2} {V₁ : NeighborhoodSystem β} {Y Y' : Set β} (hY : V₁.mem Y) (hYne : Y ≠ V₁.master) : Y ∩ Y' ≠ V₁.master

def Domain.Neighborhood.Exercise510.smash {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : NeighborhoodSystem (α ⊕ β)

Exercise 5.10 (Scott 1981, PRG-19) — the smash product 𝒟₀ ⊗ 𝒟₁. Neighbourhoods are the master Δ₀ ∪ Δ₁ together with the proper product neighbourhoods X ∪ Y (both factors proper).

This is a neighbourhood system. Condition (i) is the master clause. Condition (ii) is the new content: given two smash neighbourhoods with a consistency witness Z,

• if either is the master, the intersection collapses to the other (since X ⊆ Δ₀, Y ⊆ Δ₁);
• if both are proper, Z cannot be the master (that would force a factor to be Δ₀/Δ₁), so Z is a proper U ∪ V; U ⊆ X ∩ X' and V ⊆ Y ∩ Y' then witness X ∩ X' ∈ 𝒟₀, Y ∩ Y' ∈ 𝒟₁, both still proper (inter_ne_master_*).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise510.smash_master {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : (smash V₀ V₁).master = prodNbhd V₀.master V₁.master

theorem Domain.Neighborhood.Exercise510.smash_mem_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (α ⊕ β)} : (smash V₀ V₁).mem W ↔ W = prodNbhd V₀.master V₁.master ∨ SmashProper V₀ V₁ W

theorem Domain.Neighborhood.Exercise510.smash_mem_proper {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} {Y : Set β} (hX : V₀.mem X) (hXne : X ≠ V₀.master) (hY : V₁.mem Y) (hYne : Y ≠ V₁.master) : (smash V₀ V₁).mem (prodNbhd X Y)

A proper product neighbourhood is a neighbourhood of the smash.

theorem Domain.Neighborhood.Exercise510.smash_mem_bot {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (α ⊕ β)} : (smash V₀ V₁).bot.mem W ↔ W = prodNbhd V₀.master V₁.master

⊥ of the smash is exactly {Δ₀ ∪ Δ₁}.

The smash collapses bottoms: the strict pairing ⟨x, y⟩⊗.

The smash identifies all elements that have a ⊥ in either coordinate. We realise this by the strict pairing smashPair x y: when both x, y are non-⊥ it is the genuine pair ⟨x, y⟩, and when either is ⊥ it collapses to ⊥ (smashPair_eq_bot_iff). Every element of |𝒟₀ ⊗ 𝒟₁| arises this way.

def Domain.Neighborhood.Exercise510.smashPair {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (x : V₀.Element) (y : V₁.Element) : (smash V₀ V₁).Element

The strict pairing ⟨x, y⟩⊗: the filter generated by the proper product neighbourhoods X ∪ Y with X ∈ x ∖ {Δ₀}, Y ∈ y ∖ {Δ₁} (plus the master). When either x or y is ⊥ (i.e. contains only its master), this collapses to ⊥.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise510.mem_smashPair {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {x : V₀.Element} {y : V₁.Element} {W : Set (α ⊕ β)} : (smashPair x y).mem W ↔ W = prodNbhd V₀.master V₁.master ∨ ∃ (X : Set α) (Y : Set β), x.mem X ∧ X ≠ V₀.master ∧ y.mem Y ∧ Y ≠ V₁.master ∧ W = prodNbhd X Y

theorem Domain.Neighborhood.Exercise510.exists_proper_of_ne_bot {α : Type u_1} {V₀ : NeighborhoodSystem α} {x : V₀.Element} (hx : x ≠ V₀.bot) : ∃ (X : Set α), x.mem X ∧ X ≠ V₀.master

An element is ⊥ iff every neighbourhood it contains is the master: x ≠ ⊥ exactly when x contains a proper neighbourhood.

theorem Domain.Neighborhood.Exercise510.eq_bot_of_no_proper {α : Type u_1} {V₀ : NeighborhoodSystem α} {x : V₀.Element} (hx : ∀ (X : Set α), x.mem X → X = V₀.master) : x = V₀.bot

theorem Domain.Neighborhood.Exercise510.smashPair_eq_bot_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {x : V₀.Element} {y : V₁.Element} : smashPair x y = (smash V₀ V₁).bot ↔ x = V₀.bot ∨ y = V₁.bot

The strict pairing is ⊥ iff one of the components is ⊥: the smash glues (⊥, y) and (x, ⊥) to a single bottom.

theorem Domain.Neighborhood.Exercise510.smashPair_mono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {x x' : V₀.Element} {y y' : V₁.Element} (hx : x ≤ x') (hy : y ≤ y') : smashPair x y ≤ smashPair x' y'

The strict pairing is monotone in both arguments.

theorem Domain.Neighborhood.Exercise510.principal_master_eq_bot {α : Type u_1} {V₀ : NeighborhoodSystem α} {X : Set α} (hX : V₀.mem X) (hXm : X = V₀.master) : V₀.principal hX = V₀.bot

The principal filter of the master is ⊥.

theorem Domain.Neighborhood.Exercise510.smashPair_bot_left {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (y : V₁.Element) : smashPair V₀.bot y = (smash V₀ V₁).bot

A ⊥ left factor collapses the strict pairing to ⊥ (choice-free).

theorem Domain.Neighborhood.Exercise510.smashPair_bot_right {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (x : V₀.Element) : smashPair x V₁.bot = (smash V₀ V₁).bot

A ⊥ right factor collapses the strict pairing to ⊥ (choice-free).

The strict function space (𝒟₀ →⊥ 𝒟₁).

A map f : 𝒟₀ → 𝒟₁ is strict when f(⊥) = ⊥. In relational terms (since f(⊥) is the filter {Y ∣ Δ₀ f Y}), this says f relates the master input Δ₀ only to the master output Δ₁: Δ₀ f Y ⟹ Y = Δ₁.

We realise (𝒟₀ →⊥ 𝒟₁) as the function space whose tokens are the strict approximable maps and whose neighbourhoods are the non-empty finite intersections of step sets [X, Y] = {f ∣ X f Y}. The crucial point — making |𝒟₀ →⊥ 𝒟₁| consist exactly of the strict functions — is automatic: a step [Δ₀, Y] with Y ≠ Δ₁ contains no strict map, so it is empty, hence never a neighbourhood; thus no filter can force a non-strict value at ⊥. The representation strictFunEquiv then mirrors Theorem 3.10.

def Domain.Neighborhood.Exercise510.IsStrict {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : ApproximableMap V₀ V₁) : Prop

A map is strict when f(⊥) = ⊥. Relationally: f sends the master input only to the master output.

Equations

• Domain.Neighborhood.Exercise510.IsStrict f = ∀ ⦃Y : Set β⦄, f.rel V₀.master Y → Y = V₁.master

theorem Domain.Neighborhood.Exercise510.isStrict_iff_apply_bot {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f : ApproximableMap V₀ V₁} : IsStrict f ↔ f.toElementMap V₀.bot = V₁.bot

Strictness is exactly f(⊥) = ⊥.

theorem Domain.Neighborhood.Exercise510.IsStrict.mono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f g : ApproximableMap V₀ V₁} (hf : IsStrict f) (hgf : g ≤ f) : IsStrict g

Strictness is downward closed: a map below a strict map is strict.

theorem Domain.Neighborhood.Exercise510.isStrict_constBot {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : IsStrict (constMap V₀ V₁.bot)

The constant map at ⊥ is strict.

theorem Domain.Neighborhood.Exercise510.isStrict_idMap {α : Type u_1} {V₀ : NeighborhoodSystem α} : IsStrict (ApproximableMap.idMap V₀)

The identity is strict.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise510.StrictMap {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : Type (max 0 u_1 u_2)

The strict maps 𝒟₀ →⊥ 𝒟₁, as a subtype carrying the inherited approximation order.

Equations

• Domain.Neighborhood.Exercise510.StrictMap V₀ V₁ = { f : Domain.Neighborhood.ApproximableMap V₀ V₁ // Domain.Neighborhood.Exercise510.IsStrict f }

def Domain.Neighborhood.Exercise510.sstep {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (X : Set α) (Y : Set β) : Set (StrictMap V₀ V₁)

A step set among strict maps: [X, Y] = {f strict ∣ X f Y}.

Equations

• Domain.Neighborhood.Exercise510.sstep X Y = {f : Domain.Neighborhood.Exercise510.StrictMap V₀ V₁ | (↑f).rel X Y}

@[simp]

theorem Domain.Neighborhood.Exercise510.mem_sstep {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} {Y : Set β} {f : StrictMap V₀ V₁} : f ∈ sstep X Y ↔ (↑f).rel X Y

def Domain.Neighborhood.Exercise510.sstepFun {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (L : List (Set α × Set β)) : Set (StrictMap V₀ V₁)

A finite intersection of strict step sets.

Equations

• Domain.Neighborhood.Exercise510.sstepFun L = {f : Domain.Neighborhood.Exercise510.StrictMap V₀ V₁ | ∀ p ∈ L, (↑f).rel p.1 p.2}

@[simp]

theorem Domain.Neighborhood.Exercise510.mem_sstepFun {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} {f : StrictMap V₀ V₁} : f ∈ sstepFun L ↔ ∀ p ∈ L, (↑f).rel p.1 p.2

@[simp]

theorem Domain.Neighborhood.Exercise510.sstepFun_nil {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : sstepFun [] = Set.univ

theorem Domain.Neighborhood.Exercise510.sstepFun_cons {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (p : Set α × Set β) (L : List (Set α × Set β)) : sstepFun (p :: L) = sstep p.1 p.2 ∩ sstepFun L

theorem Domain.Neighborhood.Exercise510.sstepFun_append {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (L L' : List (Set α × Set β)) : sstepFun (L ++ L') = sstepFun L ∩ sstepFun L'

theorem Domain.Neighborhood.Exercise510.sstepFun_singleton {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (X : Set α) (Y : Set β) : sstepFun [(X, Y)] = sstep X Y

@[simp]

theorem Domain.Neighborhood.Exercise510.sstep_master_eq {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : sstep V₀.master V₁.master = Set.univ

[Δ₀, Δ₁] = |𝒟₀ →⊥ 𝒟₁|: every (strict) map relates the masters.

theorem Domain.Neighborhood.Exercise510.sstep_inter_right {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X : Set α} {Y Y' : Set β} (hY : V₁.mem Y) (hY' : V₁.mem Y') : sstep X Y ∩ sstep X Y' = sstep X (Y ∩ Y')

theorem Domain.Neighborhood.Exercise510.sstep_subset {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {X X' : Set α} {Y Y' : Set β} (hX' : V₀.mem X') (hY' : V₁.mem Y') (hX'X : X' ⊆ X) (hYY' : Y ⊆ Y') : sstep X Y ⊆ sstep X' Y'

def Domain.Neighborhood.Exercise510.strictFun {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : NeighborhoodSystem (StrictMap V₀ V₁)

Exercise 5.10 — the strict function space (𝒟₀ →⊥ 𝒟₁). Tokens are the strict approximable maps; neighbourhoods are non-empty finite intersections of step sets.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise510.strictFun_master {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : (strictFun V₀ V₁).master = Set.univ

theorem Domain.Neighborhood.Exercise510.strictFun_mem_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (StrictMap V₀ V₁)} : (strictFun V₀ V₁).mem W ↔ (∃ (L : List (Set α × Set β)), (∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) ∧ W = sstepFun L) ∧ W.Nonempty

theorem Domain.Neighborhood.Exercise510.sstep_mem_of_mem {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {g : StrictMap V₀ V₁} {X : Set α} {Y : Set β} (h : (↑g).rel X Y) : (strictFun V₀ V₁).mem (sstep X Y)

A step set is a neighbourhood as soon as it has a (strict) witness.

theorem Domain.Neighborhood.Exercise510.strictFun_mem_inter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W W' : Set (StrictMap V₀ V₁)} (hW : (strictFun V₀ V₁).mem W) (hW' : (strictFun V₀ V₁).mem W') (hne : (W ∩ W').Nonempty) : (strictFun V₀ V₁).mem (W ∩ W')

Intersection of two neighbourhoods, when non-empty, is again one.

theorem Domain.Neighborhood.Exercise510.sstepFun_up_closed {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} {f f' : StrictMap V₀ V₁} (hf : f ∈ sstepFun L) (hff' : f ≤ f') : f' ∈ sstepFun L

theorem Domain.Neighborhood.Exercise510.strictFun_mem_up_closed {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (StrictMap V₀ V₁)} (hW : (strictFun V₀ V₁).mem W) {f f' : StrictMap V₀ V₁} (hf : f ∈ W) (hff' : f ≤ f') : f' ∈ W

theorem Domain.Neighborhood.Exercise510.mem_sstepFun_iff {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (strictFun V₀ V₁).Element) {L : List (Set α × Set β)} (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) : φ.mem (sstepFun L) ↔ ∀ p ∈ L, φ.mem (sstep p.1 p.2)

The generation lemma: a filter contains sstepFun L iff it contains each step [Xᵢ, Yᵢ].

def Domain.Neighborhood.Exercise510.toStrictMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (strictFun V₀ V₁).Element) : StrictMap V₀ V₁

The strict map represented by a filter. X (toStrictMap φ) Y ↔ [X, Y] ∈ φ. It is strict because the step [Δ₀, Y] with Y ≠ Δ₁ is empty (no strict map relates Δ₀ to a proper output), hence not a neighbourhood, so it cannot belong to φ.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise510.toStrictMap_rel {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {φ : (strictFun V₀ V₁).Element} {X : Set α} {Y : Set β} : (↑(toStrictMap φ)).rel X Y ↔ φ.mem (sstep X Y)

def Domain.Neighborhood.Exercise510.toStrictFilter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (f : StrictMap V₀ V₁) : (strictFun V₀ V₁).Element

The filter f̂ = {F ∣ f ∈ F} of a strict map.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise510.mem_toStrictFilter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f : StrictMap V₀ V₁} {W : Set (StrictMap V₀ V₁)} : (toStrictFilter f).mem W ↔ (strictFun V₀ V₁).mem W ∧ f ∈ W

def Domain.Neighborhood.Exercise510.strictFunEquiv {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : (strictFun V₀ V₁).Element ≃o StrictMap V₀ V₁

Exercise 5.10 — the strict function space is complete. |𝒟₀ →⊥ 𝒟₁| is order-isomorphic to the strict approximable maps 𝒟₀ → 𝒟₁.

Equations

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

The adjunction (𝒟₀ →⊥ (𝒟₁ →⊥ 𝒟₂)) ≅ ((𝒟₀ ⊗ 𝒟₁) →⊥ 𝒟₂).

The smash product is left adjoint to the strict function space: strict maps out of a smash product are the same as strict maps into a strict function space. We realise the iso with the "appropriate combinators" Scott asks for — a strict curry and strict uncurry — connected by the computation g(⟨x, y⟩⊗) = (curry g)(x)(y).

The decisive computation is smashPair_principal_apply: for proper X, Y, applying g to the strict pairing of the principal elements is the same as g relating the proper neighbourhood X ∪ Y. At the bottom (a master factor) the strict pairing collapses to ⊥, where strictness forces the master output — exactly the gluing the smash performs.

theorem Domain.Neighborhood.Exercise510.smash_mem_prodNbhd_form {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {W : Set (α ⊕ β)} (hW : (smash V₀ V₁).mem W) : ∃ (A : Set α) (B : Set β), V₀.mem A ∧ V₁.mem B ∧ W = prodNbhd A B

Every smash neighbourhood is a product neighbourhood A ∪ B (the master is Δ₀ ∪ Δ₁).

theorem Domain.Neighborhood.Exercise510.smashPair_principal_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap (smash V₀ V₁) V₂) {X : Set α} {Y : Set β} (hX : V₀.mem X) (hXne : X ≠ V₀.master) (hY : V₁.mem Y) (hYne : Y ≠ V₁.master) {Z : Set γ} : (g.toElementMap (smashPair (V₀.principal hX) (V₁.principal hY))).mem Z ↔ g.rel (prodNbhd X Y) Z

The key computation. For proper X, Y, g(⟨↑X, ↑Y⟩⊗) contains Z iff g relates the proper neighbourhood X ∪ Y to Z. (Coarser members of the strict pairing are absorbed by monotonicity; the master member needs only that X ∪ Y ⊆ Δ₀ ∪ Δ₁.)

def Domain.Neighborhood.Exercise510.smashSection {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : ApproximableMap (smash V₀ V₁) V₂) {X : Set α} (hX : V₀.mem X) : ApproximableMap V₁ V₂

The X-section of g : 𝒟₀ ⊗ 𝒟₁ → 𝒟₂, as a map 𝒟₁ → 𝒟₂: y ↦ g(⟨↑X, y⟩⊗). Built with Exercise 2.8's ofMono from its values on principal inputs.

Equations

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

theorem Domain.Neighborhood.Exercise510.smashSection_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {g : ApproximableMap (smash V₀ V₁) V₂} {X : Set α} (hX : V₀.mem X) {Y : Set β} {Z : Set γ} : (smashSection g hX).rel Y Z ↔ ∃ (hY : V₁.mem Y), (g.toElementMap (smashPair (V₀.principal hX) (V₁.principal hY))).mem Z

theorem Domain.Neighborhood.Exercise510.smashSection_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {g : ApproximableMap (smash V₀ V₁) V₂} {X X' : Set α} (hX : V₀.mem X) (hX' : V₀.mem X') (hX'X : X' ⊆ X) : smashSection g hX ≤ smashSection g hX'

The section is monotone in the neighbourhood X (a smaller input gives a larger section).

theorem Domain.Neighborhood.Exercise510.isStrict_smashSection {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} {g : ApproximableMap (smash V₀ V₁) V₂} (hg : IsStrict g) {X : Set α} (hX : V₀.mem X) : IsStrict (smashSection g hX)

The section of a strict g is itself strict: g(⟨↑X, ⊥⟩⊗) = g(⊥) = ⊥.

theorem Domain.Neighborhood.Exercise510.rel_sstepFun_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : ApproximableMap V₀ (strictFun V₁ V₂)) {X : Set α} (hX : V₀.mem X) {L : List (Set β × Set γ)} (hL : ∀ p ∈ L, V₁.mem p.1 ∧ V₂.mem p.2) : h.rel X (sstepFun L) ↔ ∀ p ∈ L, h.rel X (sstep p.1 p.2)

The generation lemma for maps into the strict function space: X h (⋂ᵢ[Yᵢ,Zᵢ]) iff X h [Yᵢ,Zᵢ] for all i.

def Domain.Neighborhood.Exercise510.smashCurryMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : StrictMap (smash V₀ V₁) V₂) : StrictMap V₀ (strictFun V₁ V₂)

Strict curry combinator. curry⊥ : ((𝒟₀ ⊗ 𝒟₁) →⊥ 𝒟₂) → (𝒟₀ →⊥ (𝒟₁ →⊥ 𝒟₂)), sending g to x ↦ (y ↦ g(⟨x, y⟩⊗)).

Equations

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

def Domain.Neighborhood.Exercise510.smashUncurryMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : StrictMap V₀ (strictFun V₁ V₂)) : StrictMap (smash V₀ V₁) V₂

Strict uncurry combinator. uncurry⊥ : (𝒟₀ →⊥ (𝒟₁ →⊥ 𝒟₂)) → ((𝒟₀ ⊗ 𝒟₁) →⊥ 𝒟₂), X ∪ Y (uncurry⊥ h) Z ↔ X h [Y, Z].

Equations

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

The roundtrip identities and the adjunction isomorphism.

theorem Domain.Neighborhood.Exercise510.sstep_cod_master {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {Y : Set α} (hY : V₀.mem Y) : sstep Y V₁.master = Set.univ

A step with master codomain is everything: every strict map relates Y to Δ₁.

theorem Domain.Neighborhood.Exercise510.section_uncurry_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : StrictMap V₀ (strictFun V₁ V₂)) {X : Set α} (hX : V₀.mem X) {Y : Set β} (hY : V₁.mem Y) {Z : Set γ} : (smashSection (↑(smashUncurryMap h)) hX).rel Y Z ↔ (↑h).rel X (sstep Y Z)

The decisive computation for the adjunction. The X-section of uncurry⊥ h evaluated on a neighbourhood Y is exactly the strict-function value X h [Y, Z]. At the boundary (a master factor) both sides collapse via strictness; off the boundary it is smashPair_principal_apply.

theorem Domain.Neighborhood.Exercise510.smashUncurry_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (g : StrictMap (smash V₀ V₁) V₂) : smashUncurryMap (smashCurryMap g) = g

Roundtrip (i): uncurry⊥ ∘ curry⊥ = id.

theorem Domain.Neighborhood.Exercise510.smashCurry_uncurry {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h : StrictMap V₀ (strictFun V₁ V₂)) : smashCurryMap (smashUncurryMap h) = h

Roundtrip (ii): curry⊥ ∘ uncurry⊥ = id.

def Domain.Neighborhood.Exercise510.smashCurryEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : StrictMap (smash V₀ V₁) V₂ ≃o StrictMap V₀ (strictFun V₁ V₂)

Exercise 5.10 (Scott 1981, PRG-19) — the adjunction. The strict currying combinator is an order isomorphism ((𝒟₀ ⊗ 𝒟₁) →⊥ 𝒟₂) ≃ (𝒟₀ →⊥ (𝒟₁ →⊥ 𝒟₂)): the smash product is left adjoint to the strict function space.

Equations

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