mathlib3 documentation

topology.order.lower_topology

Lower topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file introduces the lower topology on a preorder as the topology generated by the complements of the closed intervals to infinity.

Main statements #

lower_topology.t0_space - the lower topology on a partial order is T₀
is_topological_basis.is_topological_basis - the complements of the upper closures of finite subsets form a basis for the lower topology
lower_topology.to_has_continuous_inf - the inf map is continuous with respect to the lower topology

Implementation notes #

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

We define a mixin class lower_topology 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 with_lower_topology α is an instance of lower_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

Tags #

lower topology, preorder

def with_lower_topology (α : Type u_1) :

Type u_1

Type synonym for a preorder equipped with the lower topology

Equations

with_lower_topology α = α

Instances for with_lower_topology

def with_lower_topology.to_lower {α : Type u_1} :

α ≃ with_lower_topology α

to_lower is the identity function to the with_lower_topology of a type.

Equations

with_lower_topology.to_lower = equiv.refl α

def with_lower_topology.of_lower {α : Type u_1} :

with_lower_topology α ≃ α

of_lower is the identity function from the with_lower_topology of a type.

Equations

with_lower_topology.of_lower = equiv.refl (with_lower_topology α)

@[simp]

theorem with_lower_topology.to_with_lower_topology_symm_eq {α : Type u_1} :

with_lower_topology.to_lower.symm = with_lower_topology.of_lower

@[simp]

theorem with_lower_topology.of_with_lower_topology_symm_eq {α : Type u_1} :

with_lower_topology.of_lower.symm = with_lower_topology.to_lower

@[simp]

theorem with_lower_topology.to_lower_of_lower {α : Type u_1} (a : with_lower_topology α) :

⇑with_lower_topology.to_lower (⇑with_lower_topology.of_lower a) = a

@[simp]

theorem with_lower_topology.of_lower_to_lower {α : Type u_1} (a : α) :

⇑with_lower_topology.of_lower (⇑with_lower_topology.to_lower a) = a

@[simp]

theorem with_lower_topology.to_lower_inj {α : Type u_1} {a b : α} :

⇑with_lower_topology.to_lower a = ⇑with_lower_topology.to_lower b ↔ a = b

@[simp]

theorem with_lower_topology.of_lower_inj {α : Type u_1} {a b : with_lower_topology α} :

⇑with_lower_topology.of_lower a = ⇑with_lower_topology.of_lower b ↔ a = b

@[protected]

def with_lower_topology.rec {α : Type u_1} {β : with_lower_topology α → Sort u_2} (h : Π (a : α), β (⇑with_lower_topology.to_lower a)) (a : with_lower_topology α) :

β a

A recursor for with_lower_topology. Use as induction x using with_lower_topology.rec.

Equations

with_lower_topology.rec h = λ (a : with_lower_topology α), h (⇑with_lower_topology.of_lower a)

@[protected, instance]

def with_lower_topology.nonempty {α : Type u_1} [nonempty α] :

nonempty (with_lower_topology α)

@[protected, instance]

def with_lower_topology.inhabited {α : Type u_1} [inhabited α] :

inhabited (with_lower_topology α)

Equations

with_lower_topology.inhabited = _inst_1

@[protected, instance]

def with_lower_topology.preorder {α : Type u_1} [preorder α] :

preorder (with_lower_topology α)

Equations

with_lower_topology.preorder = _inst_1

@[protected, instance]

def with_lower_topology.topological_space {α : Type u_1} [preorder α] :

topological_space (with_lower_topology α)

Equations

with_lower_topology.topological_space = topological_space.generate_from {s : set (with_lower_topology α) | ∃ (a : with_lower_topology α), (set.Ici a)ᶜ = s}

theorem with_lower_topology.is_open_preimage_of_lower {α : Type u_1} [preorder α] (S : set α) :

is_open (⇑with_lower_topology.of_lower ⁻¹' S) ↔ topological_space.is_open S

theorem with_lower_topology.is_open_def {α : Type u_1} [preorder α] (T : set (with_lower_topology α)) :

is_open T ↔ topological_space.is_open (⇑with_lower_topology.to_lower ⁻¹' T)

@[class]

structure lower_topology (α : Type u_3) [t : topological_space α] [preorder α] :

Prop

topology_eq_lower_topology : t = topological_space.generate_from {s : set α | ∃ (a : α), (set.Ici a)ᶜ = s}

The lower topology is the topology generated by the complements of the closed intervals to infinity.

Instances of this typeclass

@[protected, instance]

def with_lower_topology.lower_topology {α : Type u_1} [preorder α] :

lower_topology (with_lower_topology α)

def lower_topology.lower_basis (α : Type u_1) [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

lower_topology.lower_basis α = {s : set α | ∃ (t : set α), t.finite ∧ (↑(upper_closure t))ᶜ = s}

def lower_topology.with_lower_topology_homeomorph {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] :

with_lower_topology α ≃ₜ α

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

Equations

lower_topology.with_lower_topology_homeomorph = {to_equiv := {to_fun := with_lower_topology.of_lower.to_fun, inv_fun := with_lower_topology.of_lower.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

theorem lower_topology.is_open_iff_generate_Ici_compl {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] {s : set α} :

is_open s ↔ topological_space.generate_open {t : set α | ∃ (a : α), (set.Ici a)ᶜ = t} s

theorem lower_topology.is_closed_Ici {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] (a : α) :

is_closed (set.Ici a)

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

theorem lower_topology.is_closed_upper_closure {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] {s : set α} (h : s.finite) :

is_closed ↑(upper_closure s)

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

theorem lower_topology.is_lower_set_of_is_open {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] {s : set α} (h : is_open s) :

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

theorem lower_topology.is_upper_set_of_is_closed {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] {s : set α} (h : is_closed s) :

@[simp]

theorem lower_topology.closure_singleton {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] (a : α) :

closure {a} = set.Ici a

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

@[protected]

theorem lower_topology.is_topological_basis {α : Type u_1} [preorder α] [topological_space α] [lower_topology α] :

topological_space.is_topological_basis (lower_topology.lower_basis α)

@[protected, instance]

def lower_topology.t0_space {α : Type u_1} [partial_order α] [topological_space α] [lower_topology α] :

The lower topology on a partial order is T₀.

@[protected, instance]

def prod.lower_topology {α : Type u_1} {β : Type u_2} [preorder α] [topological_space α] [lower_topology α] [order_bot α] [preorder β] [topological_space β] [lower_topology β] [order_bot β] :

lower_topology (α × β)

theorem Inf_hom.continuous {α : Type u_1} {β : Type u_2} [complete_lattice α] [complete_lattice β] [topological_space α] [lower_topology α] [topological_space β] [lower_topology β] (f : Inf_hom α β) :

continuous ⇑f

@[protected, instance]

def lower_topology.to_has_continuous_inf {α : Type u_1} [complete_lattice α] [topological_space α] [lower_topology α] :

has_continuous_inf α