Compacta and Compact Hausdorff Spaces

Recall that, given a monad M on Type*, an algebra for M consists of the following data:

• A type X : Type*
• A "structure" map M X → X. This data must also satisfy a distributivity and unit axiom, and algebras for M form a category in an evident way.

See the file CategoryTheory.Monad.Algebra for a general version, as well as the following link. https://ncatlab.org/nlab/show/monad

This file proves the equivalence between the category of compact Hausdorff topological spaces and the category of algebras for the ultrafilter monad.

Notation:

Here are the main objects introduced in this file.

• Compactum is the type of compacta, which we define as algebras for the ultrafilter monad.
• compactumToCompHaus is the functor Compactum ⥤ CompHaus. Here CompHaus is the usual category of compact Hausdorff spaces.
• compactumToCompHaus.isEquivalence is a term of type IsEquivalence compactumToCompHaus.

The proof of this equivalence is a bit technical. But the idea is quite simply that the structure map Ultrafilter X → X for an algebra X of the ultrafilter monad should be considered as the map sending an ultrafilter to its limit in X. The topology on X is then defined by mimicking the characterization of open sets in terms of ultrafilters.

Any X : Compactum is endowed with a coercion to Type*, as well as the following instances:

• TopologicalSpace X.
• CompactSpace X.
• T2Space X.

Any morphism f : X ⟶ Y of is endowed with a coercion to a function X → Y, which is shown to be continuous in continuous_of_hom.

The function Compactum.ofTopologicalSpace can be used to construct a Compactum from a topological space which satisfies CompactSpace and T2Space.

We also add wrappers around structures which already exist. Here are the main ones, all in the Compactum namespace:

• forget : Compactum ⥤ Type* is the forgetful functor, which induces a ConcreteCategory instance for Compactum.
• free : Type* ⥤ Compactum is the left adjoint to forget, and the adjunction is in adj.
• str : Ultrafilter X → X is the structure map for X : Compactum. The notation X.str is preferred.
• join : Ultrafilter (Ultrafilter X) → Ultrafilter X is the monadic join for X : Compactum. Again, the notation X.join is preferred.
• incl : X → Ultrafilter X is the unit for X : Compactum. The notation X.incl is preferred.

References

• E. Manes, Algebraic Theories, Graduate Texts in Mathematics 26, Springer-Verlag, 1976.
• https://ncatlab.org/nlab/show/ultrafilter

def Compactum : Type (u_1 + 1)

The type Compactum of Compacta, defined as algebras for the ultrafilter monad.

Equations

• Compactum = CategoryTheory.Monad.Algebra (CategoryTheory.ofTypeMonad Ultrafilter)

def Compactum.forget : CategoryTheory.Functor Compactum (Type u_1)

The forgetful functor to Type*

Equations

• Compactum.forget = CategoryTheory.Monad.forget (CategoryTheory.ofTypeMonad Ultrafilter)

instance Compactum.instFaithfulCompactumInstCompactumCategoryTypeTypesForget : CategoryTheory.Faithful Compactum.forget

Equations

• Compactum.instFaithfulCompactumInstCompactumCategoryTypeTypesForget = ⋯

noncomputable instance Compactum.instCreatesLimitsCompactumInstCompactumCategoryTypeTypesForget : CategoryTheory.CreatesLimits Compactum.forget

Equations

• Compactum.instCreatesLimitsCompactumInstCompactumCategoryTypeTypesForget = let_fun this := inferInstance; this

def Compactum.free : CategoryTheory.Functor (Type u_1) Compactum

The "free" Compactum functor.

Equations

• Compactum.free = CategoryTheory.Monad.free (CategoryTheory.ofTypeMonad Ultrafilter)

def Compactum.adj : Compactum.free ⊣ Compactum.forget

The adjunction between free and forget.

Equations

• Compactum.adj = CategoryTheory.Monad.adj (CategoryTheory.ofTypeMonad Ultrafilter)

instance Compactum.instConcreteCategoryCompactumInstCompactumCategory : CategoryTheory.ConcreteCategory Compactum

Equations

• Compactum.instConcreteCategoryCompactumInstCompactumCategory = CategoryTheory.ConcreteCategory.mk Compactum.forget

instance Compactum.instCoeSortCompactumType : CoeSort Compactum (Type u_1)

Equations

• Compactum.instCoeSortCompactumType = { coe := fun (X : Compactum) => X.A }

instance Compactum.instCoeFunHomCompactumToQuiverToCategoryStructInstCompactumCategoryForAllATypeTypesOfTypeMonadUltrafilterMonadLawfulMonad {X : Compactum} {Y : Compactum} : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => X.A → Y.A

Equations

• Compactum.instCoeFunHomCompactumToQuiverToCategoryStructInstCompactumCategoryForAllATypeTypesOfTypeMonadUltrafilterMonadLawfulMonad = { coe := fun (f : X ⟶ Y) => f.f }

instance Compactum.instHasLimitsCompactumInstCompactumCategory : CategoryTheory.Limits.HasLimits Compactum

Equations

• Compactum.instHasLimitsCompactumInstCompactumCategory = ⋯

def Compactum.str (X : Compactum) : Ultrafilter X.A → X.A

The structure map for a compactum, essentially sending an ultrafilter to its limit.

Equations

• Compactum.str X = X.a

def Compactum.join (X : Compactum) : Ultrafilter (Ultrafilter X.A) → Ultrafilter X.A

The monadic join.

Equations

• Compactum.join X = (CategoryTheory.Monad.μ (CategoryTheory.ofTypeMonad Ultrafilter)).app X.A

def Compactum.incl (X : Compactum) : X.A → Ultrafilter X.A

The inclusion of X into Ultrafilter X.

Equations

• Compactum.incl X = (CategoryTheory.Monad.η (CategoryTheory.ofTypeMonad Ultrafilter)).app X.1

@[simp]

theorem Compactum.str_incl (X : Compactum) (x : X.A) : Compactum.str X (Compactum.incl X x) = x

@[simp]

theorem Compactum.str_hom_commute (X : Compactum) (Y : Compactum) (f : X ⟶ Y) (xs : Ultrafilter X.A) : f.f (Compactum.str X xs) = Compactum.str Y (Ultrafilter.map f.f xs)

@[simp]

theorem Compactum.join_distrib (X : Compactum) (uux : Ultrafilter (Ultrafilter X.A)) : Compactum.str X (Compactum.join X uux) = Compactum.str X (Ultrafilter.map (Compactum.str X) uux)

instance Compactum.instTopologicalSpaceATypeTypesOfTypeMonadUltrafilterMonadLawfulMonad {X : Compactum} : TopologicalSpace X.A

Equations

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

theorem Compactum.isClosed_iff {X : Compactum} (S : Set X.A) : IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → Compactum.str X F ∈ S

instance Compactum.instCompactSpaceATypeTypesOfTypeMonadUltrafilterMonadLawfulMonadInstTopologicalSpaceATypeTypesOfTypeMonadUltrafilterMonadLawfulMonad {X : Compactum} : CompactSpace X.A

Equations

• ⋯ = ⋯

theorem Compactum.isClosed_cl {X : Compactum} (A : Set X.A) : IsClosed (Compactum.cl A)

theorem Compactum.str_eq_of_le_nhds {X : Compactum} (F : Ultrafilter X.A) (x : X.A) : ↑F ≤ nhds x → Compactum.str X F = x

theorem Compactum.le_nhds_of_str_eq {X : Compactum} (F : Ultrafilter X.A) (x : X.A) : Compactum.str X F = x → ↑F ≤ nhds x

instance Compactum.instT2SpaceATypeTypesOfTypeMonadUltrafilterMonadLawfulMonadInstTopologicalSpaceATypeTypesOfTypeMonadUltrafilterMonadLawfulMonad {X : Compactum} : T2Space X.A

Equations

• ⋯ = ⋯

theorem Compactum.lim_eq_str {X : Compactum} (F : Ultrafilter X.A) : Ultrafilter.lim F = Compactum.str X F

The structure map of a compactum actually computes limits.

theorem Compactum.cl_eq_closure {X : Compactum} (A : Set X.A) : Compactum.cl A = closure A

theorem Compactum.continuous_of_hom {X : Compactum} {Y : Compactum} (f : X ⟶ Y) : Continuous f.f

Any morphism of compacta is continuous.

noncomputable def Compactum.ofTopologicalSpace (X : Type u_1) [TopologicalSpace X] [CompactSpace X] [T2Space X] : Compactum

Given any compact Hausdorff space, we construct a Compactum.

Equations

• Compactum.ofTopologicalSpace X = { A := X, a := Ultrafilter.lim, unit := ⋯, assoc := ⋯ }

def Compactum.homOfContinuous {X : Compactum} {Y : Compactum} (f : X.A → Y.A) (cont : Continuous f) : X ⟶ Y

Any continuous map between Compacta is a morphism of compacta.

Equations

• Compactum.homOfContinuous f cont = { f := f, h := ⋯ }

def compactumToCompHaus : CategoryTheory.Functor Compactum CompHaus

The functor functor from Compactum to CompHaus.

Equations

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

def compactumToCompHaus.full : CategoryTheory.Full compactumToCompHaus

The functor compactumToCompHaus is full.

Equations

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

theorem compactumToCompHaus.faithful : CategoryTheory.Faithful compactumToCompHaus

The functor compactumToCompHaus is faithful.

def compactumToCompHaus.isoOfTopologicalSpace {D : CompHaus} : compactumToCompHaus.obj (Compactum.ofTopologicalSpace ↑D.toTop) ≅ D

This definition is used to prove essential surjectivity of compactumToCompHaus.

Equations

• compactumToCompHaus.isoOfTopologicalSpace = { hom := { toFun := id, continuous_toFun := ⋯ }, inv := { toFun := id, continuous_toFun := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem compactumToCompHaus.essSurj : CategoryTheory.EssSurj compactumToCompHaus

The functor compactumToCompHaus is essentially surjective.

noncomputable instance compactumToCompHaus.isEquivalence : CategoryTheory.IsEquivalence compactumToCompHaus

The functor compactumToCompHaus is an equivalence of categories.

Equations

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

def compactumToCompHausCompForget : CategoryTheory.Functor.comp compactumToCompHaus (CategoryTheory.forget CompHaus) ≅ Compactum.forget

The forgetful functors of Compactum and CompHaus are compatible via compactumToCompHaus.

Equations

• compactumToCompHausCompForget = CategoryTheory.NatIso.ofComponents (fun (X : Compactum) => CategoryTheory.eqToIso ⋯) @compactumToCompHausCompForget.proof_2

noncomputable instance CompHaus.forgetCreatesLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget CompHaus)

Equations

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

noncomputable instance Profinite.forgetCreatesLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget Profinite)

Equations

• Profinite.forgetCreatesLimits = let_fun this := inferInstance; this