Documentation

Mathlib.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 [QuasiSober α] [T0Space α].

Main definition #

def IsGenericPoint {α : Type u_1} [TopologicalSpace α] (x : α) (S : Set α) :

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

Equations
Instances For
    theorem isGenericPoint_def {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} :
    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 : α} :
    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) :
    theorem IsGenericPoint.isIrreducible {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} (h : IsGenericPoint x S) :
    theorem IsGenericPoint.inseparable {α : Type u_1} [TopologicalSpace α] {x : α} {y : α} {S : Set α} (h : IsGenericPoint x S) (h' : IsGenericPoint y S) :
    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) :
    theorem IsGenericPoint.disjoint_iff {α : Type u_1} [TopologicalSpace α] {x : α} {S : Set α} {U : Set α} (h : IsGenericPoint x S) (hU : IsOpen U) :
    Disjoint S U xU
    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 Zx ZS Z
    theorem quasiSober_iff (α : Type u_3) [TopologicalSpace α] :
    QuasiSober α ∀ {S : Set α}, IsIrreducible SIsClosed S∃ (x : α), IsGenericPoint x S
    class QuasiSober (α : Type u_3) [TopologicalSpace α] :

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

    Instances
      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
      Instances For
        noncomputable def genericPoint (α : Type u_1) [TopologicalSpace α] [QuasiSober α] [IrreducibleSpace α] :
        α

        A generic point of a sober irreducible space.

        Equations
        Instances For
          noncomputable def irreducibleSetEquivPoints {α : Type u_1} [TopologicalSpace α] [QuasiSober α] [T0Space α] :
          {s : Set α | IsIrreducible s IsClosed s} ≃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.
          Instances For
            theorem ClosedEmbedding.quasiSober {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : ClosedEmbedding f) [QuasiSober β] :
            theorem OpenEmbedding.quasiSober {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : OpenEmbedding f) [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 = ) :

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

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

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

            Equations
            • =