# Documentation

Mathlib.Topology.StoneCech

# 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 ultrafilterBasis (α : Type u) :
Set (Set ())

Basis for the topology on Ultrafilter α.

Instances For
theorem ultrafilter_isOpen_basic {α : Type u} (s : Set α) :
IsOpen {u | s u}

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

theorem ultrafilter_isClosed_basic {α : Type u} (s : Set α) :
IsClosed {u | s u}

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

theorem ultrafilter_converges_iff {α : Type u} {u : } {x : } :
u nhds x x =

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

instance ultrafilter_compact {α : Type u} :
instance Ultrafilter.t2Space {α : Type u} :
@[simp]
theorem Ultrafilter.tendsto_pure_self {α : Type u} (b : ) :
Filter.Tendsto pure (b) (nhds b)
theorem ultrafilter_comap_pure_nhds {α : Type u} (b : ) :
Filter.comap pure (nhds b) b
theorem denseRange_pure {α : Type u} :

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

theorem induced_topology_pure {α : Type u} :
TopologicalSpace.induced pure Ultrafilter.topologicalSpace =

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

theorem denseInducing_pure {α : Type u} :

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

theorem denseEmbedding_pure {α : Type u} :

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

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

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

Instances For
theorem ultrafilter_extend_extends {α : Type u} {γ : Type u_1} [] [] (f : αγ) :
pure = f
theorem continuous_ultrafilter_extend {α : Type u} {γ : Type u_1} [] [] [] (f : αγ) :
theorem ultrafilter_extend_eq_iff {α : Type u} {γ : Type u_1} [] [] [] {f : αγ} {b : } {c : γ} :
= c ↑() nhds c

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

instance stoneCechSetoid (α : Type u) [] :
def StoneCech (α : Type u) [] :

The Stone-Čech compactification of a topological space.

Instances For
instance instInhabitedStoneCech {α : Type u} [] [] :
def stoneCechUnit {α : Type u} [] (x : α) :

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

Instances For
theorem denseRange_stoneCechUnit {α : Type u} [] :
DenseRange stoneCechUnit

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

def stoneCechExtend {α : Type u} [] {γ : Type u} [] [] [] {f : αγ} (hf : ) :
γ

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

Instances For
theorem stoneCechExtend_extends {α : Type u} [] {γ : Type u} [] [] [] {f : αγ} (hf : ) :
stoneCechUnit = f
theorem continuous_stoneCechExtend {α : Type u} [] {γ : Type u} [] [] [] {f : αγ} (hf : ) :
theorem stoneCech_hom_ext {α : Type u} [] {γ' : Type u} [] [T2Space γ'] {g₁ : γ'} {g₂ : γ'} (h₁ : ) (h₂ : ) (h : g₁ stoneCechUnit = g₂ stoneCechUnit) :
g₁ = g₂
theorem convergent_eqv_pure {α : Type u} [] {u : } {x : α} (ux : u nhds x) :
u pure x
theorem continuous_stoneCechUnit {α : Type u} [] :
Continuous stoneCechUnit
instance StoneCech.t2Space {α : Type u} [] :
instance StoneCech.compactSpace {α : Type u} [] :