Documentation

Mathlib.Topology.Category.Compactum

Compacta and Compact Hausdorff Spaces #

Recall that, given a monad M on Type*, an algebra for M consists of the following data:

See the file CategoryTheory.Monad.Algebra for a general version, as well as the following link. https://ncatlab.org/nlab/show/monad

This file proves the equivalence between the category of compact Hausdorff topological spaces and the category of algebras for the ultrafilter monad.

Notation: #

Here are the main objects introduced in this file.

The proof of this equivalence is a bit technical. But the idea is quite simply that the structure map Ultrafilter X → X for an algebra X of the ultrafilter monad should be considered as the map sending an ultrafilter to its limit in X. The topology on X is then defined by mimicking the characterization of open sets in terms of ultrafilters.

Any X : Compactum is endowed with a coercion to Type*, as well as the following instances:

Any morphism f : X ⟶ Y of is endowed with a coercion to a function X → Y, which is shown to be continuous in continuous_of_hom.

The function Compactum.ofTopologicalSpace can be used to construct a Compactum from a topological space which satisfies CompactSpace and T2Space.

We also add wrappers around structures which already exist. Here are the main ones, all in the Compactum namespace:

References #

def Compactum :
Type (u_1 + 1)

The type Compactum of Compacta, defined as algebras for the ultrafilter monad.

Equations
Instances For

    The forgetful functor to Type*

    Equations
    Instances For

      The "free" Compactum functor.

      Equations
      Instances For
        instance Compactum.instCoeFunHomForallA {X : Compactum} {Y : Compactum} :
        CoeFun (X Y) fun (x : X Y) => X.AY.A
        Equations
        • Compactum.instCoeFunHomForallA = { coe := fun (f : X Y) => f.f }
        def Compactum.str (X : Compactum) :
        Ultrafilter X.AX.A

        The structure map for a compactum, essentially sending an ultrafilter to its limit.

        Equations
        • X.str = X.a
        Instances For

          The monadic join.

          Equations
          Instances For
            def Compactum.incl (X : Compactum) :
            X.AUltrafilter X.A

            The inclusion of X into Ultrafilter X.

            Equations
            Instances For
              @[simp]
              theorem Compactum.str_incl (X : Compactum) (x : X.A) :
              X.str (X.incl x) = x
              @[simp]
              theorem Compactum.str_hom_commute (X : Compactum) (Y : Compactum) (f : X Y) (xs : Ultrafilter X.A) :
              f.f (X.str xs) = Y.str (Ultrafilter.map f.f xs)
              @[simp]
              theorem Compactum.join_distrib (X : Compactum) (uux : Ultrafilter (Ultrafilter X.A)) :
              X.str (X.join uux) = X.str (Ultrafilter.map X.str uux)
              Equations
              • Compactum.instTopologicalSpaceA = { IsOpen := fun (U : Set X.A) => ∀ (F : Ultrafilter X.A), X.str F UU F, isOpen_univ := , isOpen_inter := , isOpen_sUnion := }
              theorem Compactum.isClosed_iff {X : Compactum} (S : Set X.A) :
              IsClosed S ∀ (F : Ultrafilter X.A), S FX.str F S
              Equations
              • =
              theorem Compactum.str_eq_of_le_nhds {X : Compactum} (F : Ultrafilter X.A) (x : X.A) :
              F nhds xX.str F = x
              theorem Compactum.le_nhds_of_str_eq {X : Compactum} (F : Ultrafilter X.A) (x : X.A) :
              X.str F = xF nhds x
              Equations
              • =
              theorem Compactum.lim_eq_str {X : Compactum} (F : Ultrafilter X.A) :
              F.lim = X.str F

              The structure map of a compactum actually computes limits.

              theorem Compactum.continuous_of_hom {X : Compactum} {Y : Compactum} (f : X Y) :

              Any morphism of compacta is continuous.

              Given any compact Hausdorff space, we construct a Compactum.

              Equations
              Instances For
                def Compactum.homOfContinuous {X : Compactum} {Y : Compactum} (f : X.AY.A) (cont : Continuous f) :
                X Y

                Any continuous map between Compacta is a morphism of compacta.

                Equations
                Instances For

                  The functor functor from Compactum to CompHaus.

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

                    This definition is used to prove essential surjectivity of compactumToCompHaus.

                    Equations
                    • compactumToCompHaus.isoOfTopologicalSpace = { hom := { toFun := id, continuous_toFun := }, inv := { toFun := id, continuous_toFun := }, hom_inv_id := , inv_hom_id := }
                    Instances For

                      The functor compactumToCompHaus is essentially surjective.

                      Equations

                      The functor compactumToCompHaus is an equivalence of categories.

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