Exercise 4.10 (Scott 1981, PRG-19, Lecture IV) — the relativized domain Dₐ

Given a domain 𝒟 and an element a ∈ |𝒟|, construct a domain Dₐ whose elements are exactly the elements below a:

|Dₐ| = {x ∈ |𝒟| ∣ x ⊑ a}.

Construction. relSystem a keeps the same tokens and master Δ, but takes as neighbourhoods exactly the members of the filter a (mem X := a.mem X). This is a neighbourhood system because a, being a filter, contains Δ and is closed under consistent intersections. Its filters are in order-isomorphism with the elements of 𝒟 below a (relIso): a Dₐ-filter g is sent to its 𝒟-upward-closure embed a g, and an element x ⊑ a is sent to its restriction restrict a x (automatically a Dₐ-filter since x.mem ⊆ a.mem).

Restriction of f. If f : 𝒟 → 𝒟 is approximable and f(a) = a (e.g. a = fix(f), by Theorem 4.1), then f restricts to an approximable f' : Dₐ → Dₐ (relMap) with the same action (embed a (f'(g)) = f(embed a g), relMap_toElementMap_embed). The codomain condition f.rel X Y ⟹ a.mem Y for a-neighbourhoods X holds because ↑X ⊑ a, so Y ∈ f(↑X) ⊑ f(a) = a.

How many fixed points does f' have? When a = fix(f), exactly one (relMap_unique_fixed): the top element of Dₐ (corresponding to fix(f) itself). Any fixed point of f below fix(f) is a pre-fixed point, hence ⊒ fix(f) by leastness (fixElement_below_unique), so it equals fix(f).

All constructions are choice-free; equalities of Element/maps use the project's permitted Element.ext.

The relativized domain Dₐ.

def Domain.Neighborhood.ApproximableMap.relSystem {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) : NeighborhoodSystem α

Exercise 4.10 (Scott 1981, PRG-19). The relativized neighbourhood system Dₐ: same tokens and master, neighbourhoods exactly the members of the filter a.

Equations

• Domain.Neighborhood.ApproximableMap.relSystem a = { mem := fun (X : Set α) => a.mem X, master := V.master, master_mem := ⋯, inter_mem := ⋯, sub_master := ⋯ }

@[simp]

theorem Domain.Neighborhood.ApproximableMap.relSystem_mem {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) {X : Set α} : (relSystem a).mem X ↔ a.mem X

@[simp]

theorem Domain.Neighborhood.ApproximableMap.relSystem_master {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) : (relSystem a).master = V.master

def Domain.Neighborhood.ApproximableMap.embed {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) (g : (relSystem a).Element) : V.Element

The 𝒟-element obtained from a Dₐ-filter by upward closure in 𝒟.

Equations

• Domain.Neighborhood.ApproximableMap.embed a g = { mem := fun (X : Set α) => V.mem X ∧ ∃ (W : Set α), a.mem W ∧ g.mem W ∧ W ⊆ X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

def Domain.Neighborhood.ApproximableMap.restrict {α : Type u_1} {V : NeighborhoodSystem α} (a x : V.Element) (hx : x ≤ a) : (relSystem a).Element

The Dₐ-filter obtained from an element x ⊑ a by restriction (same membership).

Equations

• Domain.Neighborhood.ApproximableMap.restrict a x hx = { mem := fun (X : Set α) => x.mem X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

theorem Domain.Neighborhood.ApproximableMap.embed_le {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) (g : (relSystem a).Element) : embed a g ≤ a

embed a g ⊑ a: the embedding lands below a.

theorem Domain.Neighborhood.ApproximableMap.embed_restrict {α : Type u_1} {V : NeighborhoodSystem α} (a x : V.Element) (hx : x ≤ a) : embed a (restrict a x hx) = x

theorem Domain.Neighborhood.ApproximableMap.restrict_embed {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) (g : (relSystem a).Element) : restrict a (embed a g) ⋯ = g

theorem Domain.Neighborhood.ApproximableMap.embed_mono {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) {g₁ g₂ : (relSystem a).Element} (h : g₁ ≤ g₂) : embed a g₁ ≤ embed a g₂

theorem Domain.Neighborhood.ApproximableMap.le_of_embed_le {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) {g₁ g₂ : (relSystem a).Element} (h : embed a g₁ ≤ embed a g₂) : g₁ ≤ g₂

def Domain.Neighborhood.ApproximableMap.relIso {α : Type u_1} {V : NeighborhoodSystem α} (a : V.Element) : (relSystem a).Element ≃o { x : V.Element // x ≤ a }

Exercise 4.10 (Scott 1981, PRG-19). |Dₐ| ≃o {x ∈ |𝒟| ∣ x ⊑ a}: the relativized domain has exactly the elements below a as its points, with the inherited order.

Equations

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

Restricting an endomap with f(a) = a.

def Domain.Neighborhood.ApproximableMap.relMap {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {a : V.Element} (ha : f.toElementMap a = a) : ApproximableMap (relSystem a) (relSystem a)

Exercise 4.10 (Scott 1981, PRG-19). When f(a) = a, the restriction f' : Dₐ → Dₐ (f'(x) = f(x)). The codomain condition uses ↑X ⊑ a ⟹ f(↑X) ⊑ f(a) = a.

Equations

• f.relMap ha = { rel := fun (X Y : Set α) => a.mem X ∧ f.rel X Y, rel_dom := ⋯, rel_cod := ⋯, master_rel := ⋯, inter_right := ⋯, mono := ⋯ }

theorem Domain.Neighborhood.ApproximableMap.relMap_toElementMap_embed {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {a : V.Element} (ha : f.toElementMap a = a) (g : (relSystem a).Element) : embed a ((f.relMap ha).toElementMap g) = f.toElementMap (embed a g)

The restriction f' has the same action as f: embed a (f'(g)) = f(embed a g).

How many fixed points does f' have?

theorem Domain.Neighborhood.ApproximableMap.fixElement_below_unique {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) {x : V.Element} (hxle : x ≤ f.fixElement) (hxfix : f.toElementMap x = x) : x = f.fixElement

Exercise 4.10 (Scott 1981, PRG-19). Any fixed point of f below fix(f) is fix(f): a fixed point is a pre-fixed point, so leastness forces fix(f) ⊑ x.

theorem Domain.Neighborhood.ApproximableMap.relMap_unique_fixed {α : Type u_1} {V : NeighborhoodSystem α} (f : ApproximableMap V V) (ha : f.toElementMap f.fixElement = f.fixElement) (g : (relSystem f.fixElement).Element) (hg : (f.relMap ha).toElementMap g = g) : g = restrict f.fixElement f.fixElement ⋯

Exercise 4.10 (Scott 1981, PRG-19). With a = fix(f), the restricted map f' has exactly one fixed point: the top element of D_{fix f}, namely restrict (fix f) of fix f itself. Every Dₐ-fixed point g of f' satisfies embed a g = fix f, hence is this top element.