mathlib documentation

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 #

def specializes {α : Type u_1} [topological_space α] (x y : α) :
Prop

x specializes to y if y is in the closure of x. The notation used is x ⤳ y.

Equations
theorem specializes_def {α : Type u_1} [topological_space α] (x y : α) :
x y y closure {x}
theorem specializes_iff_closure_subset {α : Type u_1} [topological_space α] {x y : α} :
x y closure {y} closure {x}
theorem specializes_rfl {α : Type u_1} [topological_space α] {x : α} :
x x
theorem specializes_refl {α : Type u_1} [topological_space α] (x : α) :
x x
theorem specializes.trans {α : Type u_1} [topological_space α] {x y z : α} :
x yy zx z
theorem specializes_iff_forall_closed {α : Type u_1} [topological_space α] {x y : α} :
x y ∀ (Z : set α), is_closed Zx Zy Z
theorem specializes_iff_forall_open {α : Type u_1} [topological_space α] {x y : α} :
x y ∀ (U : set α), is_open Uy Ux U
theorem indistinguishable_iff_specializes_and {α : Type u_1} [topological_space α] (x y : α) :
theorem specializes_antisymm {α : Type u_1} [topological_space α] [t0_space α] (x y : α) :
x yy xx = y
theorem specializes.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x y : α} (h : x y) {f : α → β} (hf : continuous f) :
f x f y
theorem continuous_map.map_specialization {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x y : α} (h : x y) (f : C(α, β)) :
f x f y
theorem specializes.eq {α : Type u_1} [topological_space α] [t1_space α] {x y : α} (h : x y) :
x = y
@[simp]
theorem specializes_iff_eq {α : Type u_1} [topological_space α] [t1_space α] {x y : α} :
x y x = y
def specialization_preorder (α : Type u_1) [topological_space α] :

Specialization forms a preorder on the topological space.

Equations
def specialization_order (α : Type u_1) [topological_space α] [t0_space α] :

Specialization forms a partial order on a t0 topological space.

Equations
theorem specialization_order.monotone_of_continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (hf : continuous f) :
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.specializes {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) {y : α} (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
theorem is_generic_point.is_closed {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) :
theorem is_generic_point.is_irreducible {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) :
theorem is_generic_point.eq {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) [t0_space α] {y : α} (h' : is_generic_point y S) :
x = y
theorem is_generic_point.mem_open_set_iff {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) {U : set α} (hU : is_open U) :
x U (S U).nonempty
theorem is_generic_point.disjoint_iff {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) {U : set α} (hU : is_open U) :
disjoint S U x U
theorem is_generic_point.mem_closed_set_iff {α : Type u_1} [topological_space α] {x : α} {S : set α} (h : is_generic_point x S) {Z : set α} (hZ : is_closed Z) :
x Z S Z
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 Zx ZS 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 α] :
quasi_sober α ∀ {S : set α}, is_irreducible Sis_closed S(∃ (x : α), is_generic_point x S)
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
@[simp]
noncomputable def generic_point (α : Type u_1) [topological_space α] [quasi_sober α] [irreducible_space α] :
α

A generic point of a sober irreducible space.

Equations
@[simp]
theorem generic_point_specializes {α : Type u_1} [topological_space α] [quasi_sober α] [irreducible_space α] (x : α) :
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]
def t2_space.quasi_sober {α : Type u_1} [topological_space α] [t2_space α] :