Scott topology

This file introduces the Scott topology on a preorder.

Main definitions

• DirSupInacc - a set u is said to be inaccessible by directed joins if, when the least upper bound of a directed set d lies in u then d has non-empty intersection with u.
• DirSupClosed - a set s is said to be closed under directed joins if, whenever a directed set d has a least upper bound a and is a subset of s then a also lies in s.
• Topology.scott - the Scott topology is defined as the join of the topology of upper sets and the Scott-Hausdorff topology (the topological space where a set u is open if, when the least upper bound of a directed set d lies in u then there is a tail of d which is a subset of u).

Main statements

• Topology.IsScott.isUpperSet_of_isOpen: Scott open sets are upper.
• Topology.IsScott.isLowerSet_of_isClosed: Scott closed sets are lower.
• Topology.IsScott.monotone_of_continuous: Functions continuous wrt the Scott topology are monotone.
• Topology.IsScott.scottContinuous_iff_continuous - a function is Scott continuous (preserves least upper bounds of directed sets) if and only if it is continuous wrt the Scott topology.
• Topology.IsScott.instT0Space - the Scott topology on a partial order is T₀.

Implementation notes

A type synonym WithScott is introduced and for a preorder α, WithScott α is made an instance of TopologicalSpace by the scott topology.

We define a mixin class IsScott for the class of types which are both a preorder and a topology and where the topology is the scott topology. It is shown that WithScott α is an instance of IsScott.

A class Scott is defined in Topology/OmegaCompletePartialOrder and made an instance of a topological space by defining the open sets to be those which have characteristic functions which are monotone and preserve limits of countable chains (OmegaCompletePartialOrder.Continuous'). A Scott continuous function between OmegaCompletePartialOrders is always OmegaCompletePartialOrder.Continuous' (OmegaCompletePartialOrder.ScottContinuous.continuous'). The converse is true in some special cases, but not in general ([Domain Theory, 2.2.4][abramsky_gabbay_maibaum_1994]).

References

• [Abramsky and Jung, Domain Theory][abramsky_gabbay_maibaum_1994]
• [Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980]
• [Karner, Continuous monoids and semirings][Karner2004]

Tags

Scott topology, preorder

Prerequisite order properties

def DirSupInaccOn {α : Type u_1} [Preorder α] (D : Set (Set α)) (s : Set α) : Prop

A set s is said to be inaccessible by directed joins on D if, when the least upper bound of a directed set d in D lies in s then d has non-empty intersection with s.

Equations

• DirSupInaccOn D s = ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

def DirSupInacc {α : Type u_1} [Preorder α] (s : Set α) : Prop

A set s is said to be inaccessible by directed joins if, when the least upper bound of a directed set d lies in s then d has non-empty intersection with s.

Equations

• DirSupInacc s = ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

@[simp]

theorem dirSupInaccOn_univ {α : Type u_1} [Preorder α] {s : Set α} : DirSupInaccOn Set.univ s ↔ DirSupInacc s

@[simp]

theorem DirSupInacc.dirSupInaccOn {α : Type u_1} [Preorder α] {s : Set α} {D : Set (Set α)} : DirSupInacc s → DirSupInaccOn D s

theorem DirSupInaccOn.mono {α : Type u_1} [Preorder α] {s : Set α} {D₁ : Set (Set α)} {D₂ : Set (Set α)} (hD : D₁ ⊆ D₂) (hf : DirSupInaccOn D₂ s) : DirSupInaccOn D₁ s

def DirSupClosed {α : Type u_1} [Preorder α] (s : Set α) : Prop

A set s is said to be closed under directed joins if, whenever a directed set d has a least upper bound a and is a subset of s then a also lies in s.

Equations

• DirSupClosed s = ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → d ⊆ s → a ∈ s

@[simp]

theorem dirSupInacc_compl {α : Type u_1} [Preorder α] {s : Set α} : DirSupInacc sᶜ ↔ DirSupClosed s

@[simp]

theorem dirSupClosed_compl {α : Type u_1} [Preorder α] {s : Set α} : DirSupClosed sᶜ ↔ DirSupInacc s

theorem DirSupClosed.compl {α : Type u_1} [Preorder α] {s : Set α} : DirSupClosed s → DirSupInacc sᶜ

Alias of the reverse direction of dirSupInacc_compl.

theorem DirSupInacc.of_compl {α : Type u_1} [Preorder α] {s : Set α} : DirSupInacc sᶜ → DirSupClosed s

Alias of the forward direction of dirSupInacc_compl.

theorem DirSupInacc.compl {α : Type u_1} [Preorder α] {s : Set α} : DirSupInacc s → DirSupClosed sᶜ

Alias of the reverse direction of dirSupClosed_compl.

theorem DirSupClosed.of_compl {α : Type u_1} [Preorder α] {s : Set α} : DirSupClosed sᶜ → DirSupInacc s

Alias of the forward direction of dirSupClosed_compl.

theorem DirSupClosed.inter {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (hs : DirSupClosed s) (ht : DirSupClosed t) : DirSupClosed (s ∩ t)

theorem DirSupInacc.union {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∪ t)

theorem IsUpperSet.dirSupClosed {α : Type u_1} [Preorder α] {s : Set α} (hs : IsUpperSet s) : DirSupClosed s

theorem IsLowerSet.dirSupInacc {α : Type u_1} [Preorder α] {s : Set α} (hs : IsLowerSet s) : DirSupInacc s

theorem dirSupClosed_Iic {α : Type u_1} [Preorder α] (a : α) : DirSupClosed (Set.Iic a)

theorem dirSupInacc_iff_forall_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} : DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty

theorem dirSupClosed_iff_forall_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} : DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → d ⊆ s → sSup d ∈ s

Scott-Hausdorff topology

def Topology.scottHausdorff (α : Type u_3) (D : Set (Set α)) [Preorder α] : TopologicalSpace α

The Scott-Hausdorff topology.

A set u is open in the Scott-Hausdorff topology iff when the least upper bound of a directed set d lies in u then there is a tail of d which is a subset of u.

Equations

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

class Topology.IsScottHausdorff (α : Type u_1) (D : Set (Set α)) [Preorder α] [TopologicalSpace α] : Prop

Predicate for an ordered topological space to be equipped with its Scott-Hausdorff topology.

A set u is open in the Scott-Hausdorff topology iff when the least upper bound of a directed set d lies in u then there is a tail of d which is a subset of u.

• topology_eq_scottHausdorff : inst✝ = Topology.scottHausdorff α D

theorem Topology.IsScottHausdorff.topology_eq_scottHausdorff {α : Type u_1} {D : Set (Set α)} : ∀ {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : Topology.IsScottHausdorff α D], inst_1 = Topology.scottHausdorff α D

instance Topology.instIsScottHausdorff (α : Type u_1) (D : Set (Set α)) [Preorder α] : Topology.IsScottHausdorff α D

Equations

• ⋯ = ⋯

theorem Topology.IsScottHausdorff.topology_eq (α : Type u_1) (D : Set (Set α)) [Preorder α] [TopologicalSpace α] [Topology.IsScottHausdorff α D] : inst✝¹ = Topology.scottHausdorff α D

theorem Topology.IsScottHausdorff.isOpen_iff {α : Type u_1} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScottHausdorff α D] : IsOpen s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s

theorem Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen {α : Type u_1} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScottHausdorff α D] (h : IsOpen s) : DirSupInaccOn D s

theorem Topology.IsScottHausdorff.dirSupClosed_of_isClosed {α : Type u_1} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScottHausdorff α Set.univ] (h : IsClosed s) : DirSupClosed s

theorem Topology.IsScottHausdorff.isOpen_of_isLowerSet {α : Type u_1} {s : Set α} [Preorder α] {t : TopologicalSpace α} [Topology.IsScottHausdorff α Set.univ] (h : IsLowerSet s) : IsOpen s

theorem Topology.IsScottHausdorff.isClosed_of_isUpperSet {α : Type u_1} {s : Set α} [Preorder α] {t : TopologicalSpace α} [Topology.IsScottHausdorff α Set.univ] (h : IsUpperSet s) : IsClosed s

Scott topology

def Topology.scott (α : Type u_3) (D : Set (Set α)) [Preorder α] : TopologicalSpace α

The Scott topology.

It is defined as the join of the topology of upper sets and the Scott-Hausdorff topology.

Equations

• Topology.scott α D = Topology.upperSet α ⊔ Topology.scottHausdorff α D

theorem Topology.upperSet_le_scott {α : Type u_1} [Preorder α] : Topology.upperSet α ≤ Topology.scott α Set.univ

theorem Topology.scottHausdorff_le_scott {α : Type u_1} [Preorder α] : Topology.scottHausdorff α Set.univ ≤ Topology.scott α Set.univ

class Topology.IsScott (α : Type u_1) (D : Set (Set α)) [Preorder α] [TopologicalSpace α] : Prop

Predicate for an ordered topological space to be equipped with its Scott topology.

The Scott topology is defined as the join of the topology of upper sets and the Scott Hausdorff topology.

• topology_eq_scott : inst✝ = Topology.scott α D

theorem Topology.IsScott.topology_eq_scott {α : Type u_1} {D : Set (Set α)} : ∀ {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : Topology.IsScott α D], inst_1 = Topology.scott α D

theorem Topology.IsScott.topology_eq (α : Type u_1) (D : Set (Set α)) [Preorder α] [TopologicalSpace α] [Topology.IsScott α D] : inst✝¹ = Topology.scott α D

theorem Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open {α : Type u_1} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScott α D] : IsOpen s ↔ IsUpperSet s ∧ IsOpen s

theorem Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn {α : Type u_1} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScott α D] : IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s

theorem Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed {α : Type u_1} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScott α Set.univ] : IsClosed s ↔ IsLowerSet s ∧ DirSupClosed s

theorem Topology.IsScott.isUpperSet_of_isOpen {α : Type u_1} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScott α D] : IsOpen s → IsUpperSet s

theorem Topology.IsScott.isLowerSet_of_isClosed {α : Type u_1} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScott α Set.univ] : IsClosed s → IsLowerSet s

theorem Topology.IsScott.dirSupClosed_of_isClosed {α : Type u_1} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScott α Set.univ] : IsClosed s → DirSupClosed s

theorem Topology.IsScott.lowerClosure_subset_closure {α : Type u_1} [Preorder α] [TopologicalSpace α] {s : Set α} [Topology.IsScott α Set.univ] : ↑(lowerClosure s) ⊆ closure s

theorem Topology.IsScott.isClosed_Iic {α : Type u_1} [Preorder α] [TopologicalSpace α] {a : α} [Topology.IsScott α Set.univ] : IsClosed (Set.Iic a)

@[simp]

theorem Topology.IsScott.closure_singleton {α : Type u_1} [Preorder α] [TopologicalSpace α] {a : α} [Topology.IsScott α Set.univ] : closure {a} = Set.Iic a

The closure of a singleton {a} in the Scott topology is the right-closed left-infinite interval (-∞,a].

theorem Topology.IsScott.monotone_of_continuous {α : Type u_1} {β : Type u_2} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] [Preorder β] [TopologicalSpace β] [Topology.IsScott β Set.univ] {f : α → β} [Topology.IsScott α D] (hf : Continuous f) : Monotone f

@[simp]

theorem Topology.IsScott.scottContinuous_iff_continuous {α : Type u_1} {β : Type u_2} [Preorder α] [TopologicalSpace α] [Preorder β] [TopologicalSpace β] [Topology.IsScott β Set.univ] {f : α → β} {D : Set (Set α)} [Topology.IsScott α D] (hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D) : ScottContinuousOn D f ↔ Continuous f

@[instance 90]

instance Topology.IsScott.instT0Space {α : Type u_1} [PartialOrder α] [TopologicalSpace α] [Topology.IsScott α Set.univ] : T0Space α

The Scott topology on a partial order is T₀.

Equations

• ⋯ = ⋯

theorem Topology.IsScott.isOpen_iff_Iic_compl_or_univ {α : Type u_1} [CompleteLinearOrder α] [TopologicalSpace α] [Topology.IsScott α Set.univ] (U : Set α) : IsOpen U ↔ U = Set.univ ∨ ∃ (a : α), (Set.Iic a)ᶜ = U

theorem Topology.IsScott.scott_eq_upper_of_completeLinearOrder {α : Type u_1} [CompleteLinearOrder α] : Topology.scott α Set.univ = Topology.upper α

instance Topology.IsScott.instUnivSetOfIsUpper {α : Type u_1} [CompleteLinearOrder α] [TopologicalSpace α] [Topology.IsUpper α] : Topology.IsScott α Set.univ

Equations

• ⋯ = ⋯

theorem Topology.IsScott.isOpen_iff_scottContinuous_mem {α : Type u_1} [Preorder α] {s : Set α} [TopologicalSpace α] [Topology.IsScott α Set.univ] : IsOpen s ↔ ScottContinuous fun (x : α) => x ∈ s

def Topology.WithScott (α : Type u_3) : Type u_3

Type synonym for a preorder equipped with the Scott topology

Equations

• Topology.WithScott α = α

@[match_pattern]

def Topology.WithScott.toScott {α : Type u_1} : α ≃ Topology.WithScott α

toScott is the identity function to the WithScott of a type.

Equations

• Topology.WithScott.toScott = Equiv.refl α

@[match_pattern]

def Topology.WithScott.ofScott {α : Type u_1} : Topology.WithScott α ≃ α

ofScott is the identity function from the WithScott of a type.

Equations

• Topology.WithScott.ofScott = Equiv.refl (Topology.WithScott α)

@[simp]

theorem Topology.WithScott.toScott_symm_eq {α : Type u_1} : Topology.WithScott.toScott.symm = Topology.WithScott.ofScott

@[simp]

theorem Topology.WithScott.ofScott_symm_eq {α : Type u_1} : Topology.WithScott.ofScott.symm = Topology.WithScott.toScott

@[simp]

theorem Topology.WithScott.toScott_ofScott {α : Type u_1} (a : Topology.WithScott α) : Topology.WithScott.toScott (Topology.WithScott.ofScott a) = a

@[simp]

theorem Topology.WithScott.ofScott_toScott {α : Type u_1} (a : α) : Topology.WithScott.ofScott (Topology.WithScott.toScott a) = a

@[simp]

theorem Topology.WithScott.toScott_inj {α : Type u_1} {a : α} {b : α} : Topology.WithScott.toScott a = Topology.WithScott.toScott b ↔ a = b

@[simp]

theorem Topology.WithScott.ofScott_inj {α : Type u_1} {a : Topology.WithScott α} {b : Topology.WithScott α} : Topology.WithScott.ofScott a = Topology.WithScott.ofScott b ↔ a = b

def Topology.WithScott.rec {α : Type u_1} {β : Topology.WithScott α → Sort u_3} (h : (a : α) → β (Topology.WithScott.toScott a)) (a : Topology.WithScott α) : β a

A recursor for WithScott. Use as induction x.

Equations

• Topology.WithScott.rec h a = h (Topology.WithScott.ofScott a)

instance Topology.WithScott.instNonempty {α : Type u_1} [Nonempty α] : Nonempty (Topology.WithScott α)

Equations

• ⋯ = inst

instance Topology.WithScott.instInhabited {α : Type u_1} [Inhabited α] : Inhabited (Topology.WithScott α)

Equations

• Topology.WithScott.instInhabited = inst

instance Topology.WithScott.instPreorder {α : Type u_1} [Preorder α] : Preorder (Topology.WithScott α)

Equations

• Topology.WithScott.instPreorder = inst

instance Topology.WithScott.instTopologicalSpace {α : Type u_1} [Preorder α] : TopologicalSpace (Topology.WithScott α)

Equations

• Topology.WithScott.instTopologicalSpace = Topology.scott α Set.univ

instance Topology.WithScott.instIsScottUnivSet {α : Type u_1} [Preorder α] : Topology.IsScott (Topology.WithScott α) Set.univ

Equations

• ⋯ = ⋯

theorem Topology.WithScott.isOpen_iff_isUpperSet_and_scottHausdorff_open' {α : Type u_1} [Preorder α] {u : Set α} : IsOpen (⇑Topology.WithScott.ofScott ⁻¹' u) ↔ IsUpperSet u ∧ TopologicalSpace.IsOpen u

theorem Topology.scottHausdorff_le_lower {α : Type u_1} [Preorder α] : Topology.scottHausdorff α Set.univ ≤ Topology.lower α

def Topology.IsScott.withScottHomeomorph {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsScott α Set.univ] : Topology.WithScott α ≃ₜ α

If α is equipped with the Scott topology, then it is homeomorphic to WithScott α.

Equations

• Topology.IsScott.withScottHomeomorph = Topology.WithScott.ofScott.toHomeomorphOfIsInducing ⋯

theorem Topology.IsScott.scottHausdorff_le {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsScott α Set.univ] : Topology.scottHausdorff α Set.univ ≤ inst✝¹

theorem Topology.IsLower.scottHausdorff_le {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] : Topology.scottHausdorff α Set.univ ≤ inst✝¹