mathlib documentation

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 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.

Instances for CompHaus
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, 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
Instances for CompHaus.of
@[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.

noncomputable 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
@[simp]
theorem CompHaus_to_Top_obj (self : CompHaus) :
def StoneCech_obj (X : Top) :

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

Equations
noncomputable def stone_cech_equivalence (X : Top) (Y : CompHaus) :

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

Equations
noncomputable def Top_to_CompHaus  :

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

Equations
@[protected, 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