The induced (Scott) topology and the way-below relation (Scott 1972, §2)

This file formalizes the core of Scott's §2 Continuous Lattices: the topology a complete lattice carries intrinsically (Scott's "induced topology", today the Scott topology), the way-below relation ≪, the basic properties of ≪ (Scott's Proposition 2.2), and the definition of a continuous lattice (Scott's Definition 2.3).

Scott defines the induced topology on a partially ordered set D by declaring U open iff

• (i) U is an upper set; and
• (ii) whenever S ⊆ D is directed (and, in this paper, non-empty), ⊔S exists and ⊔S ∈ U, then S ∩ U ≠ ∅.

He then defines x ≪ y ("x is way below y") to mean y ∈ interior {z | x ⊑ z}, the interior being taken in this induced topology. We encode "Scott-open" as the predicate ScottOpen and ≪ as WayBelow, witnessing the interior by a Scott-open neighbourhood contained in the principal up-set Set.Ici x = {z | x ≤ z}. This is faithful to Scott's topological definition (rather than the order-theoretic shortcut), and as a result Scott's Proposition 2.2 (vi) and (vii) fall straight out of the open-set axioms.

This is the classical/topological version of the theory, so we reason classically.

def Domain.ContinuousLattice.ScottOpen {D : Type u_1} [CompleteLattice D] (U : Set D) : Prop

Scott 1972, §2, the induced topology. U is Scott-open when it is an upper set and is inaccessible by suprema of non-empty directed sets: if a non-empty directed S has its supremum in U, then some member of S already lies in U.

Equations

• Domain.ContinuousLattice.ScottOpen U = (IsUpperSet U ∧ ∀ ⦃S : Set D⦄, S.Nonempty → DirectedOn (fun (x1 x2 : D) => x1 ≤ x2) S → sSup S ∈ U → (S ∩ U).Nonempty)

theorem Domain.ContinuousLattice.ScottOpen.isUpperSet {D : Type u_1} [CompleteLattice D] {U : Set D} (h : ScottOpen U) : IsUpperSet U

theorem Domain.ContinuousLattice.scottOpen_univ {D : Type u_1} [CompleteLattice D] : ScottOpen Set.univ

theorem Domain.ContinuousLattice.scottOpen_inter {D : Type u_1} [CompleteLattice D] {U V : Set D} (hU : ScottOpen U) (hV : ScottOpen V) : ScottOpen (U ∩ V)

theorem Domain.ContinuousLattice.scottOpen_sUnion {D : Type u_1} [CompleteLattice D] {C : Set (Set D)} (hC : ∀ U ∈ C, ScottOpen U) : ScottOpen (⋃₀ C)

def Domain.ContinuousLattice.WayBelow {D : Type u_1} [CompleteLattice D] (x y : D) : Prop

Scott 1972, §2. The way-below relation: x ≪ y iff y lies in the interior of the principal up-set Set.Ici x for the induced topology, witnessed by a Scott-open neighbourhood of y contained in Set.Ici x.

Equations

• Domain.ContinuousLattice.WayBelow x y = ∃ (U : Set D), Domain.ContinuousLattice.ScottOpen U ∧ y ∈ U ∧ U ⊆ Set.Ici x

def Domain.ContinuousLattice.«term_≪_» : Lean.TrailingParserDescr

Scott 1972, §2. The way-below relation: x ≪ y iff y lies in the interior of the principal up-set Set.Ici x for the induced topology, witnessed by a Scott-open neighbourhood of y contained in Set.Ici x.

Equations

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

theorem Domain.ContinuousLattice.WayBelow.le {D : Type u_1} [CompleteLattice D] {x y : D} (h : WayBelow x y) : x ≤ y

Scott 1972, Proposition 2.2(v). x ≪ y implies x ≤ y.

theorem Domain.ContinuousLattice.bot_wayBelow {D : Type u_1} [CompleteLattice D] (x : D) : WayBelow ⊥ x

Scott 1972, Proposition 2.2(i). ⊥ ≪ x for every x.

theorem Domain.ContinuousLattice.WayBelow.trans_le {D : Type u_1} [CompleteLattice D] {x y z : D} (h : WayBelow x y) (hyz : y ≤ z) : WayBelow x z

Scott 1972, Proposition 2.2(iii). x ≪ y and y ≤ z imply x ≪ z (monotone on the right).

theorem Domain.ContinuousLattice.WayBelow.le_trans {D : Type u_1} [CompleteLattice D] {x y z : D} (hxy : x ≤ y) (h : WayBelow y z) : WayBelow x z

Scott 1972, Proposition 2.2(iv). x ≤ y and y ≪ z imply x ≪ z (monotone on the left).

theorem Domain.ContinuousLattice.WayBelow.sup {D : Type u_1} [CompleteLattice D] {x y z : D} (hx : WayBelow x z) (hy : WayBelow y z) : WayBelow (x ⊔ y) z

Scott 1972, Proposition 2.2(ii). x ≪ z and y ≪ z imply x ⊔ y ≪ z.

theorem Domain.ContinuousLattice.scottOpen_wayBelow {D : Type u_1} [CompleteLattice D] (x : D) : ScottOpen {z : D | WayBelow x z}

Auxiliary: the up-set {z | x ≪ z} is itself Scott-open. (This is not Scott's Proposition 2.2(vi) — see wayBelow_self_iff_scottOpen_Ici for that — but it is a standard and useful fact, the openness of the sets ↟x.)

theorem Domain.ContinuousLattice.wayBelow_self_iff_scottOpen_Ici {D : Type u_1} [CompleteLattice D] {x : D} : WayBelow x x ↔ ScottOpen (Set.Ici x)

Scott 1972, Proposition 2.2(vi). x ≪ x iff the principal up-set {z | x ⊑ z} (i.e. Set.Ici x) is Scott-open. This characterizes the compact (finite, isolated) elements: x is compact exactly when ↑x is open.

theorem Domain.ContinuousLattice.wayBelow_sSup_iff {D : Type u_1} [CompleteLattice D] {x : D} {S : Set D} (hS : S.Nonempty) (hSdir : DirectedOn (fun (x1 x2 : D) => x1 ≤ x2) S) : WayBelow x (sSup S) ↔ ∃ y ∈ S, WayBelow x y

Scott 1972, Proposition 2.2(vii). For a non-empty directed set S, x ≪ ⊔S iff x ≪ y for some y ∈ S. The forward direction is exactly inaccessibility of a Scott-open set; the backward direction is monotonicity on the right.

def Domain.ContinuousLattice.IsContinuousLattice (D : Type u_2) [CompleteLattice D] : Prop

Scott 1972, Definition 2.3. A complete lattice D is a continuous lattice when every element is the supremum of the elements way below it: y = ⊔ {x | x ≪ y}.

Equations

• Domain.ContinuousLattice.IsContinuousLattice D = ∀ (y : D), IsLUB {x : D | Domain.ContinuousLattice.WayBelow x y} y

theorem Domain.ContinuousLattice.IsContinuousLattice.sSup_wayBelow {D : Type u_1} [CompleteLattice D] (h : IsContinuousLattice D) (y : D) : sSup {x : D | WayBelow x y} = y

In a continuous lattice, y is the actual supremum of {x | x ≪ y}.

theorem Domain.ContinuousLattice.directedOn_wayBelow {D : Type u_1} [CompleteLattice D] (y : D) : DirectedOn (fun (x1 x2 : D) => x1 ≤ x2) {x : D | WayBelow x y}

The set {x | x ≪ y} of elements way below y is directed: it is closed under binary joins by Proposition 2.2(ii) (WayBelow.sup). This holds in any complete lattice.

theorem Domain.ContinuousLattice.wayBelow_interpolate {D : Type u_1} [CompleteLattice D] (hD : IsContinuousLattice D) {a c : D} (hac : WayBelow a c) : ∃ (b : D), WayBelow a b ∧ WayBelow b c

Interpolation property of ≪. In a continuous lattice, the way-below relation interpolates: a ≪ c implies there is some b with a ≪ b ≪ c.

The proof runs Scott's standard argument: the set M = {m | ∃ x, m ≪ x ∧ x ≪ c} is directed (using directedness of {· ≪ x} twice) and has supremum c (using continuity twice). Hence a ≪ c = ⊔M with M directed forces a ≪ m for some m ∈ M, say m ≪ x ≪ c; then a ≪ m ≤ x gives a ≪ x ≪ c, so b := x works.

theorem Domain.ContinuousLattice.exists_wayBelow_subset {D : Type u_1} [CompleteLattice D] (hD : IsContinuousLattice D) {U : Set D} (hU : ScottOpen U) {z : D} (hz : z ∈ U) : ∃ (a : D), WayBelow a z ∧ {w : D | WayBelow a w} ⊆ U

In a continuous lattice the sets ↟a = {z | a ≪ z} form a basis of the Scott topology: every Scott-open U containing z contains some basic neighbourhood ↟a of z. Indeed z = ⊔{a | a ≪ z} is a directed supremum lying in the open set U, so some a ≪ z already lies in U, and then ↟a ⊆ ↑a ⊆ U.

theorem Domain.ContinuousLattice.exists_wayBelow_Ici_subset {D : Type u_1} [CompleteLattice D] (hD : IsContinuousLattice D) {U : Set D} (hU : ScottOpen U) {z : D} (hz : z ∈ U) : ∃ (a : D), WayBelow a z ∧ Set.Ici a ⊆ U

A strengthening of exists_wayBelow_subset: the witness a ≪ z can be taken with the whole principal up-set Set.Ici a (not merely ↟a) inside U. The element a produced lies in the open U, which is upper, so ↑a ⊆ U.

theorem Domain.ContinuousLattice.sInf_wayBelow {D : Type u_1} [CompleteLattice D] {U : Set D} (hU : ScottOpen U) {y : D} (hy : y ∈ U) : WayBelow (sInf U) y

The infimum of a Scott-open neighbourhood of y is way below y: the open set is itself the required witness. Scott uses this in moving between Definition 2.3 and Proposition 2.4.

theorem Domain.ContinuousLattice.isContinuousLattice_iff_isLUB_sInf_nhds {D : Type u_1} [CompleteLattice D] : IsContinuousLattice D ↔ ∀ (y : D), IsLUB {a : D | ∃ (U : Set D), ScottOpen U ∧ y ∈ U ∧ a = sInf U} y

Scott 1972, Proposition 2.4. A complete lattice is continuous iff every element is the supremum of the infima of its open neighbourhoods: y = ⊔ {⊓U : y ∈ U open}. This is Scott's alternate form of Definition 2.3.