Theorem 1.10 (Scott 1981, PRG-19, §1) — the element-token system {[X]}

Given any neighbourhood system 𝒟, Scott replaces the tokens Δ by the elements |𝒟| themselves: for X ∈ 𝒟 put

[X] = {x ∈ |𝒟| ∣ X ∈ x},

the set of elements that contain X. The family {[X] ∣ X ∈ 𝒟} is a neighbourhood system over |𝒟|, and it determines a domain isomorphic to |𝒟| (Definition 1.9). "The rôle of the tokens is simply to keep the inclusions (and intersections) of neighbourhoods sorted out."

We prove Scott's four facts:

• (1) [Δ] = |𝒟| — bracket_master;
• (2) X, Y consistent in 𝒟 iff [X]∩[Y] ≠ ∅ — bracket_inter_nonempty_iff;
• (3) [X] ∩ [Y] = [X ∩ Y] (for X, Y ∈ 𝒟) — bracket_inter;
• (4) ↑X ∈ [X] — principal_mem_bracket;

together with the one-one (bracket_injective), inclusion-preserving (bracket_subset_iff) correspondence X ↦ [X], and finally the induced order-isomorphism tokenIso : |𝒟| ≃o |{[X]}|, giving 𝒟 ≅ᴰ tokenSystem (isomorphic_tokenSystem).

Everything is constructive ([propext, Quot.sound]): [X]-membership is just x.mem X, and the filter laws mirror the constructive proofs for principal.

def Domain.Neighborhood.NeighborhoodSystem.bracket {α : Type u_1} (V : NeighborhoodSystem α) (X : Set α) : Set V.Element

Scott's [X] = {x ∈ |𝒟| ∣ X ∈ x}: the elements of |𝒟| that contain the neighbourhood X. (This is the basicOpen X of Exercise 1.22, repeated here to avoid the topology dependency.)

Equations

• V.bracket X = {x : V.Element | x.mem X}

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.mem_bracket {α : Type u_1} (V : NeighborhoodSystem α) {X : Set α} {x : V.Element} : x ∈ V.bracket X ↔ x.mem X

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.bracket_master {α : Type u_1} (V : NeighborhoodSystem α) : V.bracket V.master = Set.univ

Theorem 1.10 (1). [Δ] = |𝒟|: every element contains the master neighbourhood.

theorem Domain.Neighborhood.NeighborhoodSystem.principal_mem_bracket {α : Type u_1} (V : NeighborhoodSystem α) {X : Set α} (hX : V.mem X) : V.principal hX ∈ V.bracket X

Theorem 1.10 (4). ↑X ∈ [X]: the principal filter of X contains X.

theorem Domain.Neighborhood.NeighborhoodSystem.bracket_inter {α : Type u_1} (V : NeighborhoodSystem α) {X Y : Set α} (hX : V.mem X) (hY : V.mem Y) : V.bracket X ∩ V.bracket Y = V.bracket (X ∩ Y)

Theorem 1.10 (3). [X] ∩ [Y] = [X ∩ Y] for X, Y ∈ 𝒟. (⊆ is filter closure under ∩; ⊇ is upward closure along X ∩ Y ⊆ X, X ∩ Y ⊆ Y.)

theorem Domain.Neighborhood.NeighborhoodSystem.bracket_subset_iff {α : Type u_1} (V : NeighborhoodSystem α) {X Y : Set α} (hX : V.mem X) (hY : V.mem Y) : V.bracket X ⊆ V.bracket Y ↔ X ⊆ Y

The correspondence X ↦ [X] is inclusion-preserving. [X] ⊆ [Y] ↔ X ⊆ Y (for X,Y ∈ 𝒟). → tests at ↑X ∈ [X], reading X ⊆ Y off ↑X ∈ [Y]; ← is upward closure.

theorem Domain.Neighborhood.NeighborhoodSystem.bracket_injective {α : Type u_1} (V : NeighborhoodSystem α) {X Y : Set α} (hX : V.mem X) (hY : V.mem Y) (h : V.bracket X = V.bracket Y) : X = Y

The correspondence X ↦ [X] is one-one. [X] = [Y] ⟹ X = Y (for X,Y ∈ 𝒟).

theorem Domain.Neighborhood.NeighborhoodSystem.bracket_inter_nonempty_iff {α : Type u_1} (V : NeighborhoodSystem α) {X Y : Set α} (hX : V.mem X) (hY : V.mem Y) : (V.bracket X ∩ V.bracket Y).Nonempty ↔ ∃ (Z : Set α), V.mem Z ∧ Z ⊆ X ∩ Y

Theorem 1.10 (2). X, Y are consistent in 𝒟 (have a common lower bound Z ∈ 𝒟, Z ⊆ X ∩ Y) iff [X] ∩ [Y] ≠ ∅. → uses ↑Z (which lies in both [X] and [Y]); ← reads a witness off any common element.

The token system {[X]} and the isomorphism.

def Domain.Neighborhood.NeighborhoodSystem.tokenSystem {α : Type u_1} (V : NeighborhoodSystem α) : NeighborhoodSystem V.Element

Theorem 1.10. The element-token system {[X] ∣ X ∈ 𝒟} over the tokens |𝒟|. The two laws reduce to facts about [·]: the master [Δ] = |𝒟| is the whole space; the consistency witness [W] for [X] ∩ [Y] yields W ⊆ X ∩ Y (via ↑W), so X ∩ Y ∈ 𝒟 and [X] ∩ [Y] = [X ∩ Y].

Equations

• V.tokenSystem = { mem := fun (S : Set V.Element) => ∃ (X : Set α), V.mem X ∧ S = V.bracket X, master := Set.univ, master_mem := ⋯, inter_mem := ⋯, sub_master := ⋯ }

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.tokenSystem_mem {α : Type u_1} (V : NeighborhoodSystem α) {S : Set V.Element} : V.tokenSystem.mem S ↔ ∃ (X : Set α), V.mem X ∧ S = V.bracket X

def Domain.Neighborhood.NeighborhoodSystem.toToken {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) : V.tokenSystem.Element

The element of |{[X]}| corresponding to x ∈ |𝒟|: the filter {[X] ∣ X ∈ x}.

Equations

• V.toToken x = { mem := fun (S : Set V.Element) => ∃ (X : Set α), x.mem X ∧ S = V.bracket X, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

def Domain.Neighborhood.NeighborhoodSystem.ofToken {α : Type u_1} (V : NeighborhoodSystem α) (y : V.tokenSystem.Element) : V.Element

The element of |𝒟| corresponding to y ∈ |{[X]}|: the filter {X ∣ [X] ∈ y}.

Equations

• V.ofToken y = { mem := fun (X : Set α) => V.mem X ∧ y.mem (V.bracket X), sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

def Domain.Neighborhood.NeighborhoodSystem.tokenIso {α : Type u_1} (V : NeighborhoodSystem α) : V.Element ≃o V.tokenSystem.Element

Theorem 1.10 (the isomorphism). X ↦ [X] induces an order-isomorphism |𝒟| ≃o |{[X]}|: toToken and ofToken are mutually inverse and preserve/reflect ⊑.

Equations

• V.tokenIso = { toFun := V.toToken, invFun := V.ofToken, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem Domain.Neighborhood.NeighborhoodSystem.isomorphic_tokenSystem {α : Type u_1} (V : NeighborhoodSystem α) : V ≅ᴰ V.tokenSystem

Theorem 1.10 (statement). Any neighbourhood system is isomorphic to its element-token system: 𝒟 ≅ᴰ {[X]}.