# mathlibdocumentation

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
@[instance]

Equations
theorem ultrafilter_basis_is_basis {α : Type u} :

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

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

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

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

theorem ultrafilter_converges_iff {α : Type u} {u : filter.ultrafilter } {x : filter.ultrafilter α} :
u.val 𝓝 x x =

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 : filter.ultrafilter α) :
(𝓝 b) b.val

theorem ultrafilter_pure_injective {α : Type u} :

theorem dense_range_pure {α : Type u} :

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

theorem induced_topology_pure {α : Type u} :

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}  :
(α → γ) → γ

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

Equations
• = let _inst : := in
theorem ultrafilter_extend_extends {α : Type u} {γ : Type u_1} [t2_space γ] (f : α → γ) :

theorem continuous_ultrafilter_extend {α : Type u} {γ : Type u_1} [t2_space γ] (f : α → γ) :

theorem ultrafilter_extend_eq_iff {α : Type u} {γ : Type u_1} [t2_space γ] {f : α → γ} {b : filter.ultrafilter α} {c : γ} :
= c b.val 𝓝 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)  :

Equations
• = {r := λ (x y : , ∀ (γ : Type u) [_inst_2 : [_inst_3 : t2_space γ] [_inst_4 : (f : α → γ), , iseqv := _}
def stone_cech (α : Type u)  :
Type u

The Stone-Čech compactification of a topological space.

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

Equations
@[instance]
def stone_cech.inhabited {α : Type u} [inhabited α] :

Equations
def stone_cech_unit {α : Type u}  :
α →

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

Equations
theorem dense_range_stone_cech_unit {α : Type u}  :

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} {γ : Type u} [t2_space γ] {f : α → γ} :
→ γ

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} {γ : Type u} [t2_space γ] {f : α → γ} (hf : continuous f) :

theorem continuous_stone_cech_extend {α : Type u} {γ : Type u} [t2_space γ] {f : α → γ} (hf : continuous f) :

theorem convergent_eqv_pure {α : Type u} {u : filter.ultrafilter α} {x : α} :
u.val 𝓝 xu pure x

theorem continuous_stone_cech_unit {α : Type u}  :

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

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