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.

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

The forgetful functor to Type*

instance Compactum.instFaithfulCompactumInstCompactumCategoryTypeTypesForget : CategoryTheory.Faithful Compactum.forget

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

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

The "free" Compactum functor.

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

The adjunction between free and forget.

instance Compactum.instConcreteCategoryCompactumInstCompactumCategory : CategoryTheory.ConcreteCategory Compactum

instance Compactum.instCoeSortCompactumType : CoeSort Compactum (Type u_1)

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

instance Compactum.instHasLimitsCompactumInstCompactumCategory : CategoryTheory.Limits.HasLimits Compactum

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

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

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

The monadic join.

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

The inclusion of X into Ultrafilter X.

@[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) : CategoryTheory.Monad.Algebra.Hom.f (Type u_1) CategoryTheory.types (CategoryTheory.ofTypeMonad Ultrafilter) X Y 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

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

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

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.

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.

def compactumToCompHaus : CategoryTheory.Functor Compactum CompHaus

The functor functor from Compactum to CompHaus.

def compactumToCompHaus.full : CategoryTheory.Full compactumToCompHaus

The functor compactumToCompHaus is full.

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.

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.

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

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

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

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