Exercise 2.15 (Scott 1981, PRG-19, §2) — the one-token system 𝒪 (Sierpiński

space)

EXERCISE 2.15. (For topologists.) Consider the one-token system with 𝒪 = {{0}, ∅}. We can regard |𝒪| as having just two finite elements ⊥ and ⊤, where ⊥ ⊑ ⊤. For any system 𝒟, show that the open subsets U of |𝒟| are in a one-one correspondence with the approximable mappings f : 𝒟 → 𝒪, where the correspondence is given by U = {x ∣ f(x) = ⊤}. What are the open subsets of |𝒪|? of |𝕋|? of |𝔹|?

We take the token type to be Fin 1, so the master neighbourhood Δ = {0} is Set.univ and the two neighbourhoods of 𝒪 are Δ = univ and ∅. Then |𝒪| has exactly two elements: ⊥ = ↑Δ = {Δ} and ⊤ = ↑∅, with ⊥ ⊑ ⊤ (botElt_le_topElt, strict by botElt_ne_topElt). The space |𝒪| is Sierpiński space: its open sets are ∅, {⊤} (basicOpen ∅), and the whole space; {⊥} is not open (⊥ is the generic point, not_isOpen_singleton_botElt).

The main theorem (openSetEquivMap) is the Sierpiński-space adjunction "open sets = continuous maps to 𝒪", here in the approximable-mapping guise:

• openToMap U hU : ApproximableMap 𝒟 𝒪 — the map with f(x) = ⊤ ↔ x ∈ U, built choice-free as the neighbourhood relation X f Y ↔ X ∈ 𝒟 ∧ Y ∈ 𝒪 ∧ (Y = ∅ → ↑X ∈ U) (monotone because U is open, i.e. an upper set);
• mapToOpen f := {x ∣ f(x) = ⊤} — open (isOpen_mapToOpen), being the preimage of the open point {⊤} = [∅] under the continuous x ↦ f(x) (Exercise 2.13);
• openSetEquivMap : {U // IsOpen U} ≃ ApproximableMap 𝒟 𝒪 — the two are mutually inverse.

For the opens of |𝕋| and |𝔹|: 𝕋 (two incomparable totals true, false above ⊥) has opens generated by the two open points [{true}] = {true-total} and [{false}] = {false-total}; |𝔹|'s opens are generated by the basic cones [σΣ*]. We record only |𝒪|'s opens in Lean.

Choice-free (#print axioms ⊆ {propext, Quot.sound}) apart from the eq_of_toElementMap_principal uniqueness step inherited from Exercise 2.8.

The one-token system 𝒪.

def Domain.Neighborhood.Exercise215.memO (X : Set (Fin 1)) : Prop

Membership for 𝒪: a neighbourhood is the master Δ = univ or the empty set.

Equations

• Domain.Neighborhood.Exercise215.memO X = (X = Set.univ ∨ X = ∅)

theorem Domain.Neighborhood.Exercise215.univ_ne_empty : Set.univ ≠ ∅

theorem Domain.Neighborhood.Exercise215.nestedOrDisjoint_O : NestedOrDisjoint memO

theorem Domain.Neighborhood.Exercise215.subMaster_O {X : Set (Fin 1)} : memO X → X ⊆ Set.univ

def Domain.Neighborhood.Exercise215.O : NeighborhoodSystem (Fin 1)

Exercise 2.15 — the one-token system 𝒪 = {Δ, ∅}.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise215.O_mem {X : Set (Fin 1)} : O.mem X ↔ memO X

@[simp]

theorem Domain.Neighborhood.Exercise215.O_master : O.master = Set.univ

theorem Domain.Neighborhood.Exercise215.O_mem_empty : O.mem ∅

theorem Domain.Neighborhood.Exercise215.O_mem_univ : O.mem Set.univ

theorem Domain.Neighborhood.Exercise215.O_inter_mem {Y Y' : Set (Fin 1)} (hY : O.mem Y) (hY' : O.mem Y') : O.mem (Y ∩ Y')

𝒪 is closed under intersection (used to verify the relation of openToMap).

The two elements ⊥ ⊑ ⊤ of |𝒪|.

def Domain.Neighborhood.Exercise215.topElt : O.Element

The top element ⊤ = ↑∅ of |𝒪|.

Equations

• Domain.Neighborhood.Exercise215.topElt = Domain.Neighborhood.Exercise215.O.principal Domain.Neighborhood.Exercise215.O_mem_empty

def Domain.Neighborhood.Exercise215.botElt : O.Element

The bottom element ⊥ = ↑Δ = {Δ} of |𝒪|.

Equations

• Domain.Neighborhood.Exercise215.botElt = Domain.Neighborhood.Exercise215.O.bot

theorem Domain.Neighborhood.Exercise215.mem_botElt {Y : Set (Fin 1)} : botElt.mem Y ↔ Y = Set.univ

Y ∈ ⊥ iff Y = Δ = univ.

theorem Domain.Neighborhood.Exercise215.mem_empty_iff_eq_top (z : O.Element) : z.mem ∅ ↔ z = topElt

The defining property of ⊤. An element z of |𝒪| is ⊤ iff it contains ∅: ∅ is the sharpest neighbourhood, so ∅ ∈ z forces z to be the principal filter ↑∅ = ⊤.

theorem Domain.Neighborhood.Exercise215.element_eq_bot_or_top (z : O.Element) : z = botElt ∨ z = topElt

Two elements. Every element of |𝒪| is ⊥ or ⊤.

theorem Domain.Neighborhood.Exercise215.botElt_le_topElt : botElt ≤ topElt

⊥ ⊑ ⊤.

theorem Domain.Neighborhood.Exercise215.botElt_ne_topElt : botElt ≠ topElt

⊥ ≠ ⊤ (so ⊥ ⊏ ⊤).

theorem Domain.Neighborhood.Exercise215.O_ext {z w : O.Element} (h : z.mem ∅ ↔ w.mem ∅) : z = w

Extensionality for |𝒪|. Two elements agreeing on membership of ∅ are equal (it distinguishes ⊥ from ⊤).

The opens of |𝒪|.

theorem Domain.Neighborhood.Exercise215.basicOpen_empty_eq_singleton_top : O.basicOpen ∅ = {topElt}

The open point {⊤} is the basic open [∅].

theorem Domain.Neighborhood.Exercise215.not_isOpen_singleton_botElt : ¬IsOpen {botElt}

The opens of |𝒪|. {⊥} is not open: ⊥ is the generic point. (The basic neighbourhood of ⊥ is [Δ] = |𝒪|, which is not contained in {⊥} because it also contains ⊤.)

The correspondence between opens of |𝒟| and approximable maps 𝒟 → 𝒪.

def Domain.Neighborhood.Exercise215.openToMap {γ : Type u_1} (V : NeighborhoodSystem γ) (U : Set V.Element) (hU : IsOpen U) : ApproximableMap V O

Exercise 2.15 — the approximable map of an open set. For open U ⊆ |𝒟|, the relation X f Y ↔ X ∈ 𝒟 ∧ Y ∈ 𝒪 ∧ (Y = ∅ → ↑X ∈ U). The single nontrivial obligation is monotonicity: sharpening the input X' ⊆ X means ↑X ⊑ ↑X', and U open (an upper set) carries ↑X ∈ U up to ↑X' ∈ U. Choice-free.

Equations

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

theorem Domain.Neighborhood.Exercise215.toElementMap_openToMap_principal_mem_empty {γ : Type u_1} (V : NeighborhoodSystem γ) (U : Set V.Element) (hU : IsOpen U) {X : Set γ} (hX : V.mem X) : ((openToMap V U hU).toElementMap (V.principal hX)).mem ∅ ↔ V.principal hX ∈ U

The value of openToMap U hU on the finite element ↑X contains ∅ iff ↑X ∈ U; i.e. (openToMap U hU)(↑X) = ⊤ ↔ ↑X ∈ U.

def Domain.Neighborhood.Exercise215.mapToOpen {γ : Type u_1} (V : NeighborhoodSystem γ) (f : ApproximableMap V O) : Set V.Element

Exercise 2.15 — the open set of an approximable map. mapToOpen f = {x ∣ f(x) = ⊤}.

Equations

• Domain.Neighborhood.Exercise215.mapToOpen V f = {x : V.Element | f.toElementMap x = Domain.Neighborhood.Exercise215.topElt}

theorem Domain.Neighborhood.Exercise215.isOpen_mapToOpen {γ : Type u_1} (V : NeighborhoodSystem γ) (f : ApproximableMap V O) : IsOpen (mapToOpen V f)

mapToOpen f is open: it is the preimage of the open point {⊤} = [∅] under the continuous x ↦ f(x) (Exercise 2.13).

theorem Domain.Neighborhood.Exercise215.mem_mapToOpen_openToMap {γ : Type u_1} (V : NeighborhoodSystem γ) (U : Set V.Element) (hU : IsOpen U) (x : V.Element) : x ∈ mapToOpen V (openToMap V U hU) ↔ x ∈ U

Exercise 2.15 — round trip (open → map → open). mapToOpen (openToMap U hU) = U.

theorem Domain.Neighborhood.Exercise215.openToMap_mapToOpen {γ : Type u_1} (V : NeighborhoodSystem γ) (f : ApproximableMap V O) : openToMap V (mapToOpen V f) ⋯ = f

Exercise 2.15 — round trip (map → open → map). openToMap (mapToOpen f) = f.

def Domain.Neighborhood.Exercise215.openSetEquivMap {γ : Type u_1} (V : NeighborhoodSystem γ) : { U : Set V.Element // IsOpen U } ≃ ApproximableMap V O

Exercise 2.15 (main). The open subsets of |𝒟| are in one-one correspondence with the approximable mappings 𝒟 → 𝒪, via U ↦ openToMap U and f ↦ {x ∣ f(x) = ⊤}.

Equations

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