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.
• genericPoints : The set of generic points of irreducible components.

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 U : Set α} (h : IsGenericPoint x S) (hU : IsOpen U) : x ∈ U ↔ (S ∩ U).Nonempty

theorem IsGenericPoint.disjoint_iff {α : Type u_1} [TopologicalSpace α] {x : α} {S 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 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

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_iff (α : Type u_3) [TopologicalSpace α] : 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.isGenericPoint_genericPoint_closure {α : Type u_1} [TopologicalSpace α] [QuasiSober α] {S : Set α} (hS : IsIrreducible S) : IsGenericPoint hS.genericPoint (closure S)

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

@[simp]

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

theorem IsIrreducible.closure_genericPoint {α : Type u_1} [TopologicalSpace α] [QuasiSober α] {S : Set α} (hS : IsIrreducible S) (hS' : IsClosed S) : closure {hS.genericPoint} = 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 α) Set.univ

@[simp]

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

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 Topology.IsClosedEmbedding.quasiSober {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsClosedEmbedding f) [QuasiSober β] : QuasiSober α

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

theorem TopologicalSpace.IsOpenCover.quasiSober_iff_forall {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {U : ι → Opens α} (hU : IsOpenCover U) : QuasiSober α ↔ ∀ (i : ι), QuasiSober ↥(U i)

theorem TopologicalSpace.IsOpenCover.quasiSober {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {U : ι → Opens α} (hU : IsOpenCover U) [∀ (i : ι), QuasiSober ↥(U i)] : QuasiSober α

theorem quasiSober_of_open_cover {α : Type u_1} [TopologicalSpace α] (S : Set (Set α)) (hS : ∀ (s : ↑S), IsOpen ↑s) [∀ (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.

def genericPoints (α : Type u_1) [TopologicalSpace α] : Set α

The set of generic points of irreducible components.

Equations

• genericPoints α = {x : α | closure {x} ∈ irreducibleComponents α}

def genericPoints.component {α : Type u_1} [TopologicalSpace α] (x : ↑(genericPoints α)) : ↑(irreducibleComponents α)

The irreducible component of a generic point

Equations

• genericPoints.component x = ⟨closure {↑x}, ⋯⟩

theorem genericPoints.isGenericPoint {α : Type u_1} [TopologicalSpace α] (x : ↑(genericPoints α)) : IsGenericPoint ↑x ↑(component x)

theorem genericPoints.component_injective {α : Type u_1} [TopologicalSpace α] [T0Space α] : Function.Injective component

noncomputable def genericPoints.ofComponent {α : Type u_1} [TopologicalSpace α] [QuasiSober α] (x : ↑(irreducibleComponents α)) : ↑(genericPoints α)

The generic point of an irreducible component.

Equations

• genericPoints.ofComponent x = ⟨⋯.genericPoint, ⋯⟩

theorem genericPoints.isGenericPoint_ofComponent {α : Type u_1} [TopologicalSpace α] [QuasiSober α] (x : ↑(irreducibleComponents α)) : IsGenericPoint ↑(ofComponent x) ↑x

@[simp]

theorem genericPoints.component_ofComponent {α : Type u_1} [TopologicalSpace α] [QuasiSober α] (x : ↑(irreducibleComponents α)) : component (ofComponent x) = x

@[simp]

theorem genericPoints.ofComponent_component {α : Type u_1} [TopologicalSpace α] [T0Space α] [QuasiSober α] (x : ↑(genericPoints α)) : ofComponent (component x) = x

theorem genericPoints.component_surjective {α : Type u_1} [TopologicalSpace α] [QuasiSober α] : Function.Surjective component

theorem genericPoints.finite {α : Type u_1} [TopologicalSpace α] [T0Space α] (h : (irreducibleComponents α).Finite) : (genericPoints α).Finite

noncomputable def genericPoints.equiv {α : Type u_1} [TopologicalSpace α] [T0Space α] [QuasiSober α] : ↑(genericPoints α) ≃ ↑(irreducibleComponents α)

In a sober space, the generic points corresponds bijectively to irreducible components

Equations

• genericPoints.equiv = { toFun := genericPoints.component, invFun := genericPoints.ofComponent, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem genericPoints.equiv_symm_apply {α : Type u_1} [TopologicalSpace α] [T0Space α] [QuasiSober α] (x : ↑(irreducibleComponents α)) : equiv.symm x = ofComponent x

@[simp]

theorem genericPoints.equiv_apply {α : Type u_1} [TopologicalSpace α] [T0Space α] [QuasiSober α] (x : ↑(genericPoints α)) : equiv x = component x

theorem genericPoints.closure {α : Type u_1} [TopologicalSpace α] [QuasiSober α] : _root_.closure (genericPoints α) = Set.univ

theorem genericPoints_eq_singleton {α : Type u_1} [TopologicalSpace α] [QuasiSober α] [IrreducibleSpace α] [T0Space α] : genericPoints α = {genericPoint α}