Specialization order and Scott topology (Scott 1972, §2 opening)

Scott's §2 begins with the specialization order on a T₀-space and the induced (Scott) topology on a complete lattice. Proposition 2.1 (monotone nets and least upper bounds) is split into its two directions; the convergence-to-below direction is the mathematically heavier half and is recorded as proposition_2_1_of_le.

Specialization order

def Domain.ContinuousLattice.SpecializationLe {X : Type u_1} [TopologicalSpace X] (x y : X) : Prop

Scott 1972, §2. The specialization order: x ⊑ y when x ∈ U open implies y ∈ U.

Equations

• Domain.ContinuousLattice.SpecializationLe x y = ∀ (U : Set X), IsOpen U → x ∈ U → y ∈ U

@[implicit_reducible]

instance Domain.ContinuousLattice.specializationPreorder {X : Type u_1} [TopologicalSpace X] : Preorder X

Equations

• Domain.ContinuousLattice.specializationPreorder = { le := Domain.ContinuousLattice.SpecializationLe, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Domain.ContinuousLattice.specializationLe_antisymm {X : Type u_1} [TopologicalSpace X] [T0Space X] {x y : X} (hxy : SpecializationLe x y) (hyx : SpecializationLe y x) : x = y

Scott topology from ScottOpen

@[reducible]

noncomputable def Domain.ContinuousLattice.scottTopologicalSpace {D : Type u_2} [CompleteLattice D] : TopologicalSpace D

Scott's induced topology on a complete lattice, realized as mathlib's Scott topology.

Equations

• Domain.ContinuousLattice.scottTopologicalSpace = Topology.scott D Set.univ

theorem Domain.ContinuousLattice.ScottOpen_iff_dirSupInacc {D : Type u_2} [CompleteLattice D] {U : Set D} : ScottOpen U ↔ IsUpperSet U ∧ DirSupInacc U

theorem Domain.ContinuousLattice.isOpen_iff_scottOpen {D : Type u_2} [CompleteLattice D] {U : Set D} : IsOpen U ↔ ScottOpen U

theorem Domain.ContinuousLattice.isOpen_scott_iff_scottOpen {D : Type u_2} [CompleteLattice D] {U : Set D} : IsOpen U ↔ ScottOpen U

Scott-open sets in our sense agree with mathlib's Scott topology (alias).

Monotone nets and Proposition 2.1

def Domain.ContinuousLattice.IsMonotoneNet {D : Type u_2} [CompleteLattice D] {ι : Type u} [Preorder ι] (x : ι → D) : Prop

A net indexed by a directed preorder that is monotone in the specialization order.

Equations

• Domain.ContinuousLattice.IsMonotoneNet x = Monotone x

def Domain.ContinuousLattice.ScottConvergesTo {D : Type u_2} [CompleteLattice D] {ι : Type u} [Preorder ι] (x : ι → D) (y : D) : Prop

Scott convergence of a monotone net to a point.

Equations

• Domain.ContinuousLattice.ScottConvergesTo x y = ∀ (U : Set D), Domain.ContinuousLattice.ScottOpen U → y ∈ U → ∃ (i : ι), ∀ j ≥ i, x j ∈ U

theorem Domain.ContinuousLattice.proposition_2_1_of_le {D : Type u_2} [CompleteLattice D] {ι : Type u} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {x : ι → D} {L y : D} [Nonempty ι] (hx : IsMonotoneNet x) (hL : IsLUB (Set.range x) L) (hyL : y ≤ L) : ScottConvergesTo x y

Scott 1972, Proposition 2.1 (backward). If y ≤ L and L is the lub of a monotone net, then the net converges to y in the Scott topology.

theorem Domain.ContinuousLattice.scottOpen_not_le {D : Type u_2} [CompleteLattice D] (L : D) : ScottOpen {z : D | ¬z ≤ L}

The complement of a principal lower set Iic L is Scott-open: it is an upper set, and it is inaccessible by directed suprema because if every member of a directed S lies below L then so does ⊔S.

theorem Domain.ContinuousLattice.proposition_2_1_le_of_converges {D : Type u_2} [CompleteLattice D] {ι : Type u} [Preorder ι] {x : ι → D} {L y : D} (hL : IsLUB (Set.range x) L) (hconv : ScottConvergesTo x y) : y ≤ L

Scott 1972, Proposition 2.1 (forward). If a monotone net converges to y in the Scott topology and L is its least upper bound, then y ≤ L.

theorem Domain.ContinuousLattice.proposition_2_1 {D : Type u_2} [CompleteLattice D] {ι : Type u} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {x : ι → D} {L y : D} [Nonempty ι] (hx : IsMonotoneNet x) (hL : IsLUB (Set.range x) L) : ScottConvergesTo x y ↔ y ≤ L

Scott 1972, Proposition 2.1. A monotone net with least upper bound L converges to y in the Scott topology iff y ⊑ L = ⊔ {xᵢ}.