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.ofTypeMonad Ultrafilter).Algebra

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

The forgetful functor to Type*

Equations

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

instance Compactum.instFaithfulForget : Compactum.forget.Faithful

Equations

• Compactum.instFaithfulForget = ⋯

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

Equations

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

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

The "free" Compactum functor.

Equations

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

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

The adjunction between free and forget.

Equations

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

instance Compactum.instConcreteCategory : CategoryTheory.ConcreteCategory Compactum

Equations

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

instance Compactum.instCoeSortType : CoeSort Compactum (Type u_1)

Equations

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

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

Equations

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

instance Compactum.instHasLimits : CategoryTheory.Limits.HasLimits Compactum

Equations

• Compactum.instHasLimits = ⋯

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 = X.a

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

The monadic join.

Equations

• X.join = (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.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 : Compactum) (Y : Compactum) (f : X ⟶ Y) (xs : Ultrafilter X.A) : f.f (X.str xs) = Y.str (Ultrafilter.map f.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

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

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 → 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

Equations

• ⋯ = ⋯

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 : 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.

instance compactumToCompHaus.full : compactumToCompHaus.Full

The functor compactumToCompHaus is full.

Equations

• compactumToCompHaus.full = ⋯

instance compactumToCompHaus.faithful : compactumToCompHaus.Faithful

The functor compactumToCompHaus is faithful.

Equations

• compactumToCompHaus.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 := ⋯ }

instance compactumToCompHaus.essSurj : compactumToCompHaus.EssSurj

The functor compactumToCompHaus is essentially surjective.

Equations

• compactumToCompHaus.essSurj = ⋯

noncomputable instance compactumToCompHaus.isEquivalence : compactumToCompHaus.IsEquivalence

The functor compactumToCompHaus is an equivalence of categories.

Equations

• compactumToCompHaus.isEquivalence = CategoryTheory.Functor.IsEquivalence.ofFullyFaithfullyEssSurj compactumToCompHaus

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_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