mathlib documentation

topology.stone_cech

Stone-Čech compactification #

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

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

@[instance]
def ultrafilter_compact {α : Type u} :
@[instance]
def ultrafilter.t2_space {α : Type u} :
theorem ultrafilter_comap_pure_nhds {α : Type u} (b : ultrafilter α) :
theorem dense_range_pure {α : Type u} :

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

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

theorem dense_inducing_pure {α : Type u} :

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

theorem dense_embedding_pure {α : Type u} :

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

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

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

Equations
theorem ultrafilter_extend_extends {α : Type u} {γ : Type u_1} [topological_space γ] [t2_space γ] (f : α → γ) :
theorem continuous_ultrafilter_extend {α : Type u} {γ : Type u_1} [topological_space γ] [t2_space γ] [compact_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 b.map f in γ.

@[instance]
def stone_cech_setoid (α : Type u) [topological_space α] :
Equations
def stone_cech (α : Type u) [topological_space α] :
Type u

The Stone-Čech compactification of a topological space.

Equations
@[instance]
Equations
@[instance]
Equations
def stone_cech_unit {α : Type u} [topological_space α] (x : α) :

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

Equations

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

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

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

Equations
theorem stone_cech_extend_extends {α : Type u} [topological_space α] {γ : Type u} [topological_space γ] [t2_space γ] [compact_space γ] {f : α → γ} (hf : continuous f) :
theorem continuous_stone_cech_extend {α : Type u} [topological_space α] {γ : Type u} [topological_space γ] [t2_space γ] [compact_space γ] {f : α → γ} (hf : continuous f) :
theorem convergent_eqv_pure {α : Type u} [topological_space α] {u : ultrafilter α} {x : α} (ux : u 𝓝 x) :
u pure x
@[instance]
def stone_cech.t2_space {α : Type u} [topological_space α] :
@[instance]