# Stone-Čech compactification #

Construction of the Stone-Čech compactification using ultrafilters.

For any topological space α, we build a compact Hausdorff space StoneCech α and a continuous map stoneCechUnit : α → StoneCech α which is minimal in the sense of the following universal property: for any compact Hausdorff space β and every map f : α → β such that hf : Continuous f : Continuous f Continuous f, there is a unique map stoneCechExtend hf : StoneCech α → β such that stoneCechExtend_extends : stoneCechExtend hf ∘ stoneCechUnit = f. Continuity of this extension is asserted by continuous_stoneCechExtend and uniqueness by stoneCech_hom_ext.

Beware that the terminology “extend” is slightly misleading since stoneCechUnit is not always injective, so one cannot always think of α as being “inside” its compactification StoneCech α.

## Implementation notes #

Parts of the formalization are based on “Ultrafilters and Topology” by Marius Stekelenburg, particularly section 5. However the construction in the general case is different because the equivalence relation on spaces of ultrafilters described by Stekelenburg causes issues with universes since it involves a condition on all compact Hausdorff spaces. We replace it by a two steps construction. The first step called PreStoneCech guarantees the expected universal property but not the Hausdorff condition. We then define StoneCech α as t2Quotient (PreStoneCech α).

def ultrafilterBasis (α : Type u) :
Set (Set ())

Basis for the topology on Ultrafilter α.

Equations
Instances For
Equations
• Ultrafilter.topologicalSpace =
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} :
Equations
• =
instance Ultrafilter.t2Space {α : Type u} :
Equations
• =
Equations
• =
@[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.

Equations
• = .extend f
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 γ.

def PreStoneCech (α : Type u) [] :

Auxilliary construction towards the Stone-Čech compactification of a topological space. It should not be used after the Stone-Čech compactification is constructed.

Equations
Instances For
instance instTopologicalSpacePreStoneCech {α : Type u} [] :
Equations
instance instCompactSpacePreStoneCech {α : Type u} [] :
Equations
• =
instance instInhabitedPreStoneCech {α : Type u} [] [] :
Equations
def preStoneCechUnit {α : Type u} [] (x : α) :

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

Equations
Instances For
theorem continuous_preStoneCechUnit {α : Type u} [] :
Continuous preStoneCechUnit
theorem denseRange_preStoneCechUnit {α : Type u} [] :
DenseRange preStoneCechUnit
theorem preStoneCechCompat {α : Type u} [] {β : Type v} [] [] [] {g : αβ} (hg : ) {F : } {G : } {x : α} (hF : F nhds x) (hG : G nhds x) :
def preStoneCechExtend {α : Type u} [] {β : Type v} [] [] [] {g : αβ} (hg : ) :
β

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

Equations
Instances For
theorem preStoneCechExtend_extends {α : Type u} [] {β : Type v} [] [] [] {g : αβ} (hg : ) :
preStoneCechUnit = g
theorem eq_if_preStoneCechUnit_eq {α : Type u} [] {β : Type v} [] [] [] {g : αβ} (hg : ) {a : α} {b : α} (h : ) :
g a = g b
theorem continuous_preStoneCechExtend {α : Type u} [] {β : Type v} [] [] [] {g : αβ} (hg : ) :
theorem preStoneCech_hom_ext {α : Type u} [] {β : Type v} [] [] {g₁ : β} {g₂ : β} (h₁ : ) (h₂ : ) (h : g₁ preStoneCechUnit = g₂ preStoneCechUnit) :
g₁ = g₂
def StoneCech (α : Type u) [] :

The Stone-Čech compactification of a topological space.

Equations
Instances For
instance instTopologicalSpaceStoneCech {α : Type u} [] :
Equations
• instTopologicalSpaceStoneCech =
instance instT2SpaceStoneCech {α : Type u} [] :
Equations
• =
instance instCompactSpaceStoneCech {α : Type u} [] :
Equations
• =
instance instInhabitedStoneCech {α : Type u} [] [] :
Equations
def stoneCechUnit {α : Type u} [] (x : α) :

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

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

The image of stoneCechUnit is dense. (But stoneCechUnit need not be an embedding, for example if the original space is not Hausdorff.)

def stoneCechExtend {α : Type u} [] {β : Type v} [] [] [] {g : αβ} (hg : ) :
β

The extension of a continuous function from α to a compact Hausdorff space β to the Stone-Čech compactification of α. This extension implements the universal property of this compactification.

Equations
Instances For
theorem stoneCechExtend_extends {α : Type u} [] {β : Type v} [] [] [] {g : αβ} (hg : ) :
stoneCechUnit = g
theorem continuous_stoneCechExtend {α : Type u} [] {β : Type v} [] [] [] {g : αβ} (hg : ) :
theorem eq_if_stoneCechUnit_eq {α : Type u} [] {β : Type v} [] [] [] {a : α} {b : α} {f : αβ} (hcf : ) (h : ) :
f a = f b
theorem stoneCech_hom_ext {α : Type u} [] {β : Type v} [] [] {g₁ : β} {g₂ : β} (h₁ : ) (h₂ : ) (h : g₁ stoneCechUnit = g₂ stoneCechUnit) :
g₁ = g₂