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
def Compactum.forget  :
Compactum Type u_1

The forgetful functor to Type*

Equations
def Compactum.free  :
Type u_1 Compactum

The "free" Compactum functor.

Equations

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

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 : ultrafilter X) :
f (X.str xs) = Y.str (ultrafilter.map f xs)
@[simp]
theorem Compactum.join_distrib (X : Compactum) (uux : ultrafilter (ultrafilter X)) :
X.str (X.join uux) = X.str (ultrafilter.map X.str uux)
@[instance]
Equations
theorem Compactum.is_closed_iff {X : Compactum} (S : set X) :
is_closed S ∀ (F : ultrafilter X), S FX.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 : ultrafilter X) (x : X) :
F 𝓝 xX.str F = x
theorem Compactum.le_nhds_of_str_eq {X : Compactum} (F : ultrafilter X) (x : X) :
X.str F = xF 𝓝 x
@[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.

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.

The functor Compactum_to_CompHaus is essentially surjective.