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.

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.

Instances For

    The forgetful functor to Type*

    Instances For

      The "free" Compactum functor.

      Instances For

        The adjunction between free and forget.

        Instances For
          def Compactum.str (X : Compactum) :
          Ultrafilter X.AX.A

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

          Instances For

            The monadic join.

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

              The inclusion of X into Ultrafilter X.

              Instances For
                theorem Compactum.str_incl (X : Compactum) (x : X.A) :
                theorem Compactum.isClosed_iff {X : Compactum} (S : Set X.A) :
                IsClosed S ∀ (F : Ultrafilter X.A), S FCompactum.str X F S
                theorem Compactum.str_eq_of_le_nhds {X : Compactum} (F : Ultrafilter X.A) (x : X.A) :
                F nhds xCompactum.str X F = x
                theorem Compactum.le_nhds_of_str_eq {X : Compactum} (F : Ultrafilter X.A) (x : X.A) :
                Compactum.str X F = xF nhds x

                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.

                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.

                  Instances For

                    The functor functor from Compactum to CompHaus.

                    Instances For

                      This definition is used to prove essential surjectivity of compactumToCompHaus.

                      Instances For

                        The functor compactumToCompHaus is an equivalence of categories.