# mathlibdocumentation

topology.category.CompHaus

# 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 Top. The fully faithful functor CompHaus ⥤ Top is denoted CompHaus_to_Top.

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

structure CompHaus  :
Type (u_1+1)

The type of Compact Hausdorff topological spaces.

@[instance]

Equations
@[instance]

Equations
@[instance]

@[instance]

@[instance]

Equations

The fully faithful embedding of CompHaus in Top.

Equations
@[instance]

Equations