# Documentation

Mathlib.Topology.Category.Compactum

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

Instances For

The forgetful functor to Type*

Instances For

The "free" Compactum functor.

Instances For

The adjunction between free and forget.

Instances For
def Compactum.str (X : Compactum) :
Ultrafilter X.AX.A

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

Instances For

The monadic join.

Instances For
def Compactum.incl (X : Compactum) :
X.AUltrafilter X.A

The inclusion of X into Ultrafilter X.

Instances For
@[simp]
theorem Compactum.str_incl (X : Compactum) (x : X.A) :
@[simp]
theorem Compactum.str_hom_commute (X : Compactum) (Y : Compactum) (f : X Y) (xs : Ultrafilter X.A) :
theorem Compactum.isClosed_iff {X : Compactum} (S : Set X.A) :
∀ (F : Ultrafilter X.A), S F S
theorem Compactum.isClosed_cl {X : Compactum} (A : Set X.A) :
theorem Compactum.str_eq_of_le_nhds {X : Compactum} (F : Ultrafilter X.A) (x : X.A) :
F nhds x = x
theorem Compactum.le_nhds_of_str_eq {X : Compactum} (F : Ultrafilter X.A) (x : X.A) :
= xF nhds x
theorem Compactum.lim_eq_str {X : Compactum} (F : Ultrafilter X.A) :

The structure map of a compactum actually computes limits.

theorem Compactum.cl_eq_closure {X : Compactum} (A : Set X.A) :
theorem Compactum.continuous_of_hom {X : Compactum} {Y : Compactum} (f : X Y) :

Any morphism of compacta is continuous.

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

Given any compact Hausdorff space, we construct a Compactum.

Instances For
def Compactum.homOfContinuous {X : Compactum} {Y : Compactum} (f : X.AY.A) (cont : ) :
X Y

Any continuous map between Compacta is a morphism of compacta.

Instances For

The functor functor from Compactum to CompHaus.

Instances For

The functor compactumToCompHaus is full.

Instances For

The functor compactumToCompHaus is faithful.

This definition is used to prove essential surjectivity of compactumToCompHaus.

Instances For

The functor compactumToCompHaus is essentially surjective.

noncomputable instance compactumToCompHaus.isEquivalence :

The functor compactumToCompHaus is an equivalence of categories.

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

Instances For
noncomputable instance CompHaus.forgetCreatesLimits :
noncomputable instance Profinite.forgetCreatesLimits :