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]
@[simp]
theorem CompHaus.coe_to_Top {X : CompHaus} :
def CompHaus.of (X : Type u_1) [topological_space X] [compact_space X] [t2_space X] :

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

Equations
@[simp]
theorem CompHaus.coe_of (X : Type u_1) [topological_space X] [compact_space X] [t2_space X] :
theorem CompHaus.is_closed_map {X Y : CompHaus} (f : X Y) :

Any continuous function on compact Hausdorff spaces is a closed map.

Any continuous bijection of compact Hausdorff spaces is an isomorphism.

def CompHaus.iso_of_bijective {X Y : CompHaus} (f : X Y) (bij : function.bijective f) :
X Y

Any continuous bijection of compact Hausdorff spaces induces an isomorphism.

Equations
def StoneCech_obj (X : Top) :

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

Equations

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

Equations

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

Equations
@[instance]

The category of compact Hausdorff spaces is reflective in the category of topological spaces.

Equations

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

Equations