# Documentation

Mathlib.Topology.Sober

# Sober spaces #

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 [QuasiSober α] [T0Space α].

## Main definition #

• IsGenericPoint : x is the generic point of S if S is the closure of x.
• QuasiSober : A space is quasi-sober if every irreducible closed subset has a generic point.
def IsGenericPoint {α : Type u_1} [] (x : α) (S : Set α) :

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

Instances For
theorem isGenericPoint_def {α : Type u_1} [] {x : α} {S : Set α} :
closure {x} = S
theorem IsGenericPoint.def {α : Type u_1} [] {x : α} {S : Set α} (h : ) :
closure {x} = S
theorem isGenericPoint_closure {α : Type u_1} [] {x : α} :
theorem isGenericPoint_iff_specializes {α : Type u_1} [] {x : α} {S : Set α} :
∀ (y : α), x y y S
theorem IsGenericPoint.specializes_iff_mem {α : Type u_1} [] {x : α} {y : α} {S : Set α} (h : ) :
x y y S
theorem IsGenericPoint.specializes {α : Type u_1} [] {x : α} {y : α} {S : Set α} (h : ) (h' : y S) :
x y
theorem IsGenericPoint.mem {α : Type u_1} [] {x : α} {S : Set α} (h : ) :
x S
theorem IsGenericPoint.isClosed {α : Type u_1} [] {x : α} {S : Set α} (h : ) :
theorem IsGenericPoint.isIrreducible {α : Type u_1} [] {x : α} {S : Set α} (h : ) :
theorem IsGenericPoint.inseparable {α : Type u_1} [] {x : α} {y : α} {S : Set α} (h : ) (h' : ) :
theorem IsGenericPoint.eq {α : Type u_1} [] {x : α} {y : α} {S : Set α} [] (h : ) (h' : ) :
x = y

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

theorem IsGenericPoint.mem_open_set_iff {α : Type u_1} [] {x : α} {S : Set α} {U : Set α} (h : ) (hU : ) :
theorem IsGenericPoint.disjoint_iff {α : Type u_1} [] {x : α} {S : Set α} {U : Set α} (h : ) (hU : ) :
theorem IsGenericPoint.mem_closed_set_iff {α : Type u_1} [] {x : α} {S : Set α} {Z : Set α} (h : ) (hZ : ) :
x Z S Z
theorem IsGenericPoint.image {α : Type u_1} {β : Type u_2} [] [] {x : α} {S : Set α} (h : ) {f : αβ} (hf : ) :
IsGenericPoint (f x) (closure (f '' S))
theorem isGenericPoint_iff_forall_closed {α : Type u_1} [] {x : α} {S : Set α} (hS : ) (hxS : x S) :
∀ (Z : Set α), x ZS Z
theorem quasiSober_iff (α : Type u_3) [] :
∀ {S : Set α}, x,
class QuasiSober (α : Type u_3) [] :
• sober : ∀ {S : Set α}, x,

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

Instances
noncomputable def IsIrreducible.genericPoint {α : Type u_1} [] [] {S : Set α} (hS : ) :
α

A generic point of the closure of an irreducible space.

Instances For
theorem IsIrreducible.genericPoint_spec {α : Type u_1} [] [] {S : Set α} (hS : ) :
@[simp]
theorem IsIrreducible.genericPoint_closure_eq {α : Type u_1} [] [] {S : Set α} (hS : ) :
noncomputable def genericPoint (α : Type u_1) [] [] [] :
α

A generic point of a sober irreducible space.

Instances For
theorem genericPoint_spec (α : Type u_1) [] [] [] :
@[simp]
theorem genericPoint_closure (α : Type u_1) [] [] [] :
theorem genericPoint_specializes {α : Type u_1} [] [] [] (x : α) :
noncomputable def irreducibleSetEquivPoints {α : Type u_1} [] [] [] :
{s | } ≃o α

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

Instances For
theorem ClosedEmbedding.quasiSober {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) [] :
theorem OpenEmbedding.quasiSober {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) [] :
theorem quasiSober_of_open_cover {α : Type u_1} [] (S : Set (Set α)) (hS : ∀ (s : S), IsOpen s) [hS' : ∀ (s : S), QuasiSober s] (hS'' : ⋃₀ S = ) :

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

instance T2Space.quasiSober {α : Type u_1} [] [] :

Any Hausdorff space is a quasi-sober space because any irreducible set is a singleton.