Exercise 3.28 (Scott 1981, PRG-19, §3) — the elementwise formula for the least

map

In (𝒟₀ → 𝒟₁), let ⋂ {[Xᵢ, Yᵢ] ∣ i < n} be a non-empty neighbourhood. Proposition 3.9 characterizes its minimal element f₀ as a relation (leastMap, X f₀ Y ↔ ⋂{Yᵢ ∣ X ⊆ Xᵢ} ⊆ Y). Exercise 3.28 asks for the elementwise description:

f₀(x) = ⊔ { ↑Yᵢ ∣ x ∈ [Xᵢ] } for x ∈ |𝒟₀|,

where x ∈ [Xᵢ] means Xᵢ ∈ x (the input is at least as defined as Xᵢ). We formalize this as toElementMap_leastMap_eq_sSup: f₀(x) is the least upper bound (Exercise 1.27's sSup) of the principal filters ↑Yᵢ over the active indices.

The proof shows f₀(x) is the least upper bound of that set: it is an upper bound (val_le_leastMap_toElementMap, from Yᵢ ∈ f₀(x)), and it is least (leastMap_toElementMap_le_of_ub, because any upper bound contains every relevant Yᵢ, hence the finite intersection ⋂{Yᵢ ∣ X ⊆ Xᵢ}); the equality with ⊔ then follows by antisymmetry.

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

theorem Domain.Neighborhood.Element.mem_interYs_of {α : Type u_1} {β : Type u_2} {V₁ : NeighborhoodSystem β} (z : V₁.Element) {L : List (Set α × Set β)} {X : Set α} (hall : ∀ p ∈ L, X ⊆ p.1 → z.mem p.2) : z.mem (interYs V₁.master L X)

A filter z contains the finite intersection ⋂{Yᵢ ∣ X ⊆ Xᵢ} (inside Δ₁) as soon as it contains each Yᵢ whose input Xᵢ ⊇ X. (The element-side analogue of rel_interYs.)

def Domain.Neighborhood.leastMapVals {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (L : List (Set α × Set β)) (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) (x : V₀.Element) : Set V₁.Element

Exercise 3.28 — the active values. The set { ↑Yᵢ ∣ x ∈ [Xᵢ] } of principal filters whose input Xᵢ is a member of x.

Equations

• Domain.Neighborhood.leastMapVals L hL x = {z : V₁.Element | ∃ (p : Set α × Set β) (hp : p ∈ L), x.mem p.1 ∧ z = V₁.principal ⋯}

theorem Domain.Neighborhood.val_le_leastMap_toElementMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) (hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master L X)) {x : V₀.Element} {p : Set α × Set β} (hp : p ∈ L) (hp1x : x.mem p.1) : V₁.principal ⋯ ≤ (leastMap L ⋯).toElementMap x

Each active value ↑Yᵢ (with Xᵢ ∈ x) approximates f₀(x), because Yᵢ ∈ f₀(x).

theorem Domain.Neighborhood.leastMapVals_bounded {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) (hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master L X)) (x : V₀.Element) : V₁.Bounded (leastMapVals L hL x)

The active values are bounded (by f₀(x)).

theorem Domain.Neighborhood.leastMap_toElementMap_le_of_ub {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {L : List (Set α × Set β)} (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) (hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master L X)) {x : V₀.Element} {z : V₁.Element} (hz : ∀ w ∈ leastMapVals L hL x, w ≤ z) : (leastMap L ⋯).toElementMap x ≤ z

f₀(x) is a lower bound of the upper bounds: any upper bound z of the active values dominates f₀(x). (Uses that z then contains ⋂{Yᵢ ∣ X ⊆ Xᵢ}.)

theorem Domain.Neighborhood.toElementMap_leastMap_eq_sSup {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (L : List (Set α × Set β)) (hL : ∀ p ∈ L, V₀.mem p.1 ∧ V₁.mem p.2) (hcons : ∀ {X : Set α}, V₀.mem X → V₁.mem (interYs V₁.master L X)) (x : V₀.Element) : (leastMap L ⋯).toElementMap x = V₁.sSup (leastMapVals L hL x) ⋯

Exercise 3.28 (Scott 1981, PRG-19). The least map's elementwise action is the least upper bound of the active principal filters: f₀(x) = ⊔ { ↑Yᵢ ∣ x ∈ [Xᵢ] }.