Lecture VI — Definition 6.10 (Scott 1981, PRG-19): the subsystem relation `D ◁

E`

To explain why the minimal solutions of a domain equation exist, Scott introduces a notion of "subdomain". The functors T he has in mind are not merely continuous on maps (Definition 6.8) but also possess continuity properties on domains, and those are phrased in terms of this relation.

Definition 6.10. For two neighbourhood systems D and E over the same set of tokens Δ, we write D ◁ E to mean that

• D ⊆ E (every neighbourhood of D is a neighbourhood of E), and
• whenever X, Y ∈ D and X ∩ Y ∈ E, then X ∩ Y ∈ D.

The second clause is the crucial one: it says the notion of consistency in D is the same as in E. A subdomain is a smaller family of neighbourhoods, but it must agree with E about which pairs are consistent.

This module formalizes the relation together with the elementary facts Scott records in the prose:

• it is reflexive (Subsystem.refl) and transitive (Subsystem.trans);
• it is antisymmetric (Subsystem.antisymm): D ◁ E and E ◁ D force D = E;
• Scott's remark. If D₀ ◁ E and D₁ ◁ E, then D₀ ◁ D₁ ↔ D₀ ⊆ D₁ (Subsystem.subsystem_iff_subset_of_common) — once both sit inside a common E, the subdomain relation collapses to plain inclusion of neighbourhood families.

Everything here is at the Prop level and choice-free (#print axioms ⊆ {propext, Quot.sound}). Propositions 6.11 (the subsystems of E form a domain) and 6.12 (a D ◁ E yields a projection pair i, j) build on this relation and are formalized separately.

structure Domain.Neighborhood.Subsystem {α : Type u_1} (D E : NeighborhoodSystem α) : Prop

Definition 6.10 (Scott 1981, PRG-19). The subsystem (subdomain) relation D ◁ E for two neighbourhood systems over the same token type. It records that D and E are systems over the same Δ (master_eq), that D is a subfamily of E (sub), and — the essential clause — that consistency is inherited from E: an intersection of two D-neighbourhoods that happens to be an E-neighbourhood is already a D-neighbourhood (inter_closed).

• master_eq : D.master = E.master

  D and E are systems over the same set of tokens Δ.

• sub {X : Set α} : D.mem X → E.mem X

  D ⊆ E: every neighbourhood of D is a neighbourhood of E.

• inter_closed {X Y : Set α} : D.mem X → D.mem Y → E.mem (X ∩ Y) → D.mem (X ∩ Y)

  Consistency in D is the same as in E: if X, Y ∈ D and X ∩ Y ∈ E, then X ∩ Y ∈ D.

def Domain.Neighborhood.«term_◁_» : Lean.TrailingParserDescr

Definition 6.10 (Scott 1981, PRG-19). The subsystem (subdomain) relation D ◁ E for two neighbourhood systems over the same token type. It records that D and E are systems over the same Δ (master_eq), that D is a subfamily of E (sub), and — the essential clause — that consistency is inherited from E: an intersection of two D-neighbourhoods that happens to be an E-neighbourhood is already a D-neighbourhood (inter_closed).

Equations

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

theorem Domain.Neighborhood.Subsystem.refl {α : Type u_1} (D : NeighborhoodSystem α) : D ◁ D

The subsystem relation is reflexive: D ◁ D. (The inter_closed clause is trivial — the hypothesis is already the conclusion.)

theorem Domain.Neighborhood.Subsystem.trans {α : Type u_1} {D E F : NeighborhoodSystem α} (h₁ : D ◁ E) (h₂ : E ◁ F) : D ◁ F

The subsystem relation is transitive: D ◁ E and E ◁ F give D ◁ F.

The inter_closed clause threads through E: from X, Y ∈ D ⊆ E and X ∩ Y ∈ F, the relation E ◁ F puts X ∩ Y ∈ E, and then D ◁ E puts X ∩ Y ∈ D.

theorem Domain.Neighborhood.NeighborhoodSystem.ext {α : Type u_1} {D E : NeighborhoodSystem α} (hmem : ∀ (X : Set α), D.mem X ↔ E.mem X) (hmaster : D.master = E.master) : D = E

Two neighbourhood systems with the same mem and the same master are equal (the remaining fields of NeighborhoodSystem are Props).

theorem Domain.Neighborhood.Subsystem.antisymm {α : Type u_1} {D E : NeighborhoodSystem α} (h₁ : D ◁ E) (h₂ : E ◁ D) : D = E

The subsystem relation is antisymmetric: D ◁ E and E ◁ D force D = E. (Mutual sub gives equal mem, and master_eq gives equal masters.)

theorem Domain.Neighborhood.Subsystem.subsystem_iff_subset_of_common {α : Type u_1} {D₀ D₁ E : NeighborhoodSystem α} (h₀ : D₀ ◁ E) (h₁ : D₁ ◁ E) : D₀ ◁ D₁ ↔ ∀ {X : Set α}, D₀.mem X → D₁.mem X

Scott's remark (the prose after Definition 6.10). Once D₀ and D₁ both sit inside a common system E as subdomains, the subdomain relation between them is just inclusion of neighbourhood families: D₀ ◁ D₁ ↔ D₀ ⊆ D₁.

• → is the sub clause of D₀ ◁ D₁.
• ← builds D₀ ◁ D₁ from D₀ ⊆ D₁: the masters agree because both equal E's master, and the inter_closed clause routes through E — an intersection X ∩ Y of D₀-neighbourhoods lying in D₁ lies in E (since D₁ ⊆ E), and D₀ ◁ E then returns it to D₀.