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.

instance instCompactumCategory : CategoryTheory.Category.{u_1, u_1 + 1} Compactum

instance instCompactumInhabited : Inhabited Compactum

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

The forgetful functor to Type*

instance Compactum.instFaithfulForget : forget.Faithful

noncomputable instance Compactum.instCreatesLimitsForget : CategoryTheory.CreatesLimits forget

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

The "free" Compactum functor.

def Compactum.adj : free ⊣ forget

The adjunction between free and forget.

instance Compactum.instCoeSortType : CoeSort Compactum (Type u_1)

instance Compactum.instFunLikeHomA {X Y : Compactum} : FunLike (X ⟶ Y) X.A Y.A

instance Compactum.instConcreteCategoryHomA : CategoryTheory.ConcreteCategory Compactum fun (x1 x2 : Compactum) => x1 ⟶ x2

instance Compactum.instHasLimits : 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) : X.str (X.incl x) = x

@[simp]

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

@[simp]

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

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

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

instance Compactum.instCompactSpaceA {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 → X.str F = x

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

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

theorem Compactum.lim_eq_str {X : Compactum} (F : Ultrafilter X.A) : F.lim = X.str 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 Y : Compactum} (f : X ⟶ Y) : Continuous ⇑(CategoryTheory.ConcreteCategory.hom 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 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.

instance compactumToCompHaus.full : compactumToCompHaus.Full

The functor compactumToCompHaus is full.

instance compactumToCompHaus.faithful : compactumToCompHaus.Faithful

The functor compactumToCompHaus is faithful.

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

This definition is used to prove essential surjectivity of compactumToCompHaus.

instance compactumToCompHaus.essSurj : compactumToCompHaus.EssSurj

The functor compactumToCompHaus is essentially surjective.

instance compactumToCompHaus.isEquivalence : compactumToCompHaus.IsEquivalence

The functor compactumToCompHaus is an equivalence of categories.

def compactumToCompHausCompForget : compactumToCompHaus.comp (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)