mathlib documentation

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:

See the file category_theory.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.

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

def Compactum  :
Type (u_1+1)

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

Equations

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

Equations

The inclusion of X into ultrafilter X.

Equations
@[simp]
theorem Compactum.str_incl (X : Compactum) (x : X) :
X.str (X.incl x) = x

@[simp]
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

@[instance]

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.

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

Any continuous map between Compacta is a morphism of compacta.

Equations

The functor functor from Compactum to CompHaus.

Equations

The functor Compactum_to_CompHaus is full.

Equations

The functor Compactum_to_CompHaus is faithful.