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} [TopologicalSpace α] (x : α) (S : Set α) : Prop

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

Equations

• IsGenericPoint x S = (closure {x} = S)

theorem isGenericPoint_def {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} : IsGenericPoint x S ↔ closure {x} = S

theorem IsGenericPoint.def {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} (h : IsGenericPoint x S) : closure {x} = S

theorem isGenericPoint_closure {α : Type u_1} [TopologicalSpace α] {x : α} : IsGenericPoint x (closure {x})

theorem isGenericPoint_iff_specializes {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} : IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S

theorem IsGenericPoint.specializes_iff_mem {α : Type u_1} [TopologicalSpace α] {x : α} {y : α} {S : Set α} (h : IsGenericPoint x S) : x ⤳ y ↔ y ∈ S

theorem IsGenericPoint.specializes {α : Type u_1} [TopologicalSpace α] {x : α} {y : α} {S : Set α} (h : IsGenericPoint x S) (h' : y ∈ S) : x ⤳ y

theorem IsGenericPoint.mem {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} (h : IsGenericPoint x S) : x ∈ S

theorem IsGenericPoint.isClosed {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} (h : IsGenericPoint x S) : IsClosed S

theorem IsGenericPoint.isIrreducible {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} (h : IsGenericPoint x S) : IsIrreducible S

theorem IsGenericPoint.inseparable {α : Type u_1} [TopologicalSpace α] {x : α} {y : α} {S : Set α} (h : IsGenericPoint x S) (h' : IsGenericPoint y S) : Inseparable x y

theorem IsGenericPoint.eq {α : Type u_1} [TopologicalSpace α] {x : α} {y : α} {S : Set α} [T0Space α] (h : IsGenericPoint x S) (h' : IsGenericPoint y S) : x = y

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

theorem IsGenericPoint.mem_open_set_iff {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} {U : Set α} (h : IsGenericPoint x S) (hU : IsOpen U) : x ∈ U ↔ (S ∩ U).Nonempty

theorem IsGenericPoint.disjoint_iff {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} {U : Set α} (h : IsGenericPoint x S) (hU : IsOpen U) : Disjoint S U ↔ x ∉ U

theorem IsGenericPoint.mem_closed_set_iff {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} {Z : Set α} (h : IsGenericPoint x S) (hZ : IsClosed Z) : x ∈ Z ↔ S ⊆ Z

theorem IsGenericPoint.image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {S : Set α} (h : IsGenericPoint x S) {f : α → β} (hf : Continuous f) : IsGenericPoint (f x) (closure (f '' S))

theorem isGenericPoint_iff_forall_closed {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} (hS : IsClosed S) (hxS : x ∈ S) : IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

theorem quasiSober_iff (α : Type u_3) [TopologicalSpace α] : QuasiSober α ↔ ∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ (x : α), IsGenericPoint x S

class QuasiSober (α : Type u_3) [TopologicalSpace α] : Prop

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

• sober : ∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ (x : α), IsGenericPoint x S

theorem QuasiSober.sober {α : Type u_3} [TopologicalSpace α] [self : QuasiSober α] {S : Set α} : IsIrreducible S → IsClosed S → ∃ (x : α), IsGenericPoint x S

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

A generic point of the closure of an irreducible space.

Equations

• hS.genericPoint = ⋯.choose

theorem IsIrreducible.genericPoint_spec {α : Type u_1} [TopologicalSpace α] [QuasiSober α] {S : Set α} (hS : IsIrreducible S) : IsGenericPoint hS.genericPoint (closure S)

@[simp]

theorem IsIrreducible.genericPoint_closure_eq {α : Type u_1} [TopologicalSpace α] [QuasiSober α] {S : Set α} (hS : IsIrreducible S) : closure {hS.genericPoint} = closure S

noncomputable def genericPoint (α : Type u_1) [TopologicalSpace α] [QuasiSober α] [IrreducibleSpace α] : α

A generic point of a sober irreducible space.

Equations

• genericPoint α = ⋯.genericPoint

theorem genericPoint_spec (α : Type u_1) [TopologicalSpace α] [QuasiSober α] [IrreducibleSpace α] : IsGenericPoint (genericPoint α) ⊤

@[simp]

theorem genericPoint_closure (α : Type u_1) [TopologicalSpace α] [QuasiSober α] [IrreducibleSpace α] : closure {genericPoint α} = ⊤

theorem genericPoint_specializes {α : Type u_1} [TopologicalSpace α] [QuasiSober α] [IrreducibleSpace α] (x : α) : genericPoint α ⤳ x

noncomputable def irreducibleSetEquivPoints {α : Type u_1} [TopologicalSpace α] [QuasiSober α] [T0Space α] : TopologicalSpace.IrreducibleCloseds α ≃o α

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

Equations

• One or more equations did not get rendered due to their size.

theorem ClosedEmbedding.quasiSober {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : ClosedEmbedding f) [QuasiSober β] : QuasiSober α

theorem OpenEmbedding.quasiSober {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : OpenEmbedding f) [QuasiSober β] : QuasiSober α

theorem quasiSober_of_open_cover {α : Type u_1} [TopologicalSpace α] (S : Set (Set α)) (hS : ∀ (s : ↑S), IsOpen ↑s) [hS' : ∀ (s : ↑S), QuasiSober ↑↑s] (hS'' : ⋃₀ S = ⊤) : QuasiSober α

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

@[instance 100]

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

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

Equations

• ⋯ = ⋯