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
Any continuous bijection of compact Hausdorff spaces induces an isomorphism.
(Implementation) The bijection of homsets to establish the reflective adjunction of compact Hausdorff spaces in topological spaces.
The Stone-Cech compactification functor from topological spaces to compact Hausdorff spaces, left adjoint to the inclusion functor.
The limit cone
CompHaus.limit_cone F is indeed a limit cone.