Scott topology

This file introduces the Scott topology on a preorder.

Main definitions

• Topology.scottHausdorff: the Scott-Hausdorff topology is the topology whose closed sets are DirSupClosed, i.e. closed under directed suprema.
• 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 w.r.t. the Scott topology are monotone.
• Topology.IsScott.scottContinuousOn_iff_continuous - a function is Scott continuous (preserves least upper bounds of directed sets) if and only if it is continuous w.r.t. 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).

References

• Abramsky and Jung, Domain Theory
• Gierz et al, A Compendium of Continuous Lattices
• Karner, Continuous monoids and semirings

Tags

Scott topology, preorder

Scott-Hausdorff topology

@[implicit_reducible]

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✝ = scottHausdorff α D

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

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

theorem Topology.IsScottHausdorff.isOpen_iff {α : Type u_1} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] {s : Set α} [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 α} [IsScottHausdorff α D] (h : IsOpen s) : DirSupInaccOn D s

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

theorem Topology.IsScottHausdorff.isOpen_iff_dirSupInacc {α : Type u_1} [Preorder α] [TopologicalSpace α] {s : Set α} [IsScottHausdorff α Set.univ] : IsOpen s ↔ DirSupInacc s

theorem Topology.IsScottHausdorff.isClosed_iff_dirSupClosed {α : Type u_1} [Preorder α] [TopologicalSpace α] {s : Set α} [IsScottHausdorff α Set.univ] : IsClosed s ↔ DirSupClosed s

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

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

Scott topology

@[implicit_reducible]

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 α] : upperSet α ≤ scott α Set.univ

theorem Topology.scottHausdorff_le_scott {α : Type u_1} [Preorder α] : scottHausdorff α Set.univ ≤ 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✝ = scott α D

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

theorem Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open {α : Type u_1} {D : Set (Set α)} [Preorder α] [TopologicalSpace α] {s : Set α} [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 α} [IsScott α D] : IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s

theorem Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed {α : Type u_1} [Preorder α] [TopologicalSpace α] {s : Set α} [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 α} [IsScott α D] : IsOpen s → IsUpperSet s

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

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

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

instance Topology.IsScott.instClosedIicTopologyOfUnivSet {α : Type u_1} [Preorder α] [TopologicalSpace α] [IsScott α Set.univ] : ClosedIicTopology α

@[simp]

theorem Topology.IsScott.closure_singleton {α : Type u_1} [Preorder α] [TopologicalSpace α] {a : α} [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 β] [IsScott β Set.univ] {f : α → β} [IsScott α D] (hf : Continuous f) : Monotone f

@[simp]

theorem Topology.IsScott.scottContinuousOn_iff_continuous {α : Type u_1} {β : Type u_2} [Preorder α] [TopologicalSpace α] [Preorder β] [TopologicalSpace β] [IsScott β Set.univ] {f : α → β} {D : Set (Set α)} [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 α] [IsScott α Set.univ] : T0Space α

The Scott topology on a partial order is T₀.

theorem Topology.IsScott.isOpen_iff_Iic_compl_or_univ {α : Type u_1} [CompleteLinearOrder α] [TopologicalSpace α] [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 α] : scott α Set.univ = upper α

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

theorem Topology.IsScott.isOpen_iff_scottContinuous_mem {α : Type u_1} [Preorder α] {s : Set α} [TopologicalSpace α] [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} : α ≃ 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} : 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} : toScott.symm = ofScott

@[simp]

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

@[simp]

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

@[simp]

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

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

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

def Topology.WithScott.rec {α : Type u_1} {β : WithScott α → Sort u_3} (h : (a : α) → β (toScott a)) (a : 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 (WithScott α)

@[implicit_reducible]

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

Equations

• Topology.WithScott.instInhabited = inst✝

@[implicit_reducible]

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

Equations

• Topology.WithScott.instPreorder = inst✝

@[implicit_reducible]

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

Equations

• Topology.WithScott.instTopologicalSpace = Topology.WithScott.instTopologicalSpace._aux_1

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

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

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

def Topology.IsScott.withScottHomeomorph {α : Type u_1} [Preorder α] [TopologicalSpace α] [IsScott α Set.univ] : 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 α] [IsScott α Set.univ] : scottHausdorff α Set.univ ≤ inst✝

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