mathlib documentation


Stone-Čech compactification #

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

Construction of the Stone-Čech compactification using ultrafilters.

Parts of the formalization are based on "Ultrafilters and Topology" by Marius Stekelenburg, particularly section 5.

def ultrafilter_basis (α : Type u) :

Basis for the topology on ultrafilter α.

theorem ultrafilter_is_open_basic {α : Type u} (s : set α) :
is_open {u : ultrafilter α | s u}

The basic open sets for the topology on ultrafilters are open.

theorem ultrafilter_is_closed_basic {α : Type u} (s : set α) :
is_closed {u : ultrafilter α | s u}

The basic open sets for the topology on ultrafilters are also closed.

theorem ultrafilter_converges_iff {α : Type u} {u : ultrafilter (ultrafilter α)} {x : ultrafilter α} :

Every ultrafilter u on ultrafilter α converges to a unique point of ultrafilter α, namely mjoin u.

@[protected, instance]
@[protected, instance]

The range of pure : α → ultrafilter α is dense in ultrafilter α.

The map pure : α → ultra_filter α induces on α the discrete topology.

pure : α → ultrafilter α defines a dense inducing of α in ultrafilter α.

pure : α → ultrafilter α defines a dense embedding of α in ultrafilter α.

noncomputable def ultrafilter.extend {α : Type u} {γ : Type u_1} [topological_space γ] (f : α γ) :

The extension of a function α → γ to a function ultrafilter α → γ. When γ is a compact Hausdorff space it will be continuous.

theorem ultrafilter_extend_extends {α : Type u} {γ : Type u_1} [topological_space γ] [t2_space γ] (f : α γ) :
theorem ultrafilter_extend_eq_iff {α : Type u} {γ : Type u_1} [topological_space γ] [t2_space γ] [compact_space γ] {f : α γ} {b : ultrafilter α} {c : γ} :

The value of ultrafilter.extend f on an ultrafilter b is the unique limit of the ultrafilter f in γ.

@[protected, instance]
def stone_cech (α : Type u) [topological_space α] :

The Stone-Čech compactification of a topological space.

Instances for stone_cech
@[protected, instance]
@[protected, instance]
def stone_cech_unit {α : Type u} [topological_space α] (x : α) :

The natural map from α to its Stone-Čech compactification.


The image of stone_cech_unit is dense. (But stone_cech_unit need not be an embedding, for example if α is not Hausdorff.)

noncomputable def stone_cech_extend {α : Type u} [topological_space α] {γ : Type u} [topological_space γ] [t2_space γ] [compact_space γ] {f : α γ} (hf : continuous f) :

The extension of a continuous function from α to a compact Hausdorff space γ to the Stone-Čech compactification of α.

theorem stone_cech_hom_ext {α : Type u} [topological_space α] {γ' : Type u} [topological_space γ'] [t2_space γ'] {g₁ g₂ : stone_cech α γ'} (h₁ : continuous g₁) (h₂ : continuous g₂) (h : g₁ stone_cech_unit = g₂ stone_cech_unit) :
g₁ = g₂
theorem convergent_eqv_pure {α : Type u} [topological_space α] {u : ultrafilter α} {x : α} (ux : u nhds x) :
@[protected, instance]
@[protected, instance]