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.

instance CompHaus.instInhabitedCompHaus : Inhabited CompHaus

Equations

• CompHaus.instInhabitedCompHaus = { default := CompHaus.mk { α := PEmpty.{u_1 + 1} , str := inferInstance } }

instance CompHaus.instCoeSortCompHausType : CoeSort CompHaus (Type u_1)

Equations

• CompHaus.instCoeSortCompHausType = { coe := fun (X : CompHaus) => ↑X.toTop }

instance CompHaus.instCompactSpaceαTopologicalSpaceToTopTopologicalSpace_coe {X : CompHaus} : CompactSpace ↑X.toTop

Equations

• ⋯ = ⋯

instance CompHaus.instT2SpaceαTopologicalSpaceToTopTopologicalSpace_coe {X : CompHaus} : T2Space ↑X.toTop

Equations

• ⋯ = ⋯

instance CompHaus.category : CategoryTheory.Category.{u_1, u_1 + 1} CompHaus

Equations

• CompHaus.category = CategoryTheory.InducedCategory.category CompHaus.toTop

instance CompHaus.concreteCategory : CategoryTheory.ConcreteCategory CompHaus

Equations

• CompHaus.concreteCategory = CategoryTheory.InducedCategory.concreteCategory CompHaus.toTop

def CompHaus.of (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] : CompHaus

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

Equations

• CompHaus.of X = CompHaus.mk (TopCat.of X)

@[simp]

theorem CompHaus.coe_of (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] : ↑(CompHaus.of X).toTop = X

instance CompHaus.instTopologicalSpaceObjCompHausToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory (X : CompHaus) : TopologicalSpace ((CategoryTheory.forget CompHaus).obj X)

Equations

• CompHaus.instTopologicalSpaceObjCompHausToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory X = let_fun this := inferInstance; this

instance CompHaus.instCompactSpaceObjCompHausToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategoryInstTopologicalSpaceObjCompHausToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory (X : CompHaus) : CompactSpace ((CategoryTheory.forget CompHaus).obj X)

Equations

• ⋯ = ⋯

instance CompHaus.instT2SpaceObjCompHausToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategoryInstTopologicalSpaceObjCompHausToQuiverToCategoryStructCategoryTypeTypesToPrefunctorForgetConcreteCategory (X : CompHaus) : T2Space ((CategoryTheory.forget CompHaus).obj X)

Equations

• ⋯ = ⋯

theorem CompHaus.isClosedMap {X : CompHaus} {Y : CompHaus} (f : X ⟶ Y) : IsClosedMap ⇑f

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

theorem CompHaus.isIso_of_bijective {X : CompHaus} {Y : CompHaus} (f : X ⟶ Y) (bij : Function.Bijective ⇑f) : CategoryTheory.IsIso f

Any continuous bijection of compact Hausdorff spaces is an isomorphism.

noncomputable def CompHaus.isoOfBijective {X : CompHaus} {Y : CompHaus} (f : X ⟶ Y) (bij : Function.Bijective ⇑f) : X ≅ Y

Any continuous bijection of compact Hausdorff spaces induces an isomorphism.

Equations

• CompHaus.isoOfBijective f bij = CategoryTheory.asIso f

@[simp]

theorem CompHaus.isoOfHomeo_inv {X : CompHaus} {Y : CompHaus} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : (CompHaus.isoOfHomeo f).inv = { toFun := ⇑(Homeomorph.symm f), continuous_toFun := ⋯ }

@[simp]

theorem CompHaus.isoOfHomeo_hom {X : CompHaus} {Y : CompHaus} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : (CompHaus.isoOfHomeo f).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

• CompHaus.isoOfHomeo f = { hom := { toFun := ⇑f, continuous_toFun := ⋯ }, inv := { toFun := ⇑(Homeomorph.symm f), continuous_toFun := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CompHaus.homeoOfIso_apply {X : CompHaus} {Y : CompHaus} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj X) : (CompHaus.homeoOfIso f) a = f.hom a

@[simp]

theorem CompHaus.homeoOfIso_symm_apply {X : CompHaus} {Y : CompHaus} (f : X ≅ Y) (a : (CategoryTheory.forget CompHaus).obj Y) : (Homeomorph.symm (CompHaus.homeoOfIso f)) 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

• CompHaus.homeoOfIso f = { toEquiv := { toFun := ⇑f.hom, invFun := ⇑f.inv, left_inv := ⋯, right_inv := ⋯ }, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem CompHaus.isoEquivHomeo_symm_apply {X : CompHaus} {Y : CompHaus} (f : ↑X.toTop ≃ₜ ↑Y.toTop) : CompHaus.isoEquivHomeo.symm f = CompHaus.isoOfHomeo f

@[simp]

theorem CompHaus.isoEquivHomeo_apply {X : CompHaus} {Y : CompHaus} (f : X ≅ Y) : CompHaus.isoEquivHomeo f = CompHaus.homeoOfIso 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 := ⋯ }

@[simp]

theorem compHausToTop_map : ∀ {X Y : CategoryTheory.InducedCategory TopCat CompHaus.toTop} (f : X ⟶ Y), compHausToTop.map f = f

@[simp]

theorem compHausToTop_obj (self : CompHaus) : compHausToTop.obj self = self.toTop

def compHausToTop : CategoryTheory.Functor CompHaus TopCat

The fully faithful embedding of CompHaus in TopCat.

Equations

• compHausToTop = CategoryTheory.inducedFunctor CompHaus.toTop

instance instFullCompHausCategoryTopCatInstTopCatLargeCategoryCompHausToTop : CategoryTheory.Functor.Full compHausToTop

Equations

• instFullCompHausCategoryTopCatInstTopCatLargeCategoryCompHausToTop = let_fun this := inferInstance; this

instance instFaithfulCompHausCategoryTopCatInstTopCatLargeCategoryCompHausToTop : CategoryTheory.Functor.Faithful compHausToTop

Equations

• instFaithfulCompHausCategoryTopCatInstTopCatLargeCategoryCompHausToTop = ⋯

instance instCompactSpaceαTopologicalSpaceObjCompHausToQuiverToCategoryStructCategoryTopCatInstTopCatLargeCategoryToPrefunctorCompHausToTopTopologicalSpace_coe (X : CompHaus) : CompactSpace ↑(compHausToTop.obj X)

Equations

• ⋯ = ⋯

instance instT2SpaceαTopologicalSpaceObjCompHausToQuiverToCategoryStructCategoryTopCatInstTopCatLargeCategoryToPrefunctorCompHausToTopTopologicalSpace_coe (X : CompHaus) : T2Space ↑(compHausToTop.obj X)

Equations

• ⋯ = ⋯

instance CompHaus.forget_reflectsIsomorphisms : CategoryTheory.Functor.ReflectsIsomorphisms (CategoryTheory.forget CompHaus)

Equations

• CompHaus.forget_reflectsIsomorphisms = ⋯

@[simp]

theorem stoneCechObj_toTop_α (X : TopCat) : ↑(stoneCechObj X).toTop = StoneCech ↑X

@[simp]

theorem stoneCechObj_toTop_str_IsOpen (X : TopCat) (s : Set (Quotient (stoneCechSetoid ↑X))) : TopologicalSpace.IsOpen s = IsOpen (Quotient.mk' ⁻¹' s)

def stoneCechObj (X : TopCat) : CompHaus

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

Equations

• stoneCechObj X = CompHaus.of (StoneCech ↑X)

noncomputable def stoneCechEquivalence (X : TopCat) (Y : CompHaus) : (stoneCechObj X ⟶ Y) ≃ (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.

noncomputable def topToCompHaus : CategoryTheory.Functor TopCat CompHaus

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

Equations

• topToCompHaus = CategoryTheory.Adjunction.leftAdjointOfEquiv stoneCechEquivalence topToCompHaus.proof_1

theorem topToCompHaus_obj (X : TopCat) : ↑(topToCompHaus.obj X).toTop = StoneCech ↑X

noncomputable instance compHausToTop.reflective : CategoryTheory.Reflective compHausToTop

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

Equations

• compHausToTop.reflective = CategoryTheory.Reflective.mk

noncomputable instance compHausToTop.createsLimits : CategoryTheory.CreatesLimits compHausToTop

Equations

• compHausToTop.createsLimits = CategoryTheory.monadicCreatesLimits compHausToTop

instance CompHaus.hasLimits : CategoryTheory.Limits.HasLimits CompHaus

Equations

• CompHaus.hasLimits = ⋯

instance CompHaus.hasColimits : CategoryTheory.Limits.HasColimits CompHaus

Equations

• CompHaus.hasColimits = ⋯

def CompHaus.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CompHaus) : CategoryTheory.Limits.Cone F

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

Equations

• One or more equations did not get rendered due to their size.

def CompHaus.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CompHaus) : CategoryTheory.Limits.IsLimit (CompHaus.limitCone F)

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

Equations

• One or more equations did not get rendered due to their size.

theorem CompHaus.epi_iff_surjective {X : CompHaus} {Y : CompHaus} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ Function.Surjective ⇑f

theorem CompHaus.mono_iff_injective {X : CompHaus} {Y : CompHaus} (f : X ⟶ Y) : CategoryTheory.Mono f ↔ Function.Injective ⇑f

@[inline, reducible]

abbrev CompHausMax : Type ((max w w') + 1)

Many definitions involving universe inequalities in Mathlib are expressed through use of max u v. Unfortunately, this leads to unbound universes which cannot be solved for during unification, eg max u v =?= max v ?. The current solution is to wrap Type max u v in TypeMax.{u,v} to expose both universe parameters directly. Similarly, for other concrete categories for which we need to refer to the maximum of two universes (e.g. any category for which we are constructing limits), we need an analogous abbreviation.

Equations

• CompHausMax = CompHaus