# mathlibdocumentation

topology.category.CompHaus.default

# 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]
def CompHaus.has_coe_to_sort  :
(Type u_1)
Equations
@[instance]
@[instance]
@[instance]
Equations
@[instance]
Equations
@[simp]
theorem CompHaus.coe_to_Top {X : CompHaus} :
def CompHaus.of (X : Type u_1) [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) [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.

theorem CompHaus.is_iso_of_bijective {X Y : CompHaus} (f : X Y) (bij : function.bijective f) :

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
• = let _inst : := _ in

The fully faithful embedding of CompHaus in Top.

Equations
@[simp]
theorem CompHaus_to_Top_map (f : x y) :
@[instance]
@[simp]
theorem CompHaus_to_Top_obj (self : CompHaus) :
@[instance]
def StoneCech_obj (X : Top) :

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

Equations
@[simp]
theorem StoneCech_obj_to_Top_str_is_open (X : Top) (s : set ) :
@[simp]
def stone_cech_equivalence (X : Top) (Y : CompHaus) :
Y) (X

(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
theorem Top_to_CompHaus_obj (X : Top) :
@[instance]

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

Equations
@[instance]
Equations
@[instance]
@[instance]
def CompHaus.limit_cone {J : Type u} (F : J CompHaus) :

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

Equations
def CompHaus.limit_cone_is_limit {J : Type u} (F : J CompHaus) :

The limit cone CompHaus.limit_cone F is indeed a limit cone.

Equations
theorem CompHaus.epi_iff_surjective {X Y : CompHaus} (f : X Y) :
theorem CompHaus.mono_iff_injective {X Y : CompHaus} (f : X Y) :