mathlib3 documentation

topology.sober

Sober spaces #

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

A quasi-sober space is a topological space where every irreducible closed subset has a generic point. A sober space is a quasi-sober space where every irreducible closed subset has a unique generic point. This is if and only if the space is T0, and thus sober spaces can be stated via [quasi_sober α] [t0_space α].

Main definition #

def is_generic_point {α : Type u_1} [topological_space α] (x : α) (S : set α) :
Prop

x is a generic point of S if S is the closure of x.

Equations
theorem is_generic_point_def {α : Type u_1} [topological_space α] {x : α} {S : set α} :
theorem is_generic_point.def {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) :
closure {x} = S
theorem is_generic_point_closure {α : Type u_1} [topological_space α] {x : α} :
theorem is_generic_point_iff_specializes {α : Type u_1} [topological_space α] {x : α} {S : set α} :
is_generic_point x S (y : α), x y y S
theorem is_generic_point.specializes_iff_mem {α : Type u_1} [topological_space α] {x y : α} {S : set α} (h : is_generic_point x S) :
x y y S
theorem is_generic_point.specializes {α : Type u_1} [topological_space α] {x y : α} {S : set α} (h : is_generic_point x S) (h' : y S) :
x y
theorem is_generic_point.mem {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) :
x S
@[protected]
theorem is_generic_point.is_closed {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) :
@[protected]
theorem is_generic_point.is_irreducible {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) :
@[protected]
theorem is_generic_point.eq {α : Type u_1} [topological_space α] {x y : α} {S : set α} [t0_space α] (h : is_generic_point x S) (h' : is_generic_point y S) :
x = y

In a T₀ space, each set has at most one generic point.

theorem is_generic_point.mem_open_set_iff {α : Type u_1} [topological_space α] {x : α} {S U : set α} (h : is_generic_point x S) (hU : is_open U) :
x U (S U).nonempty
theorem is_generic_point.disjoint_iff {α : Type u_1} [topological_space α] {x : α} {S U : set α} (h : is_generic_point x S) (hU : is_open U) :
disjoint S U x U
theorem is_generic_point.mem_closed_set_iff {α : Type u_1} [topological_space α] {x : α} {S Z : set α} (h : is_generic_point x S) (hZ : is_closed Z) :
x Z S Z
@[protected]
theorem is_generic_point.image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x : α} {S : set α} (h : is_generic_point x S) {f : α β} (hf : continuous f) :
theorem is_generic_point_iff_forall_closed {α : Type u_1} [topological_space α] {x : α} {S : set α} (hS : is_closed S) (hxS : x S) :
is_generic_point x S (Z : set α), is_closed Z x Z S Z
@[class]
structure quasi_sober (α : Type u_3) [topological_space α] :
Prop

A space is sober if every irreducible closed subset has a generic point.

Instances of this typeclass
theorem quasi_sober_iff (α : Type u_3) [topological_space α] :
noncomputable def is_irreducible.generic_point {α : Type u_1} [topological_space α] [quasi_sober α] {S : set α} (hS : is_irreducible S) :
α

A generic point of the closure of an irreducible space.

Equations
noncomputable def generic_point (α : Type u_1) [topological_space α] [quasi_sober α] [irreducible_space α] :
α

A generic point of a sober irreducible space.

Equations
noncomputable def irreducible_set_equiv_points {α : Type u_1} [topological_space α] [quasi_sober α] [t0_space α] :

The closed irreducible subsets of a sober space bijects with the points of the space.

Equations
theorem closed_embedding.quasi_sober {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} (hf : closed_embedding f) [quasi_sober β] :
theorem open_embedding.quasi_sober {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} (hf : open_embedding f) [quasi_sober β] :
theorem quasi_sober_of_open_cover {α : Type u_1} [topological_space α] (S : set (set α)) (hS : (s : S), is_open s) [hS' : (s : S), quasi_sober s] (hS'' : ⋃₀ S = ) :

A space is quasi sober if it can be covered by open quasi sober subsets.

@[protected, instance]