Exercise 1.21 (Scott 1981, PRG-19, §1) — Theorem 1.10 in greater detail

Scott asks to work out the proof of Theorem 1.10 more fully and to observe two further properties of the element-token system {[X]} over |𝒟|:

• it is positive (tokenSystem_isPositive), giving "in a different way the same kind of conclusion as in 1.20";
• it is complete (tokenSystem_complete): every filter is fixed by a unique point — the point whose filter of containing neighbourhoods it is. We formalize "fixed by a point" as IsComplete, and derive it from the bijection tokenIso of Theorem 1.10 (tokenSystem_toToken_bijective). Thus tokens and (partial) elements are identified.

Finally, consistency of {Xᵢ ∣ i < n} is equivalent to ⋂_{i<n} [Xᵢ] ≠ ∅ (consistent_iff_iInter_bracket_nonempty), the finite generalization of Theorem 1.10(2) via Theorem 1.1c.

Everything is [propext, Quot.sound] (the corollaries inherit the constructive proofs of Theorem 1.10 / Theorem 1.1c).

theorem Domain.Neighborhood.NeighborhoodSystem.tokenSystem_isPositive {α : Type u_1} (V : NeighborhoodSystem α) : V.tokenSystem.IsPositive

Exercise 1.21 — the token system is positive. [X] ∩ [Y] = [X ∩ Y] is a neighbourhood iff non-empty: a common element x gives X ∩ Y ∈ 𝒟 (via x.sub (x.inter_mem …)); conversely [W] always contains the principal filter ↑W.

Completeness: every filter is fixed by a unique point.

def Domain.Neighborhood.NeighborhoodSystem.IsComplete {β : Type u_2} (V' : NeighborhoodSystem β) : Prop

A neighbourhood system 𝒟' over β is complete when every filter y ∈ |𝒟'| is fixed by a unique point b ∈ β: a neighbourhood S lies in y iff b ∈ S. (Scott: "a filter is fixed by a point iff it is the filter of all neighbourhoods containing that point".)

Equations

• V'.IsComplete = ∀ (y : V'.Element), ∃! b : β, ∀ (S : Set β), V'.mem S → (y.mem S ↔ b ∈ S)

theorem Domain.Neighborhood.NeighborhoodSystem.tokenSystem_complete {α : Type u_1} (V : NeighborhoodSystem α) : V.tokenSystem.IsComplete

Exercise 1.21 — the token system is complete. Every filter y of {[X]} is fixed by the unique point ofToken y ∈ |𝒟|: [W] ∈ y ↔ ofToken y ∈ [W]. Uniqueness is Element.ext applied through the brackets.

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

The filter of {[X]} fixed by the point x ∈ |𝒟| is toToken x (the filter of all brackets containing x). By Theorem 1.10 this is a bijection |𝒟| ≃ |{[X]}|, so tokens and (partial) elements are identified.

Equations

• V.filterFixedBy x = V.toToken x

theorem Domain.Neighborhood.NeighborhoodSystem.tokenSystem_toToken_bijective {α : Type u_1} (V : NeighborhoodSystem α) : Function.Bijective V.toToken

Exercise 1.21 — tokens ↔ elements. toToken : |𝒟| → |{[X]}| is a bijection (it is the underlying map of the order-iso tokenIso), so a complete system identifies tokens with (partial) elements under a one-one correspondence.

Consistency iff non-empty intersection of brackets.

theorem Domain.Neighborhood.NeighborhoodSystem.bracket_nonempty_iff {α : Type u_1} (V : NeighborhoodSystem α) {X : Set α} : (V.bracket X).Nonempty ↔ V.mem X

[X] ≠ ∅ iff X ∈ 𝒟. → reads X ∈ 𝒟 off any element of [X]; ← exhibits ↑X.

theorem Domain.Neighborhood.NeighborhoodSystem.consistent_iff_bracket_interUpTo_nonempty {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) {n : ℕ} (hX : ∀ (i : ℕ), i < n → V.mem (X i)) : V.Consistent X n ↔ (V.bracket (V.interUpTo X n)).Nonempty

Exercise 1.21 — consistency via the intersection [⋂]. For X₀, …, Xₙ₋₁ ∈ 𝒟, ⟨Xᵢ⟩ is consistent iff [⋂_{i<n} Xᵢ] ≠ ∅. Combines Theorem 1.1c (consistent_iff_interUpTo_mem) with bracket_nonempty_iff.

theorem Domain.Neighborhood.NeighborhoodSystem.consistent_iff_iInter_bracket_nonempty {α : Type u_1} (V : NeighborhoodSystem α) (X : ℕ → Set α) {n : ℕ} (hX : ∀ (i : ℕ), i < n → V.mem (X i)) : V.Consistent X n ↔ ∃ (x : V.Element), ∀ (i : ℕ), i < n → x ∈ V.bracket (X i)

Exercise 1.21 — consistency iff ⋂_{i<n} [Xᵢ] ≠ ∅. The literal form of Scott's equivalence: ⟨Xᵢ⟩ is consistent iff there is a filter lying in every [Xᵢ] (i < n). → uses upward closure along ⋂_{i<n} Xᵢ ⊆ Xᵢ; ← uses Element.mem_interUpTo.