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 #

specializes : specializes x y (x ⤳ y) means that x specializes to y, i.e. y is in the closure of x.
specialization_preorder : specialization gives a preorder on a topological space.
specialization_order : specialization gives a partial order on a T0 space.
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 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

x ⤳ y = (y ∈ closure {x})

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 ⤳ y → y ⤳ z → x ⤳ z

theorem specializes_iff_forall_closed {α : Type u_1} [topological_space α] {x y : α} :

x ⤳ y ↔ ∀ (Z : set α), is_closed Z → x ∈ Z → y ∈ Z

theorem specializes_iff_forall_open {α : Type u_1} [topological_space α] {x y : α} :

x ⤳ y ↔ ∀ (U : set α), is_open U → y ∈ U → x ∈ U

theorem indistinguishable_iff_specializes_and {α : Type u_1} [topological_space α] (x y : α) :

indistinguishable x y ↔ x ⤳ y ∧ y ⤳ x

theorem specializes_antisymm {α : Type u_1} [topological_space α] [t0_space α] (x y : α) :

x ⤳ y → y ⤳ x → x = 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

specialization_preorder α = {le := λ (x y : α), y ⤳ x, lt := λ (a b : α), b ⤳ a ∧ ¬a ⤳ b, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

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

partial_order α

Specialization forms a partial order on a t0 topological space.

Equations

specialization_order α = {le := preorder.le (specialization_preorder α), lt := preorder.lt (specialization_preorder α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

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

is_generic_point x S = (closure {x} = S)

theorem is_generic_point_def {α : Type u_1} [topological_space α] {x : α} {S : set α} :

is_generic_point x S ↔ closure {x} = S

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 : α} :

is_generic_point x (closure {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) :

is_irreducible 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) :

is_generic_point (f x) (closure (f '' S))

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

sober : ∀ {S : set α}, is_irreducible S → is_closed S → (∃ (x : α), is_generic_point x S)

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

Instances

theorem quasi_sober_iff (α : Type u_3) [topological_space α] :

quasi_sober α ↔ ∀ {S : set α}, is_irreducible S → is_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

hS.generic_point = _.some

theorem is_irreducible.generic_point_spec {α : Type u_1} [topological_space α] [quasi_sober α] {S : set α} (hS : is_irreducible S) :

is_generic_point hS.generic_point (closure S)

@[simp]

theorem is_irreducible.generic_point_closure_eq {α : Type u_1} [topological_space α] [quasi_sober α] {S : set α} (hS : is_irreducible S) :

closure {hS.generic_point} = closure S

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

α

A generic point of a sober irreducible space.

Equations

generic_point α = _.generic_point

theorem generic_point_spec (α : Type u_1) [topological_space α] [quasi_sober α] [irreducible_space α] :

is_generic_point (generic_point α) ⊤

@[simp]

theorem generic_point_closure (α : Type u_1) [topological_space α] [quasi_sober α] [irreducible_space α] :

closure {generic_point α} = ⊤

theorem generic_point_specializes {α : Type u_1} [topological_space α] [quasi_sober α] [irreducible_space α] (x : α) :

generic_point α ⤳ x

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

↥{s : set α | is_irreducible s ∧ is_closed s} ≃o α

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

Equations

irreducible_set_equiv_points = {to_equiv := {to_fun := λ (s : ↥{s : set α | is_irreducible s ∧ is_closed s}), _.generic_point, inv_fun := λ (x : α), ⟨closure {x}, _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

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 α] :