Documentation

Mathlib.Topology.Category.CompHaus.Basic

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 Mathlib/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 Mathlib/Topology/Category/Compactum.lean for a more detailed discussion where these definitions are introduced.

Implementation #

The category CompHaus is defined using the structure CompHausLike. See the file CompHausLike.Basic for more information.

@[reducible, inline]

abbrev CompHaus :

Type (u_1 + 1)

The category of compact Hausdorff spaces.

Equations

CompHaus = CompHausLike fun (x : TopCat) => True

Instances For

instance CompHaus.instInhabited :

Inhabited CompHaus

Equations

CompHaus.instInhabited = { default := CompHausLike.mk { α := PEmpty.{?u.4 + 1} , str := inferInstance } trivial }

instance CompHaus.instCoeSortType :

CoeSort CompHaus (Type u_1)

Equations

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

instance CompHaus.instCompactSpaceαTopologicalSpaceToTopTrue {X : CompHaus} :

CompactSpace ↑X.toTop

Equations

⋯ = ⋯

instance CompHaus.instT2SpaceαTopologicalSpaceToTopTrue {X : CompHaus} :

T2Space ↑X.toTop

Equations

⋯ = ⋯

instance CompHaus.instHasPropTrue (X : Type u_1) [TopologicalSpace X] :

CompHausLike.HasProp (fun (x : TopCat) => True) X

Equations

⋯ = ⋯

@[reducible, inline]

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

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 = CompHausLike.of (fun (x : TopCat) => True) X

Instances For

CompHaus.projective_ultrafilter

@[reducible, inline]

abbrev compHausToTop :

CategoryTheory.Functor CompHaus TopCat

The fully faithful embedding of CompHaus in TopCat.

Equations

compHausToTop = CompHausLike.compHausLikeToTop fun (x : TopCat) => True

Instances For

@[simp]

theorem stoneCechObj_toTop_str_IsOpen (X : TopCat) (s : Set (Quotient (t2Setoid (PreStoneCech ↑X)))) :

TopologicalSpace.IsOpen s = IsOpen (Quotient.mk' ⁻¹' s)

@[simp]

theorem stoneCechObj_toTop_α (X : TopCat) :

↑(stoneCechObj X).toTop = StoneCech ↑X

def stoneCechObj (X : TopCat) :

(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 topToCompHaus (CategoryTheory.Adjunction.adjunctionOfEquivLeft stoneCechEquivalence topToCompHaus.proof_1)

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

@[reducible, inline]

abbrev compHausLikeToCompHaus (P : TopCat → Prop) :

CategoryTheory.Functor (CompHausLike P) CompHaus

Every CompHausLike admits a functor to CompHaus.

Equations

compHausLikeToCompHaus P = CompHausLike.toCompHausLike ⋯