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 TopCat. The fully faithful functor CompHaus ⥤ TopCat is denoted compHausToTop.

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. CompactumToCompHaus is the functor from Compactum to CompHaus which is proven to be an equivalence of categories in CompactumToCompHaus.isEquivalence. 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.

• toTop : TopCat

The underlying topological space of an object of CompHaus.

• is_compact : CompactSpace self.toTop

The underlying topological space is compact.

• is_hausdorff : T2Space self.toTop

The underlying topological space is T2.

Instances For
theorem CompHaus.is_compact (self : CompHaus) :
CompactSpace self.toTop

The underlying topological space is compact.

theorem CompHaus.is_hausdorff (self : CompHaus) :
T2Space self.toTop

The underlying topological space is T2.

Equations
Equations
Equations
• =
def CompHaus.of (X : Type u_1) [] [] [] :

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

Equations
Instances For
@[simp]
theorem CompHaus.coe_of (X : Type u_1) [] [] [] :
().toTop = X
Equations
• X.instTopologicalSpaceObjForget = let_fun this := inferInstance; this
Equations
• =
theorem CompHaus.isClosedMap {X : CompHaus} {Y : CompHaus} (f : X Y) :

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

theorem CompHaus.isIso_of_bijective {X : CompHaus} {Y : CompHaus} (f : X Y) (bij : ) :

Any continuous bijection of compact Hausdorff spaces is an isomorphism.

noncomputable def CompHaus.isoOfBijective {X : CompHaus} {Y : CompHaus} (f : X Y) (bij : ) :
X Y

Any continuous bijection of compact Hausdorff spaces induces an isomorphism.

Equations
Instances For
@[simp]
theorem CompHaus.isoOfHomeo_inv {X : CompHaus} {Y : CompHaus} (f : X.toTop ≃ₜ Y.toTop) :
.inv = { toFun := f.symm, continuous_toFun := }
@[simp]
theorem CompHaus.isoOfHomeo_hom {X : CompHaus} {Y : CompHaus} (f : X.toTop ≃ₜ Y.toTop) :
.hom = { toFun := f, continuous_toFun := }
def CompHaus.isoOfHomeo {X : CompHaus} {Y : CompHaus} (f : X.toTop ≃ₜ Y.toTop) :
X Y

Construct an isomorphism from a homeomorphism.

Equations
• = { hom := { toFun := f, continuous_toFun := }, inv := { toFun := f.symm, continuous_toFun := }, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CompHaus.homeoOfIso_apply {X : CompHaus} {Y : CompHaus} (f : X Y) (a : X) :
a = f.hom a
@[simp]
theorem CompHaus.homeoOfIso_symm_apply {X : CompHaus} {Y : CompHaus} (f : X Y) (a : Y) :
.symm a = f.inv a
def CompHaus.homeoOfIso {X : CompHaus} {Y : CompHaus} (f : X Y) :
X.toTop ≃ₜ Y.toTop

Construct a homeomorphism from an isomorphism.

Equations
• = { toFun := f.hom, invFun := f.inv, left_inv := , right_inv := , continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem CompHaus.isoEquivHomeo_apply {X : CompHaus} {Y : CompHaus} (f : X Y) :
CompHaus.isoEquivHomeo f =
@[simp]
theorem CompHaus.isoEquivHomeo_symm_apply {X : CompHaus} {Y : CompHaus} (f : X.toTop ≃ₜ Y.toTop) :
CompHaus.isoEquivHomeo.symm f =
def CompHaus.isoEquivHomeo {X : CompHaus} {Y : CompHaus} :
(X Y) (X.toTop ≃ₜ Y.toTop)

The equivalence between isomorphisms in CompHaus and homeomorphisms of topological spaces.

Equations
• CompHaus.isoEquivHomeo = { toFun := CompHaus.homeoOfIso, invFun := CompHaus.isoOfHomeo, left_inv := , right_inv := }
Instances For
@[simp]
theorem compHausToTop_map :
∀ {X Y : } (f : X Y), compHausToTop.map f = f
@[simp]
theorem compHausToTop_obj (self : CompHaus) :
compHausToTop.obj self = self.toTop

The fully faithful embedding of CompHaus in TopCat.

Equations
Instances For
instance CompHaus.forget_reflectsIsomorphisms :
.ReflectsIsomorphisms
Equations
@[simp]
theorem stoneCechObj_toTop_str_IsOpen (X : TopCat) (s : Set ()) :
= IsOpen (Quotient.mk' ⁻¹' s)
@[simp]
theorem stoneCechObj_toTop_α (X : TopCat) :
().toTop =

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

Equations
Instances For
noncomputable def stoneCechEquivalence (X : TopCat) (Y : CompHaus) :
() (X compHausToTop.obj Y)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def topToCompHaus :

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

Equations
Instances For
theorem topToCompHaus_obj (X : TopCat) :
(topToCompHaus.obj X).toTop =
noncomputable instance compHausToTop.reflective :

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

Equations
noncomputable instance compHausToTop.createsLimits :
Equations
Equations
Equations
def CompHaus.limitCone {J : Type v} (F : ) :

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

Equations
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CompHaus.epi_iff_surjective {X : CompHaus} {Y : CompHaus} (f : X Y) :
theorem CompHaus.mono_iff_injective {X : CompHaus} {Y : CompHaus} (f : X Y) :