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.

Notation: #

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:

References #

@[protected, instance]
def Compactum.forget  :
Compactum Type u_1

The forgetful functor to Type*

Instances for Compactum.forget
def  :
Type u_1 Compactum

The "free" Compactum functor.

@[protected, instance]
def Compactum.quiver.hom.has_coe_to_fun {X Y : Compactum} :
has_coe_to_fun (X Y) (λ (f : X Y), X → Y)

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

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 : ultrafilter X) :
f (X.str xs) = Y.str ( f xs)
theorem Compactum.join_distrib (X : Compactum) (uux : ultrafilter (ultrafilter X)) :
X.str (X.join uux) = X.str ( X.str uux)
@[protected, instance]
theorem Compactum.is_closed_iff {X : Compactum} (S : set X) :
is_closed S ∀ (F : ultrafilter X), S FX.str F S
@[protected, instance]
theorem Compactum.is_closed_cl {X : Compactum} (A : set X) :
is_closed (cl A)
theorem Compactum.str_eq_of_le_nhds {X : Compactum} (F : ultrafilter X) (x : X) :
F nhds xX.str F = x
theorem Compactum.le_nhds_of_str_eq {X : Compactum} (F : ultrafilter X) (x : X) :
X.str F = xF nhds x
@[protected, instance]
theorem Compactum.Lim_eq_str {X : Compactum} (F : 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.

noncomputable def Compactum.of_topological_space (X : Type u_1) [topological_space X] [compact_space X] [t2_space X] :

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.

Instances for Compactum_to_CompHaus

The functor Compactum_to_CompHaus is full.


The functor Compactum_to_CompHaus is faithful.

The functor Compactum_to_CompHaus is essentially surjective.