Lower and Upper topology

This file introduces the lower topology on a preorder as the topology generated by the complements of the left-closed right-infinite intervals.

For completeness we also introduce the dual upper topology, generated by the complements of the right-closed left-infinite intervals.

Main statements

• IsLower.t0Space - the lower topology on a partial order is T₀
• IsLower.isTopologicalBasis - the complements of the upper closures of finite subsets form a basis for the lower topology
• IsLower.continuousInf - the inf map is continuous with respect to the lower topology

Implementation notes

A type synonym WithLower is introduced and for a preorder α, WithLower α is made an instance of TopologicalSpace by the topology generated by the complements of the closed intervals to infinity.

We define a mixin class IsLower for the class of types which are both a preorder and a topology and where the topology is generated by the complements of the closed intervals to infinity. It is shown that WithLower α is an instance of IsLower.

Similarly for the upper topology.

Motivation

The lower topology is used with the Scott topology to define the Lawson topology. The restriction of the lower topology to the spectrum of a complete lattice coincides with the hull-kernel topology.

References

• [Gierz et al, A Compendium of Continuous Lattices][GierzEtAl1980]

Tags

lower topology, upper topology, preorder

def Topology.lower (α : Type u_1) [Preorder α] : TopologicalSpace α

The lower topology is the topology generated by the complements of the left-closed right-infinite intervals.

Equations

• Topology.lower α = TopologicalSpace.generateFrom {s : Set α | ∃ (a : α), (Set.Ici a)ᶜ = s}

def Topology.upper (α : Type u_1) [Preorder α] : TopologicalSpace α

The upper topology is the topology generated by the complements of the right-closed left-infinite intervals.

Equations

• Topology.upper α = TopologicalSpace.generateFrom {s : Set α | ∃ (a : α), (Set.Iic a)ᶜ = s}

def Topology.WithLower (α : Type u_1) : Type u_1

Type synonym for a preorder equipped with the lower set topology.

Equations

• Topology.WithLower α = α

@[match_pattern]

def Topology.WithLower.toLower {α : Type u_1} : α ≃ Topology.WithLower α

toLower is the identity function to the WithLower of a type.

Equations

• Topology.WithLower.toLower = Equiv.refl α

@[match_pattern]

def Topology.WithLower.ofLower {α : Type u_1} : Topology.WithLower α ≃ α

ofLower is the identity function from the WithLower of a type.

Equations

• Topology.WithLower.ofLower = Equiv.refl (Topology.WithLower α)

@[simp]

theorem Topology.WithLower.to_WithLower_symm_eq {α : Type u_1} : Topology.WithLower.toLower.symm = Topology.WithLower.ofLower

@[simp]

theorem Topology.WithLower.of_WithLower_symm_eq {α : Type u_1} : Topology.WithLower.ofLower.symm = Topology.WithLower.toLower

@[simp]

theorem Topology.WithLower.toLower_ofLower {α : Type u_1} (a : Topology.WithLower α) : Topology.WithLower.toLower (Topology.WithLower.ofLower a) = a

@[simp]

theorem Topology.WithLower.ofLower_toLower {α : Type u_1} (a : α) : Topology.WithLower.ofLower (Topology.WithLower.toLower a) = a

theorem Topology.WithLower.toLower_inj {α : Type u_1} {a : α} {b : α} : Topology.WithLower.toLower a = Topology.WithLower.toLower b ↔ a = b

theorem Topology.WithLower.ofLower_inj {α : Type u_1} {a : Topology.WithLower α} {b : Topology.WithLower α} : Topology.WithLower.ofLower a = Topology.WithLower.ofLower b ↔ a = b

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

A recursor for WithLower. Use as induction x.

Equations

• Topology.WithLower.rec h a = h (Topology.WithLower.ofLower a)

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

Equations

• ⋯ = inst

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

Equations

• Topology.WithLower.instInhabited = inst

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

Equations

• Topology.WithLower.instPreorder = inst

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

Equations

• Topology.WithLower.instTopologicalSpace = Topology.lower α

theorem Topology.WithLower.isOpen_preimage_ofLower {α : Type u_1} [Preorder α] {s : Set α} : IsOpen (⇑Topology.WithLower.ofLower ⁻¹' s) ↔ TopologicalSpace.IsOpen s

theorem Topology.WithLower.isOpen_def {α : Type u_1} [Preorder α] (T : Set (Topology.WithLower α)) : IsOpen T ↔ TopologicalSpace.IsOpen (⇑Topology.WithLower.toLower ⁻¹' T)

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

Type synonym for a preorder equipped with the upper topology.

Equations

• Topology.WithUpper α = α

@[match_pattern]

def Topology.WithUpper.toUpper {α : Type u_1} : α ≃ Topology.WithUpper α

toUpper is the identity function to the WithUpper of a type.

Equations

• Topology.WithUpper.toUpper = Equiv.refl α

@[match_pattern]

def Topology.WithUpper.ofUpper {α : Type u_1} : Topology.WithUpper α ≃ α

ofUpper is the identity function from the WithUpper of a type.

Equations

• Topology.WithUpper.ofUpper = Equiv.refl (Topology.WithUpper α)

@[simp]

theorem Topology.WithUpper.to_WithUpper_symm_eq {α : Type u_3} : Topology.WithUpper.toUpper.symm = Topology.WithUpper.ofUpper

@[simp]

theorem Topology.WithUpper.of_WithUpper_symm_eq {α : Type u_1} : Topology.WithUpper.ofUpper.symm = Topology.WithUpper.toUpper

@[simp]

theorem Topology.WithUpper.toUpper_ofUpper {α : Type u_1} (a : Topology.WithUpper α) : Topology.WithUpper.toUpper (Topology.WithUpper.ofUpper a) = a

@[simp]

theorem Topology.WithUpper.ofUpper_toUpper {α : Type u_1} (a : α) : Topology.WithUpper.ofUpper (Topology.WithUpper.toUpper a) = a

theorem Topology.WithUpper.toUpper_inj {α : Type u_1} {a : α} {b : α} : Topology.WithUpper.toUpper a = Topology.WithUpper.toUpper b ↔ a = b

theorem Topology.WithUpper.ofUpper_inj {α : Type u_1} {a : Topology.WithUpper α} {b : Topology.WithUpper α} : Topology.WithUpper.ofUpper a = Topology.WithUpper.ofUpper b ↔ a = b

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

A recursor for WithUpper. Use as induction x.

Equations

• Topology.WithUpper.rec h a = h (Topology.WithUpper.ofUpper a)

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

Equations

• ⋯ = inst

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

Equations

• Topology.WithUpper.instInhabited = inst

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

Equations

• Topology.WithUpper.instPreorder = inst

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

Equations

• Topology.WithUpper.instTopologicalSpace = Topology.upper α

theorem Topology.WithUpper.isOpen_preimage_ofUpper {α : Type u_1} [Preorder α] {s : Set α} : IsOpen (⇑Topology.WithUpper.ofUpper ⁻¹' s) ↔ TopologicalSpace.IsOpen s

theorem Topology.WithUpper.isOpen_def {α : Type u_1} [Preorder α] {s : Set (Topology.WithUpper α)} : IsOpen s ↔ TopologicalSpace.IsOpen (⇑Topology.WithUpper.toUpper ⁻¹' s)

class Topology.IsLower (α : Type u_3) [t : TopologicalSpace α] [Preorder α] : Prop

The lower topology is the topology generated by the complements of the left-closed right-infinite intervals.

• topology_eq_lowerTopology : t = Topology.lower α

theorem Topology.IsLower.topology_eq_lowerTopology {α : Type u_3} {t : TopologicalSpace α} : ∀ {inst : Preorder α} [self : Topology.IsLower α], t = Topology.lower α

class Topology.IsUpper (α : Type u_3) [t : TopologicalSpace α] [Preorder α] : Prop

The upper topology is the topology generated by the complements of the right-closed left-infinite intervals.

• topology_eq_upperTopology : t = Topology.upper α

theorem Topology.IsUpper.topology_eq_upperTopology {α : Type u_3} {t : TopologicalSpace α} : ∀ {inst : Preorder α} [self : Topology.IsUpper α], t = Topology.upper α

instance Topology.instIsLowerWithLower {α : Type u_1} [Preorder α] : Topology.IsLower (Topology.WithLower α)

Equations

• ⋯ = ⋯

instance Topology.instIsUpperWithUpper {α : Type u_1} [Preorder α] : Topology.IsUpper (Topology.WithUpper α)

Equations

• ⋯ = ⋯

def Topology.WithLower.toDualHomeomorph {α : Type u_1} [Preorder α] : Topology.WithLower α ≃ₜ Topology.WithUpper αᵒᵈ

The lower topology is homeomorphic to the upper topology on the dual order

Equations

• Topology.WithLower.toDualHomeomorph = { toFun := ⇑OrderDual.toDual, invFun := ⇑OrderDual.ofDual, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Topology.IsLower.lowerBasis (α : Type u_3) [Preorder α] : Set (Set α)

The complements of the upper closures of finite sets are a collection of lower sets which form a basis for the lower topology.

Equations

• Topology.IsLower.lowerBasis α = {s : Set α | ∃ (t : Set α), t.Finite ∧ (↑(upperClosure t))ᶜ = s}

theorem Topology.IsLower.topology_eq (α : Type u_1) [Preorder α] [TopologicalSpace α] [Topology.IsLower α] : inst✝¹ = Topology.lower α

def Topology.IsLower.withLowerHomeomorph {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] : Topology.WithLower α ≃ₜ α

If α is equipped with the lower topology, then it is homeomorphic to WithLower α.

Equations

• Topology.IsLower.withLowerHomeomorph = Topology.WithLower.ofLower.toHomeomorphOfIsInducing ⋯

theorem Topology.IsLower.isOpen_iff_generate_Ici_compl {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] {s : Set α} : IsOpen s ↔ TopologicalSpace.GenerateOpen {t : Set α | ∃ (a : α), (Set.Ici a)ᶜ = t} s

instance OrderDual.instIsUpper {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] : Topology.IsUpper αᵒᵈ

Equations

• ⋯ = ⋯

instance Topology.IsLower.instClosedIciTopology {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] : ClosedIciTopology α

Left-closed right-infinite intervals [a, ∞) are closed in the lower topology.

Equations

• ⋯ = ⋯

theorem Topology.IsLower.isClosed_upperClosure {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] {s : Set α} (h : s.Finite) : IsClosed ↑(upperClosure s)

The upper closure of a finite set is closed in the lower topology.

theorem Topology.IsLower.isLowerSet_of_isOpen {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] {s : Set α} (h : IsOpen s) : IsLowerSet s

Every set open in the lower topology is a lower set.

theorem Topology.IsLower.isUpperSet_of_isClosed {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] {s : Set α} (h : IsClosed s) : IsUpperSet s

@[simp]

theorem Topology.IsLower.closure_singleton {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] (a : α) : closure {a} = Set.Ici a

The closure of a singleton {a} in the lower topology is the left-closed right-infinite interval [a, ∞).

theorem Topology.IsLower.isTopologicalBasis {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] : TopologicalSpace.IsTopologicalBasis (Topology.IsLower.lowerBasis α)

theorem Topology.IsLower.continuous_iff_Ici {α : Type u_1} {β : Type u_2} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Set.Ici a)

A function f : β → α with lower topology in the codomain is continuous if and only if the preimage of every interval Set.Ici a is a closed set.

@[instance 90]

instance Topology.IsLower.t0Space {α : Type u_1} [PartialOrder α] [TopologicalSpace α] [Topology.IsLower α] : T0Space α

The lower topology on a partial order is T₀.

Equations

• ⋯ = ⋯

theorem Topology.IsLower.isTopologicalBasis_insert_univ_subbasis {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [Topology.IsLower α] : TopologicalSpace.IsTopologicalBasis (insert Set.univ {s : Set α | ∃ (a : α), (Set.Ici a)ᶜ = s})

theorem Topology.IsLower.isTopologicalSpace_basis {α : Type u_1} [CompleteLinearOrder α] [t : TopologicalSpace α] [Topology.IsLower α] (U : Set α) : IsOpen U ↔ U = Set.univ ∨ ∃ (a : α), (Set.Ici a)ᶜ = U

def Topology.IsUpper.upperBasis (α : Type u_3) [Preorder α] : Set (Set α)

The complements of the lower closures of finite sets are a collection of upper sets which form a basis for the upper topology.

Equations

• Topology.IsUpper.upperBasis α = {s : Set α | ∃ (t : Set α), t.Finite ∧ (↑(lowerClosure t))ᶜ = s}

theorem Topology.IsUpper.topology_eq (α : Type u_1) [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] : inst✝¹ = Topology.upper α

def Topology.IsUpper.withUpperHomeomorph {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] : Topology.WithUpper α ≃ₜ α

If α is equipped with the upper topology, then it is homeomorphic to WithUpper α.

Equations

• Topology.IsUpper.withUpperHomeomorph = Topology.WithUpper.ofUpper.toHomeomorphOfIsInducing ⋯

theorem Topology.IsUpper.isOpen_iff_generate_Iic_compl {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] {s : Set α} : IsOpen s ↔ TopologicalSpace.GenerateOpen {t : Set α | ∃ (a : α), (Set.Iic a)ᶜ = t} s

instance OrderDual.instIsLower {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] : Topology.IsLower αᵒᵈ

Equations

• ⋯ = ⋯

instance Topology.IsUpper.instClosedIicTopology {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] : ClosedIicTopology α

Left-infinite right-closed intervals (-∞,a] are closed in the upper topology.

Equations

• ⋯ = ⋯

theorem Topology.IsUpper.isClosed_lowerClosure {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] {s : Set α} (h : s.Finite) : IsClosed ↑(lowerClosure s)

The lower closure of a finite set is closed in the upper topology.

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

Every set open in the upper topology is a upper set.

theorem Topology.IsUpper.isLowerSet_of_isClosed {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] {s : Set α} (h : IsClosed s) : IsLowerSet s

@[simp]

theorem Topology.IsUpper.closure_singleton {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] (a : α) : closure {a} = Set.Iic a

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

theorem Topology.IsUpper.isTopologicalBasis {α : Type u_1} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] : TopologicalSpace.IsTopologicalBasis (Topology.IsUpper.upperBasis α)

theorem Topology.IsUpper.continuous_iff_Iic {α : Type u_1} {β : Type u_2} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Set.Iic a)

A function f : β → α with upper topology in the codomain is continuous if and only if the preimage of every interval Set.Iic a is a closed set.

@[instance 90]

instance Topology.IsUpper.t0Space {α : Type u_1} [PartialOrder α] [TopologicalSpace α] [Topology.IsUpper α] : T0Space α

The upper topology on a partial order is T₀.

Equations

• ⋯ = ⋯

theorem Topology.IsUpper.isTopologicalBasis_insert_univ_subbasis {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [Topology.IsUpper α] : TopologicalSpace.IsTopologicalBasis (insert Set.univ {s : Set α | ∃ (a : α), (Set.Iic a)ᶜ = s})

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

instance Topology.instIsLowerProd {α : Type u_1} {β : Type u_2} [Preorder α] [TopologicalSpace α] [Topology.IsLower α] [OrderBot α] [Preorder β] [TopologicalSpace β] [Topology.IsLower β] [OrderBot β] : Topology.IsLower (α × β)

Equations

• ⋯ = ⋯

instance Topology.instIsUpperProd {α : Type u_1} {β : Type u_2} [Preorder α] [TopologicalSpace α] [Topology.IsUpper α] [OrderTop α] [Preorder β] [TopologicalSpace β] [Topology.IsUpper β] [OrderTop β] : Topology.IsUpper (α × β)

Equations

• ⋯ = ⋯

theorem sInfHom.continuous {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] [TopologicalSpace α] [Topology.IsLower α] [TopologicalSpace β] [Topology.IsLower β] (f : sInfHom α β) : Continuous ⇑f

@[instance 90]

instance Topology.IsLower.toContinuousInf {α : Type u_1} [CompleteLattice α] [TopologicalSpace α] [Topology.IsLower α] : ContinuousInf α

Equations

• ⋯ = ⋯

theorem sSupHom.continuous {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] [TopologicalSpace α] [Topology.IsUpper α] [TopologicalSpace β] [Topology.IsUpper β] (f : sSupHom α β) : Continuous ⇑f

@[instance 90]

instance Topology.IsUpper.toContinuousInf {α : Type u_1} [CompleteLattice α] [TopologicalSpace α] [Topology.IsUpper α] : ContinuousSup α

Equations

• ⋯ = ⋯

theorem Topology.isUpper_orderDual {α : Type u_1} [Preorder α] [TopologicalSpace α] : Topology.IsUpper αᵒᵈ ↔ Topology.IsLower α

theorem Topology.isLower_orderDual {α : Type u_1} [Preorder α] [TopologicalSpace α] : Topology.IsLower αᵒᵈ ↔ Topology.IsUpper α

instance instIsUpperProp : Topology.IsUpper Prop

The Sierpiński topology on Prop is the upper topology

Equations

• instIsUpperProp = ⋯