Exercise 2.22 (Scott 1981, PRG-19) — the abstract representation theorem

(For set theorists.) Exercises 1.18 and 2.11 noted that any domain |𝒟|, viewed as a family of sets, is closed under (i) the intersection of an arbitrary non-empty subfamily and (ii) the union of any directed subfamily. This exercise proves the converse: any family C of sets with these two closure properties is inclusion-isomorphic to a domain.

We follow Scott's hint. Fix C : Set (Set τ) (non-empty) closed under non-empty intersections (hInter) and directed unions (hDir).

• Δ = the finite sets F included in some member of C (here the subtype Tok C).
• The closure of F is Fbar = ⋂ {X ∈ C ∣ F ⊆ X} (Cl C F); since F lies in some member of C, this intersection is over a non-empty family, so Fbar ∈ C (Cl_mem). The Fbar are the "finite" elements.
• The neighbourhood system reprSystem over Δ has neighbourhoods C(F) = {G ∈ Δ ∣ F ⊆ Gbar} (nbhd C F).

The representation isomorphism reprIso : reprSystem.Element ≃o C (under ⊆) sends an ideal element x to ⋃ {Fbar ∣ C(F) ∈ x} and a set X ∈ C to the element generated by {C(F) ∣ F ⊆ X}. The key identity (Scott) is X = ⋃ {Fbar ∣ F ⊆ X, F ∈ Δ}, realized by toC_ofC/mem_nbhd_iff.

Axioms. This is the genuinely set-theoretic exercise: it uses Classical.choice (picking witnesses of C.Nonempty, finite-set induction). This is documented and expected per the exercise's framing ("for set theorists").

Closure and tokens.

def Domain.Neighborhood.Exercise222.Cl {τ : Type u_1} (C : Set (Set τ)) (F : Set τ) : Set τ

The closure Fbar = ⋂ {X ∈ C ∣ F ⊆ X} of a set F relative to the family C.

Equations

• Domain.Neighborhood.Exercise222.Cl C F = ⋂₀ {X : Set τ | X ∈ C ∧ F ⊆ X}

theorem Domain.Neighborhood.Exercise222.subset_Cl {τ : Type u_1} (C : Set (Set τ)) (F : Set τ) : F ⊆ Cl C F

F ⊆ Fbar: a set is contained in its closure.

theorem Domain.Neighborhood.Exercise222.Cl_subset {τ : Type u_1} (C : Set (Set τ)) {F X : Set τ} (hX : X ∈ C) (hFX : F ⊆ X) : Cl C F ⊆ X

Fbar ⊆ X whenever X ∈ C contains F: the closure is the smallest member of C over F.

def Domain.Neighborhood.Exercise222.IsTok {τ : Type u_1} (C : Set (Set τ)) (F : Set τ) : Prop

A token: a finite set included in some member of C.

Equations

• Domain.Neighborhood.Exercise222.IsTok C F = (F.Finite ∧ ∃ X ∈ C, F ⊆ X)

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise222.Tok {τ : Type u_1} (C : Set (Set τ)) : Type u_1

Scott's Δ: the type of tokens (finite sets included in members of C).

Equations

• Domain.Neighborhood.Exercise222.Tok C = { F : Set τ // Domain.Neighborhood.Exercise222.IsTok C F }

theorem Domain.Neighborhood.Exercise222.Cl_mem {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) {F : Set τ} (h : ∃ X ∈ C, F ⊆ X) : Cl C F ∈ C

Every closure Fbar of a token lies in C (closure under non-empty intersection).

The neighbourhood system reprSystem.

def Domain.Neighborhood.Exercise222.nbhd {τ : Type u_1} (C : Set (Set τ)) (F : Set τ) : Set (Tok C)

Scott's neighbourhood C(F) = {G ∈ Δ ∣ F ⊆ Gbar}.

Equations

• Domain.Neighborhood.Exercise222.nbhd C F = {G : Domain.Neighborhood.Exercise222.Tok C | F ⊆ Domain.Neighborhood.Exercise222.Cl C ↑G}

@[simp]

theorem Domain.Neighborhood.Exercise222.mem_nbhd {τ : Type u_1} (C : Set (Set τ)) {F : Set τ} {G : Tok C} : G ∈ nbhd C F ↔ F ⊆ Cl C ↑G

theorem Domain.Neighborhood.Exercise222.nbhd_subset_iff {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) {F G : Set τ} (hF : IsTok C F) : nbhd C F ⊆ nbhd C G ↔ G ⊆ Cl C F

C(F) ⊆ C(G) ↔ G ⊆ Fbar: comparison of neighbourhoods reduces to inclusion against closures.

theorem Domain.Neighborhood.Exercise222.nbhd_empty {τ : Type u_1} (C : Set (Set τ)) : nbhd C ∅ = Set.univ

C(∅) = Δ: the empty token's neighbourhood is everything (the master).

def Domain.Neighborhood.Exercise222.botTok {τ : Type u_1} (C : Set (Set τ)) (hne : C.Nonempty) : Tok C

The empty token ∅ ∈ Δ (needs C non-empty for ∅ to lie in some member).

Equations

• Domain.Neighborhood.Exercise222.botTok C hne = ⟨∅, ⋯⟩

def Domain.Neighborhood.Exercise222.reprSystem {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) : NeighborhoodSystem (Tok C)

The representation neighbourhood system reprSystem over Δ = Tok C: neighbourhoods are exactly the C(F) for tokens F, the master is all of Δ = C(∅).

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise222.mem_reprSystem {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) {N : Set (Tok C)} : (reprSystem C hInter hne).mem N ↔ ∃ (F : Tok C), N = nbhd C ↑F

@[simp]

theorem Domain.Neighborhood.Exercise222.reprSystem_master {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) : (reprSystem C hInter hne).master = Set.univ

From an element to a set of C: x ↦ ⋃ {Fbar ∣ C(F) ∈ x}.

def Domain.Neighborhood.Exercise222.famC {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (x : (reprSystem C hInter hne).Element) : Set (Set τ)

The family {Fbar ∣ C(F) ∈ x} of finite-element closures present in the ideal element x.

Equations

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

def Domain.Neighborhood.Exercise222.toC {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (x : (reprSystem C hInter hne).Element) : Set τ

Scott's ⋃ {Fbar ∣ C(F) ∈ x}: the set of C represented by the ideal element x.

Equations

• Domain.Neighborhood.Exercise222.toC C hInter hne x = ⋃₀ Domain.Neighborhood.Exercise222.famC C hInter hne x

theorem Domain.Neighborhood.Exercise222.mem_toC {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (x : (reprSystem C hInter hne).Element) {t : τ} : t ∈ toC C hInter hne x ↔ ∃ (F : Tok C), x.mem (nbhd C ↑F) ∧ t ∈ Cl C ↑F

theorem Domain.Neighborhood.Exercise222.directed_step {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (x : (reprSystem C hInter hne).Element) {F F' : Tok C} (hF : x.mem (nbhd C ↑F)) (hF' : x.mem (nbhd C ↑F')) : ∃ (F₃ : Tok C), x.mem (nbhd C ↑F₃) ∧ Cl C ↑F ⊆ Cl C ↑F₃ ∧ Cl C ↑F' ⊆ Cl C ↑F₃

Directedness step. If C(F), C(F') ∈ x then there is a token F₃ with C(F₃) ∈ x whose closure dominates both Fbar and Fbar'. (From the filter intersection C(F) ∩ C(F') ∈ x, which is some C(F₃).)

theorem Domain.Neighborhood.Exercise222.mem_nbhd_bot {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (x : (reprSystem C hInter hne).Element) : x.mem (nbhd C ↑(botTok C hne))

The empty token's neighbourhood C(∅) = Δ is in every element (it is the master).

theorem Domain.Neighborhood.Exercise222.exists_tok_of_finite_subset {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (x : (reprSystem C hInter hne).Element) {s : Set τ} (hs : s.Finite) (hsub : s ⊆ toC C hInter hne x) : ∃ (F : Tok C), x.mem (nbhd C ↑F) ∧ s ⊆ Cl C ↑F

Finite sets are captured by a single token. A finite s ⊆ toC x is contained in some Fbar with C(F) ∈ x — the finite-subcover property of the directed union toC x.

theorem Domain.Neighborhood.Exercise222.mem_nbhd_iff {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (x : (reprSystem C hInter hne).Element) (G : Tok C) : x.mem (nbhd C ↑G) ↔ ↑G ⊆ toC C hInter hne x

Key membership identity. C(G) ∈ x ↔ G ⊆ toC x. Forward: G ⊆ Gbar ⊆ toC x. Reverse: G is finite, so the finite-subcover lemma gives F with C(F) ∈ x and G ⊆ Fbar, whence C(F) ⊆ C(G) and upward closure gives C(G) ∈ x.

From a set of C to an element: X ↦ {C(F) ∣ F ⊆ X}.

def Domain.Neighborhood.Exercise222.ofC {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (X : Set τ) (hX : X ∈ C) : (reprSystem C hInter hne).Element

The ideal element generated by X ∈ C: it contains the neighbourhoods above some C(F) with F ⊆ X.

Equations

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

theorem Domain.Neighborhood.Exercise222.toC_ofC {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (X : Set τ) (hX : X ∈ C) : toC C hInter hne (ofC C hInter hne X hX) = X

Scott's identity X = ⋃ {Fbar ∣ F ⊆ X, F ∈ Δ} in round-trip form: toC (ofC X) = X.

theorem Domain.Neighborhood.Exercise222.toC_mem {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (hDir : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → DirectedOn (fun (x1 x2 : Set τ) => x1 ⊆ x2) 𝒮 → ⋃₀ 𝒮 ∈ C) (x : (reprSystem C hInter hne).Element) : toC C hInter hne x ∈ C

toC x ∈ C: the represented set lies in the family (closure under directed unions).

theorem Domain.Neighborhood.Exercise222.ofC_toC {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (hDir : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → DirectedOn (fun (x1 x2 : Set τ) => x1 ⊆ x2) 𝒮 → ⋃₀ 𝒮 ∈ C) (x : (reprSystem C hInter hne).Element) : ofC C hInter hne (toC C hInter hne x) ⋯ = x

The other round-trip ofC (toC x) = x.

The representation isomorphism.

def Domain.Neighborhood.Exercise222.reprIso {τ : Type u_1} (C : Set (Set τ)) (hInter : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → ⋂₀ 𝒮 ∈ C) (hne : C.Nonempty) (hDir : ∀ (𝒮 : Set (Set τ)), 𝒮.Nonempty → 𝒮 ⊆ C → DirectedOn (fun (x1 x2 : Set τ) => x1 ⊆ x2) 𝒮 → ⋃₀ 𝒮 ∈ C) : (reprSystem C hInter hne).Element ≃o { X : Set τ // X ∈ C }

Exercise 2.22 — the representation theorem. C, ordered by inclusion, is order-isomorphic to the domain |reprSystem|. The isomorphism sends x ↦ ⋃ {Fbar ∣ C(F) ∈ x} (toC) and X ↦ {C(F) ∣ F ⊆ X} (ofC).

Equations

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