Documentation

Mathlib.Topology.StoneCech

Stone-Čech compactification #

Construction of the Stone-Čech compactification using ultrafilters.

For any topological space α, we build a compact Hausdorff space StoneCech α and a continuous map stoneCechUnit : α → StoneCech α which is minimal in the sense of the following universal property: for any compact Hausdorff space β and every map f : α → β such that hf : Continuous f : Continuous f Continuous f, there is a unique map stoneCechExtend hf : StoneCech α → β such that stoneCechExtend_extends : stoneCechExtend hf ∘ stoneCechUnit = f. Continuity of this extension is asserted by continuous_stoneCechExtend and uniqueness by stoneCech_hom_ext.

Beware that the terminology “extend” is slightly misleading since stoneCechUnit is not always injective, so one cannot always think of α as being “inside” its compactification StoneCech α.

Implementation notes #

Parts of the formalization are based on “Ultrafilters and Topology” by Marius Stekelenburg, particularly section 5. However the construction in the general case is different because the equivalence relation on spaces of ultrafilters described by Stekelenburg causes issues with universes since it involves a condition on all compact Hausdorff spaces. We replace it by a two steps construction. The first step called PreStoneCech guarantees the expected universal property but not the Hausdorff condition. We then define StoneCech α as t2Quotient (PreStoneCech α).

def ultrafilterBasis (α : Type u) :

Basis for the topology on Ultrafilter α.

Equations
Instances For
    theorem ultrafilter_isOpen_basic {α : Type u} (s : Set α) :
    IsOpen {u : Ultrafilter α | s u}

    The basic open sets for the topology on ultrafilters are open.

    theorem ultrafilter_isClosed_basic {α : Type u} (s : Set α) :
    IsClosed {u : Ultrafilter α | s u}

    The basic open sets for the topology on ultrafilters are also closed.

    theorem ultrafilter_converges_iff {α : Type u} {u : Ultrafilter (Ultrafilter α)} {x : Ultrafilter α} :
    u nhds x x = joinM u

    Every ultrafilter u on Ultrafilter α converges to a unique point of Ultrafilter α, namely joinM u.

    Equations
    • =
    Equations
    • =
    @[simp]
    theorem Ultrafilter.tendsto_pure_self {α : Type u} (b : Ultrafilter α) :
    Filter.Tendsto pure (b) (nhds b)
    theorem ultrafilter_comap_pure_nhds {α : Type u} (b : Ultrafilter α) :
    Filter.comap pure (nhds b) b
    theorem denseRange_pure {α : Type u} :

    The range of pure : α → Ultrafilter α is dense in Ultrafilter α.

    theorem induced_topology_pure {α : Type u} :
    TopologicalSpace.induced pure Ultrafilter.topologicalSpace =

    The map pure : α → Ultrafilter α induces on α the discrete topology.

    theorem denseInducing_pure {α : Type u} :

    pure : α → Ultrafilter α defines a dense inducing of α in Ultrafilter α.

    theorem denseEmbedding_pure {α : Type u} :

    pure : α → Ultrafilter α defines a dense embedding of α in Ultrafilter α.

    def Ultrafilter.extend {α : Type u} {γ : Type u_1} [TopologicalSpace γ] (f : αγ) :
    Ultrafilter αγ

    The extension of a function α → γ to a function Ultrafilter α → γ. When γ is a compact Hausdorff space it will be continuous.

    Equations
    Instances For
      theorem ultrafilter_extend_extends {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] (f : αγ) :
      theorem continuous_ultrafilter_extend {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] (f : αγ) :
      theorem ultrafilter_extend_eq_iff {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] {f : αγ} {b : Ultrafilter α} {c : γ} :

      The value of Ultrafilter.extend f on an ultrafilter b is the unique limit of the ultrafilter b.map f in γ.

      def PreStoneCech (α : Type u) [TopologicalSpace α] :

      Auxilliary construction towards the Stone-Čech compactification of a topological space. It should not be used after the Stone-Čech compactification is constructed.

      Equations
      Instances For
        Equations
        Equations
        def preStoneCechUnit {α : Type u} [TopologicalSpace α] (x : α) :

        The natural map from α to its pre-Stone-Čech compactification.

        Equations
        Instances For
          theorem continuous_preStoneCechUnit {α : Type u} [TopologicalSpace α] :
          Continuous preStoneCechUnit
          theorem denseRange_preStoneCechUnit {α : Type u} [TopologicalSpace α] :
          DenseRange preStoneCechUnit
          theorem preStoneCechCompat {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : αβ} (hg : Continuous g) {F : Ultrafilter α} {G : Ultrafilter α} {x : α} (hF : F nhds x) (hG : G nhds x) :
          def preStoneCechExtend {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : αβ} (hg : Continuous g) :
          PreStoneCech αβ

          The extension of a continuous function from α to a compact Hausdorff space β to the pre-Stone-Čech compactification of α.

          Equations
          Instances For
            theorem preStoneCechExtend_extends {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : αβ} (hg : Continuous g) :
            preStoneCechExtend hg preStoneCechUnit = g
            theorem eq_if_preStoneCechUnit_eq {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : αβ} (hg : Continuous g) {a : α} {b : α} (h : preStoneCechUnit a = preStoneCechUnit b) :
            g a = g b
            theorem preStoneCech_hom_ext {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g₁ : PreStoneCech αβ} {g₂ : PreStoneCech αβ} (h₁ : Continuous g₁) (h₂ : Continuous g₂) (h : g₁ preStoneCechUnit = g₂ preStoneCechUnit) :
            g₁ = g₂
            def StoneCech (α : Type u) [TopologicalSpace α] :

            The Stone-Čech compactification of a topological space.

            Equations
            Instances For
              Equations
              • =
              Equations
              • =
              Equations
              def stoneCechUnit {α : Type u} [TopologicalSpace α] (x : α) :

              The natural map from α to its Stone-Čech compactification.

              Equations
              Instances For
                theorem continuous_stoneCechUnit {α : Type u} [TopologicalSpace α] :
                Continuous stoneCechUnit
                theorem denseRange_stoneCechUnit {α : Type u} [TopologicalSpace α] :
                DenseRange stoneCechUnit

                The image of stoneCechUnit is dense. (But stoneCechUnit need not be an embedding, for example if the original space is not Hausdorff.)

                def stoneCechExtend {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : αβ} (hg : Continuous g) :
                StoneCech αβ

                The extension of a continuous function from α to a compact Hausdorff space β to the Stone-Čech compactification of α. This extension implements the universal property of this compactification.

                Equations
                Instances For
                  theorem stoneCechExtend_extends {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : αβ} (hg : Continuous g) :
                  stoneCechExtend hg stoneCechUnit = g
                  theorem continuous_stoneCechExtend {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : αβ} (hg : Continuous g) :
                  theorem eq_if_stoneCechUnit_eq {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {a : α} {b : α} {f : αβ} (hcf : Continuous f) (h : stoneCechUnit a = stoneCechUnit b) :
                  f a = f b
                  theorem stoneCech_hom_ext {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g₁ : StoneCech αβ} {g₂ : StoneCech αβ} (h₁ : Continuous g₁) (h₂ : Continuous g₂) (h : g₁ stoneCechUnit = g₂ stoneCechUnit) :
                  g₁ = g₂