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
The fully faithful functor
CompHaus ⥤ Top is denoted
Note: The file
topology/category/Compactum.lean provides the equivalence between
which is defined as the category of algebras for the ultrafilter monad, and
Compactum_to_CompHaus is the functor from
CompHaus which is proven to be an
equivalence of categories in
topology/category/Compactum.lean for a more detailed discussion where these definitions are
(Implementation) The bijection of homsets to establish the reflective adjunction of compact Hausdorff spaces in topological spaces.
The limit cone
CompHaus.limit_cone F is indeed a limit cone.