mathlib3 documentation

topology.category.Compactum

Compacta and Compact Hausdorff Spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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 #

E. Manes, Algebraic Theories, Graduate Texts in Mathematics 26, Springer-Verlag, 1976.
https://ncatlab.org/nlab/show/ultrafilter

@[protected, instance]

def Compactum.category :

category_theory.category Compactum

def Compactum :

Type (u_1+1)

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

Equations

Compactum = (category_theory.of_type_monad ultrafilter).algebra

Instances for Compactum

@[protected, instance]

def Compactum.inhabited :

inhabited Compactum

@[protected, instance]

def Compactum.forget.faithful :

category_theory.faithful Compactum.forget

def Compactum.forget :

Compactum ⥤ Type u_1

The forgetful functor to Type*

Equations

Compactum.forget = (category_theory.of_type_monad ultrafilter).forget

Instances for Compactum.forget

@[protected, instance]

noncomputable def Compactum.forget.creates_limits :

category_theory.creates_limits Compactum.forget

def Compactum.free :

Type u_1 ⥤ Compactum

The "free" Compactum functor.

Equations

Compactum.free = (category_theory.of_type_monad ultrafilter).free

def Compactum.adj :

Compactum.free ⊣ Compactum.forget

The adjunction between free and forget.

Equations

Compactum.adj = (category_theory.of_type_monad ultrafilter).adj

@[protected, instance]

def Compactum.category_theory.concrete_category :

category_theory.concrete_category Compactum

Equations

Compactum.category_theory.concrete_category = category_theory.concrete_category.mk Compactum.forget

@[protected, instance]

def Compactum.has_coe_to_sort :

has_coe_to_sort Compactum (Type u_1)

Equations

Compactum.has_coe_to_sort = {coe := Compactum.forget.obj}

@[protected, instance]

def Compactum.quiver.hom.has_coe_to_fun {X Y : Compactum} :

has_coe_to_fun (X ⟶ Y) (λ (f : X ⟶ Y), ↥X → ↥Y)

Equations

Compactum.quiver.hom.has_coe_to_fun = {coe := λ (f : X ⟶ Y), f.f}

@[protected, instance]

def Compactum.category_theory.limits.has_limits :

category_theory.limits.has_limits Compactum

def Compactum.str (X : Compactum) :

ultrafilter ↥X → ↥X

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

Equations

X.str = X.a

def Compactum.join (X : Compactum) :

ultrafilter (ultrafilter ↥X) → ultrafilter ↥X

The monadic join.

Equations

X.join = (category_theory.of_type_monad ultrafilter).μ.app ↥X

def Compactum.incl (X : Compactum) :

↥X → ultrafilter ↥X

The inclusion of X into ultrafilter X.

Equations

X.incl = (category_theory.of_type_monad ultrafilter).η.app (Compactum.forget.obj X)

@[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)

@[protected, instance]

def Compactum.topological_space {X : Compactum} :

topological_space ↥X

Equations

Compactum.topological_space = {is_open := λ (U : set ↥X), ∀ (F : ultrafilter ↥X), X.str F ∈ U → U ∈ F, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}

theorem Compactum.is_closed_iff {X : Compactum} (S : set ↥X) :

is_closed S ↔ ∀ (F : ultrafilter ↥X), S ∈ F → X.str F ∈ S

@[protected, instance]

def Compactum.compact_space {X : Compactum} :

compact_space ↥X

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 x → X.str F = x

theorem Compactum.le_nhds_of_str_eq {X : Compactum} (F : ultrafilter ↥X) (x : ↥X) :

X.str F = x → ↑F ≤ nhds x

@[protected, instance]

def Compactum.t2_space {X : Compactum} :

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) :

continuous ⇑f

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.

Equations

Compactum.of_topological_space X = {A := X, a := ultrafilter.Lim _inst_1, unit' := _, assoc' := _}

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

Compactum.hom_of_continuous f cont = {f := f, h' := _}

def Compactum_to_CompHaus :

Compactum ⥤ CompHaus

The functor functor from Compactum to CompHaus.

Equations

Compactum_to_CompHaus = {obj := λ (X : Compactum), CompHaus.mk {α := ↥X, str := Compactum.topological_space X}, map := λ (X Y : Compactum) (f : X ⟶ Y), {to_fun := ⇑f, continuous_to_fun := _}, map_id' := Compactum_to_CompHaus._proof_1, map_comp' := Compactum_to_CompHaus._proof_2}

Instances for Compactum_to_CompHaus

Compactum_to_CompHaus.is_equivalence

def Compactum_to_CompHaus.full :

category_theory.full Compactum_to_CompHaus

The functor Compactum_to_CompHaus is full.

Equations

Compactum_to_CompHaus.full = {preimage := λ (X Y : Compactum) (f : Compactum_to_CompHaus.obj X ⟶ Compactum_to_CompHaus.obj Y), Compactum.hom_of_continuous f.to_fun _, witness' := Compactum_to_CompHaus.full._proof_2}

theorem Compactum_to_CompHaus.faithful :

category_theory.faithful Compactum_to_CompHaus

The functor Compactum_to_CompHaus is faithful.

def Compactum_to_CompHaus.iso_of_topological_space {D : CompHaus} :

Compactum_to_CompHaus.obj (Compactum.of_topological_space ↥D) ≅ D

This definition is used to prove essential surjectivity of Compactum_to_CompHaus.

Equations

Compactum_to_CompHaus.iso_of_topological_space = {hom := {to_fun := id ↥((Compactum_to_CompHaus.obj (Compactum.of_topological_space ↥D)).to_Top), continuous_to_fun := _}, inv := {to_fun := id ↥(D.to_Top), continuous_to_fun := _}, hom_inv_id' := _, inv_hom_id' := _}

theorem Compactum_to_CompHaus.ess_surj :

category_theory.ess_surj Compactum_to_CompHaus

The functor Compactum_to_CompHaus is essentially surjective.

@[protected, instance]

noncomputable def Compactum_to_CompHaus.is_equivalence :

category_theory.is_equivalence Compactum_to_CompHaus

The functor Compactum_to_CompHaus is an equivalence of categories.

Equations

Compactum_to_CompHaus.is_equivalence = category_theory.equivalence.of_fully_faithfully_ess_surj Compactum_to_CompHaus

def Compactum_to_CompHaus_comp_forget :

Compactum_to_CompHaus ⋙ category_theory.forget CompHaus ≅ Compactum.forget

The forgetful functors of Compactum and CompHaus are compatible via Compactum_to_CompHaus.

Equations

Compactum_to_CompHaus_comp_forget = category_theory.nat_iso.of_components (λ (X : Compactum), category_theory.eq_to_iso _) Compactum_to_CompHaus_comp_forget._proof_2

@[protected, instance]

noncomputable def Profinite.forget_creates_limits :

category_theory.creates_limits (category_theory.forget Profinite)

Equations

Profinite.forget_creates_limits = id (category_theory.comp_creates_limits Profinite_to_CompHaus (category_theory.forget CompHaus))