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 Mathlib/CategoryTheory/Monad/Algebra.lean 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.ofTypeMonad Ultrafilter).Algebra

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance instInhabitedCompactum : Inhabited Compactum

Equations

• instInhabitedCompactum = { default := instInhabitedCompactum._aux_1 }

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

The forgetful functor to TypeCat

Equations

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

instance Compactum.instFaithfulForget : forget.Faithful

@[implicit_reducible]

noncomputable instance Compactum.instCreatesLimitsForget : CategoryTheory.CreatesLimits forget

Equations

• Compactum.instCreatesLimitsForget = inferInstance

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

The "free" Compactum functor.

Equations

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

def Compactum.adj : free ⊣ forget

The adjunction between free and forget.

Equations

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

@[implicit_reducible]

instance Compactum.instCoeSortType : CoeSort Compactum (Type u_1)

Equations

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

@[implicit_reducible]

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

Equations

• Compactum.instFunLikeHomA = { coe := fun (f : X ⟶ Y) => ⇑(CategoryTheory.ConcreteCategory.hom f.f), coe_injective' := ⋯ }

@[implicit_reducible]

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

Equations

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

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.

Equations

• X.str = ⇑(CategoryTheory.ConcreteCategory.hom X.a)

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

The monadic join.

Equations

• X.join = ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.ofTypeMonad Ultrafilter).μ.app X.A))

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

The inclusion of X into Ultrafilter X.

Equations

• X.incl = ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.ofTypeMonad Ultrafilter).η.app X.1))

@[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)

@[implicit_reducible]

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

Equations

• Compactum.instTopologicalSpaceA = { IsOpen := fun (U : Set X.A) => ∀ (F : Ultrafilter X.A), X.str F ∈ U → U ∈ F, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

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.

Equations

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

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.

Equations

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

def compactumToCompHaus : CategoryTheory.Functor Compactum CompHaus

The functor from Compactum to CompHaus.

Equations

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

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.

Equations

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

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.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• Profinite.forgetCreatesLimits = id inferInstance