mathlib documentation


Compacta and Compact Hausdorff Spaces

Recall that, given a monad M on Type*, an algebra for M consists of the following data:

See the file category_theory.monad.algebra for a general version, as well as the following link.

This file proves the equivalence between the category of compact Hausdorff topological spaces and the category of algebras for the ultrafilter monad.


Here are the main objects introduced in this file.

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:

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.of_topological_space can be used to construct a Compactum from a topological space which satisfies compact_space and t2_space.

We also add wrappers around structures which already exist. Here are the main ones, all in the Compactum namespace:


def Compactum  :
Type (u_1+1)

The type Compactum of Compacta, defined as algebras for the ultrafilter monad.


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


The inclusion of X into ultrafilter X.

theorem Compactum.str_incl (X : Compactum) (x : X) :
X.str (X.incl x) = x

theorem Compactum.str_hom_commute (X Y : Compactum) (f : X Y) (xs : filter.ultrafilter X) :

theorem Compactum.is_closed_iff {X : Compactum} (S : set X) :
is_closed S ∀ (F : filter.ultrafilter X), S F.valX.str F S

theorem Compactum.is_closed_cl {X : Compactum} (A : set X) :
is_closed (cl A)

theorem Compactum.str_eq_of_le_nhds {X : Compactum} (F : filter.ultrafilter X) (x : X) :
F.val 𝓝 xX.str F = x

theorem Compactum.le_nhds_of_str_eq {X : Compactum} (F : filter.ultrafilter X) (x : X) :
X.str F = xF.val 𝓝 x


theorem Compactum.Lim_eq_str {X : Compactum} (F : filter.ultrafilter X) :
F.Lim = X.str F

The structure map of a compactum actually computes limits.

theorem Compactum.cl_eq_closure {X : Compactum} (A : set X) :
cl A = closure A

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

Any morphism of compacta is continuous.

Given any compact Hausdorff space, we construct a Compactum.

def Compactum.hom_of_continuous {X Y : Compactum} (f : X → Y) (cont : continuous f) :

Any continuous map between Compacta is a morphism of compacta.


The functor functor from Compactum to CompHaus.


The functor Compactum_to_CompHaus is full.


The functor Compactum_to_CompHaus is faithful.