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

source
structure CompHaus  :
Type (u_1+1)

The type of Compact Hausdorff topological spaces.

source
@[protected, instance]
def CompHaus.inhabited  :
inhabited CompHaus
Equations
source
@[protected, instance]
def CompHaus.has_coe_to_sort  :
has_coe_to_sort CompHaus
Equations
source
@[protected, instance]
def CompHaus.compact_space {X : CompHaus} :
compact_space ↥X
source
@[protected, instance]
def CompHaus.t2_space {X : CompHaus} :
t2_space ↥X
source
@[protected, instance]
def CompHaus.category  :
category_theory.category CompHaus
Equations
source
@[protected, instance]
def CompHaus.concrete_category  :
category_theory.concrete_category CompHaus
Equations
source
@[simp]
theorem CompHaus.coe_to_Top {X : CompHaus} :
↥(X.to_Top) = ↥X
source
def CompHaus.of (X : Type u_1) [topological_space X] [compact_space X] [t2_space X] :
CompHaus

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

Equations
source
@[simp]
theorem CompHaus.coe_of (X : Type u_1) [topological_space X] [compact_space X] [t2_space X] :
↥(CompHaus.of X) = X
source
theorem CompHaus.is_closed_map {X Y : CompHaus} (f : X ⟶ Y) :
is_closed_map ⇑f

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

source
theorem CompHaus.is_iso_of_bijective {X Y : CompHaus} (f : X ⟶ Y) (bij : function.bijective ⇑f) :
category_theory.is_iso f

Any continuous bijection of compact Hausdorff spaces is an isomorphism.

source
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
source
def CompHaus_to_Top  :
CompHaus ⥤ Top

The fully faithful embedding of CompHaus in Top.

Equations
source
@[simp]
theorem CompHaus_to_Top_map (x y : category_theory.induced_category Top CompHaus.to_Top) (f : x ⟶ y) :
CompHaus_to_Top.map f = f
source
@[protected, instance]
def CompHaus_to_Top.faithful  :
category_theory.faithful CompHaus_to_Top
source
@[simp]
theorem CompHaus_to_Top_obj (c : CompHaus) :
CompHaus_to_Top.obj c = c.to_Top
source
@[protected, instance]
def CompHaus_to_Top.full  :
category_theory.full CompHaus_to_Top
source
@[protected, instance]
def CompHaus.forget_reflects_isomorphisms  :
category_theory.reflects_isomorphisms (category_theory.forget CompHaus)
source
def StoneCech_obj (X : Top) :
CompHaus

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

Equations
source
@[simp]
theorem StoneCech_obj_to_Top_str_is_open (X : Top) (s : set (quotient (stone_cech_setoid ↥X))) :
topological_space.is_open (StoneCech_obj X).to_Top.str s = ultrafilter.topological_space.is_open (quotient.mk ⁻¹' s)
source
@[simp]
theorem StoneCech_obj_to_Top_α (X : Top) :
↥((StoneCech_obj X).to_Top) = stone_cech ↥X
source
def stone_cech_equivalence (X : Top) (Y : CompHaus) :
(StoneCech_obj X ⟶ Y) ≃ (X ⟶ CompHaus_to_Top.obj Y)

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

Equations
source
def Top_to_CompHaus  :
Top ⥤ CompHaus

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

Equations
source
theorem Top_to_CompHaus_obj (X : Top) :
↥(Top_to_CompHaus.obj X) = stone_cech ↥X
source
@[protected, instance]
def CompHaus_to_Top.reflective  :
category_theory.reflective CompHaus_to_Top

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

Equations
source
@[protected, instance]
def CompHaus_to_Top.creates_limits  :
category_theory.creates_limits CompHaus_to_Top
Equations
source
@[protected, instance]
def CompHaus.has_limits  :
category_theory.limits.has_limits CompHaus
source
@[protected, instance]
def CompHaus.has_colimits  :
category_theory.limits.has_colimits CompHaus
source
def CompHaus.limit_cone {J : Type u} [category_theory.small_category J] (F : J ⥤ CompHaus) :
category_theory.limits.cone F

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

Equations
source
def CompHaus.limit_cone_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ CompHaus) :
category_theory.limits.is_limit (CompHaus.limit_cone F)

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

Equations