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

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

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

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

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

@[instance]

@[instance]

theorem dense_range_pure {α : Type u} :

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

The map pure : α → ultra_filter α induces on a 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 γ] :
(α → γ)filter.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 : filter.ultrafilter α} {c : γ} :

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

@[instance]

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 α] :
α → stone_cech α

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 : α → γ} :
continuous fstone_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 : filter.ultrafilter α} {x : α} :
u.val 𝓝 xu pure x

@[instance]
def stone_cech.t2_space {α : Type u} [topological_space α] :

@[instance]