mathlib documentation

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 CompHausTop 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]

The fully faithful embedding of CompHaus in Top.

Equations
@[instance]

Equations