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 #

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} [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_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) :

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

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 of this typeclass

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