Documentation

Mathlib.Topology.Category.CompHaus.Basic

The category of Compact Hausdorff Spaces #

We construct the category of compact Hausdorff spaces. The type of compact Hausdorff spaces is denoted CompHaus, and it is endowed with a category instance making it a full subcategory of TopCat. The fully faithful functor CompHausTopCat is denoted compHausToTop.

Note: The file Mathlib/Topology/Category/Compactum.lean provides the equivalence between Compactum, which is defined as the category of algebras for the ultrafilter monad, and CompHaus. CompactumToCompHaus is the functor from Compactum to CompHaus which is proven to be an equivalence of categories in CompactumToCompHaus.isEquivalence. See Mathlib/Topology/Category/Compactum.lean for a more detailed discussion where these definitions are introduced.

Implementation #

The category CompHaus is defined using the structure CompHausLike. See the file CompHausLike.Basic for more information.

@[reducible, inline]
abbrev CompHaus :
Type (u_1 + 1)

The category of compact Hausdorff spaces.

Equations
Instances For
    Equations
    Equations
    Equations
    • =
    Equations
    • =
    @[reducible, inline]

    A constructor for objects of the category CompHaus, taking a type, and bundling the compact Hausdorff topology found by typeclass inference.

    Equations
    Instances For
      @[reducible, inline]

      The fully faithful embedding of CompHaus in TopCat.

      Equations
      Instances For
        @[simp]
        theorem stoneCechObj_toTop_α (X : TopCat) :
        (stoneCechObj X).toTop = StoneCech X

        (Implementation) The object part of the compactification functor from topological spaces to compact Hausdorff spaces.

        Equations
        Instances For
          noncomputable def stoneCechEquivalence (X : TopCat) (Y : CompHaus) :

          (Implementation) The bijection of homsets to establish the reflective adjunction of compact Hausdorff spaces in topological spaces.

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

            The Stone-Cech compactification functor from topological spaces to compact Hausdorff spaces, left adjoint to the inclusion functor.

            Equations
            Instances For
              theorem topToCompHaus_obj (X : TopCat) :
              (topToCompHaus.obj X).toTop = StoneCech X

              An explicit limit cone for a functor F : J ⥤ CompHaus, defined in terms of TopCat.limitCone.

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

                The limit cone CompHaus.limitCone F is indeed a limit cone.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[reducible, inline]

                  Every CompHausLike admits a functor to CompHaus.

                  Equations
                  Instances For