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 [quasi_sober α] [t0_space α].

Main definition #

• is_generic_point : x is the generic point of S if S is the closure of x.
• quasi_sober : A space is quasi-sober if every irreducible closed subset has a generic point.
def is_generic_point {α : Type u_1} (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} {x : α} {S : set α} :
closure {x} = S
theorem is_generic_point.def {α : Type u_1} {x : α} {S : set α} (h : S) :
closure {x} = S
theorem is_generic_point_closure {α : Type u_1} {x : α} :
(closure {x})
theorem is_generic_point_iff_specializes {α : Type u_1} {x : α} {S : set α} :
∀ (y : α), x y y S
theorem is_generic_point.specializes_iff_mem {α : Type u_1} {x y : α} {S : set α} (h : S) :
x y y S
theorem is_generic_point.specializes {α : Type u_1} {x y : α} {S : set α} (h : S) (h' : y S) :
x y
theorem is_generic_point.mem {α : Type u_1} {x : α} {S : set α} (h : S) :
x S
@[protected]
theorem is_generic_point.is_closed {α : Type u_1} {x : α} {S : set α} (h : S) :
@[protected]
theorem is_generic_point.is_irreducible {α : Type u_1} {x : α} {S : set α} (h : S) :
@[protected]
theorem is_generic_point.eq {α : Type u_1} {x y : α} {S : set α} [t0_space α] (h : S) (h' : 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} {x : α} {S U : set α} (h : S) (hU : is_open U) :
x U (S U).nonempty
theorem is_generic_point.disjoint_iff {α : Type u_1} {x : α} {S U : set α} (h : S) (hU : is_open U) :
U x U
theorem is_generic_point.mem_closed_set_iff {α : Type u_1} {x : α} {S Z : set α} (h : S) (hZ : is_closed Z) :
x Z S Z
@[protected]
theorem is_generic_point.image {α : Type u_1} {β : Type u_2} {x : α} {S : set α} (h : S) {f : α → β} (hf : continuous f) :
theorem is_generic_point_iff_forall_closed {α : Type u_1} {x : α} {S : set α} (hS : is_closed S) (hxS : x S) :
∀ (Z : set α), x ZS Z
@[class]
structure quasi_sober (α : Type u_3)  :
Prop
• sober : ∀ {S : set α}, (∃ (x : α), S)

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

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

A generic point of the closure of an irreducible space.

Equations
theorem is_irreducible.generic_point_spec {α : Type u_1} [quasi_sober α] {S : set α} (hS : is_irreducible S) :
@[simp]
theorem is_irreducible.generic_point_closure_eq {α : Type u_1} [quasi_sober α] {S : set α} (hS : is_irreducible S) :
noncomputable def generic_point (α : Type u_1) [quasi_sober α]  :
α

A generic point of a sober irreducible space.

Equations
theorem generic_point_spec (α : Type u_1) [quasi_sober α]  :
@[simp]
theorem generic_point_closure (α : Type u_1) [quasi_sober α]  :
theorem generic_point_specializes {α : Type u_1} [quasi_sober α] (x : α) :
noncomputable def irreducible_set_equiv_points {α : Type u_1} [quasi_sober α] [t0_space α] :
{s : set α | ≃o α

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} {f : α → β} (hf : closed_embedding f) [quasi_sober β] :
theorem open_embedding.quasi_sober {α : Type u_1} {β : Type u_2} {f : α → β} (hf : open_embedding f) [quasi_sober β] :
theorem quasi_sober_of_open_cover {α : Type u_1} (S : set (set α)) (hS : ∀ (s : S), ) [hS' : ∀ (s : S), ] (hS'' : ⋃₀ S = ) :

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

@[protected, instance]
def t2_space.quasi_sober {α : Type u_1} [t2_space α] :