# mathlibdocumentation

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

• Compactum is the type of compacta, which we define as algebras for the ultrafilter monad.
• Compactum_to_CompHaus is the functor Compactum ⥤ CompHaus. Here CompHaus is the usual category of compact Hausdorff spaces.
• Compactum_to_CompHaus.is_equivalence is a term of type is_equivalence Compactum_to_CompHaus.

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:

• topological_space X.
• compact_space X.
• t2_space 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.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:

• forget : Compactum ⥤ Type* is the forgetful functor, which induces a concrete_category 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 #

@[instance]
def Compactum  :
Type (u_1+1)

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

Equations
@[instance]
@[instance]
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 adjunction between free and forget.

Equations
@[instance]
Equations
@[instance]
Equations
def Compactum.str (X : Compactum) :
X

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

Equations
def Compactum.join (X : Compactum) :

Equations
def Compactum.incl (X : Compactum) :
X →

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

This definition is used to prove essential surjectivity of Compactum_to_CompHaus.

Equations

The functor Compactum_to_CompHaus is essentially surjective.

The functor Compactum_to_CompHaus is an equivalence of categories.

Equations