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, 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 (Ultrafilter α))

Basis for the topology on Ultrafilter α.

Equations

• ultrafilterBasis α = Set.range fun (s : Set α) => {u : Ultrafilter α | s ∈ u}

instance Ultrafilter.topologicalSpace {α : Type u} : TopologicalSpace (Ultrafilter α)

Equations

• Ultrafilter.topologicalSpace = TopologicalSpace.generateFrom (ultrafilterBasis α)

theorem ultrafilterBasis_is_basis {α : Type u} : TopologicalSpace.IsTopologicalBasis (ultrafilterBasis α)

theorem ultrafilter_isOpen_basic {α : Type u} (s : Set α) : IsOpen {u : Ultrafilter α | s ∈ u}

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

theorem ultrafilter_isClosed_basic {α : Type u} (s : Set α) : IsClosed {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 α} : ↑u ≤ nhds x ↔ x = joinM u

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

instance ultrafilter_compact {α : Type u} : CompactSpace (Ultrafilter α)

instance Ultrafilter.t2Space {α : Type u} : T2Space (Ultrafilter α)

instance instTotallyDisconnectedSpaceUltrafilter {α : Type u} : TotallyDisconnectedSpace (Ultrafilter α)

@[simp]

theorem Ultrafilter.tendsto_pure_self {α : Type u} (b : Ultrafilter α) : Filter.Tendsto pure (↑b) (nhds b)

theorem ultrafilter_comap_pure_nhds {α : Type u} (b : Ultrafilter α) : Filter.comap pure (nhds b) ≤ ↑b

@[deprecated Ultrafilter.pure_injective (since := "2025-08-14")]

theorem ultrafilter_pure_injective {α : Type u} : Function.Injective pure

Alias of Ultrafilter.pure_injective.

theorem denseRange_pure {α : Type u} : DenseRange pure

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 isDenseInducing_pure {α : Type u} : IsDenseInducing pure

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

theorem isDenseEmbedding_pure {α : Type u} : IsDenseEmbedding pure

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

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

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

Equations

• Ultrafilter.extend f = ⋯.extend f

@[simp]

theorem ultrafilter_extend_extends {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] (f : α → γ) : Ultrafilter.extend f ∘ pure = f

@[simp]

theorem ultrafilter_extend_pure {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] (f : α → γ) (a : α) : Ultrafilter.extend f (pure a) = f a

theorem continuous_ultrafilter_extend {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] (f : α → γ) : Continuous (Ultrafilter.extend f)

theorem ultrafilter_extend_eq_iff {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] {f : α → γ} {b : Ultrafilter α} {c : γ} : Ultrafilter.extend f b = c ↔ ↑(Ultrafilter.map f b) ≤ 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) [TopologicalSpace α] : Type u

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

Equations

• PreStoneCech α = Quot fun (F G : Ultrafilter α) => ∃ (x : α), ↑F ≤ nhds x ∧ ↑G ≤ nhds x

instance instTopologicalSpacePreStoneCech {α : Type u} [TopologicalSpace α] : TopologicalSpace (PreStoneCech α)

Equations

• instTopologicalSpacePreStoneCech = inferInstanceAs (TopologicalSpace (Quot fun (F G : Ultrafilter α) => ∃ (x : α), ↑F ≤ nhds x ∧ ↑G ≤ nhds x))

instance instCompactSpacePreStoneCech {α : Type u} [TopologicalSpace α] : CompactSpace (PreStoneCech α)

instance instInhabitedPreStoneCech {α : Type u} [TopologicalSpace α] [Inhabited α] : Inhabited (PreStoneCech α)

Equations

• instInhabitedPreStoneCech = inferInstanceAs (Inhabited (Quot fun (F G : Ultrafilter α) => ∃ (x : α), ↑F ≤ nhds x ∧ ↑G ≤ nhds x))

def preStoneCechUnit {α : Type u} [TopologicalSpace α] (x : α) : PreStoneCech α

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

Equations

• preStoneCechUnit x = Quot.mk (fun (F G : Ultrafilter α) => ∃ (x : α), ↑F ≤ nhds x ∧ ↑G ≤ nhds x) (pure x)

theorem continuous_preStoneCechUnit {α : Type u} [TopologicalSpace α] : Continuous preStoneCechUnit

theorem denseRange_preStoneCechUnit {α : Type u} [TopologicalSpace α] : DenseRange preStoneCechUnit

theorem preStoneCech_hom_ext {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g₁ g₂ : PreStoneCech α → β} (h₁ : Continuous g₁) (h₂ : Continuous g₂) (h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit) : g₁ = g₂

theorem preStoneCechCompat {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) {F G : Ultrafilter α} {x : α} (hF : ↑F ≤ nhds x) (hG : ↑G ≤ nhds x) : Ultrafilter.extend g F = Ultrafilter.extend g G

def preStoneCechExtend {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) : PreStoneCech α → β

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

Equations

• preStoneCechExtend hg = Quot.lift (Ultrafilter.extend g) ⋯

@[simp]

theorem preStoneCechExtend_extends {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) : preStoneCechExtend hg ∘ preStoneCechUnit = g

@[simp]

theorem preStoneCechExtend_preStoneCechUnit {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) (a : α) : preStoneCechExtend hg (preStoneCechUnit a) = g a

theorem eq_if_preStoneCechUnit_eq {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) {a b : α} (h : preStoneCechUnit a = preStoneCechUnit b) : g a = g b

theorem continuous_preStoneCechExtend {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) : Continuous (preStoneCechExtend hg)

def StoneCech (α : Type u) [TopologicalSpace α] : Type u

The Stone-Čech compactification of a topological space.

Equations

• StoneCech α = T2Quotient (PreStoneCech α)

instance instTopologicalSpaceStoneCech {α : Type u} [TopologicalSpace α] : TopologicalSpace (StoneCech α)

Equations

• instTopologicalSpaceStoneCech = inferInstanceAs (TopologicalSpace (T2Quotient (PreStoneCech α)))

instance instT2SpaceStoneCech {α : Type u} [TopologicalSpace α] : T2Space (StoneCech α)

instance instCompactSpaceStoneCech {α : Type u} [TopologicalSpace α] : CompactSpace (StoneCech α)

instance instInhabitedStoneCech {α : Type u} [TopologicalSpace α] [Inhabited α] : Inhabited (StoneCech α)

Equations

• instInhabitedStoneCech = inferInstanceAs (Inhabited (Quotient (t2Setoid (PreStoneCech α))))

def stoneCechUnit {α : Type u} [TopologicalSpace α] (x : α) : StoneCech α

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

Equations

• stoneCechUnit x = T2Quotient.mk (preStoneCechUnit x)

theorem continuous_stoneCechUnit {α : Type u} [TopologicalSpace α] : Continuous stoneCechUnit

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

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

theorem stoneCech_hom_ext {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g₁ g₂ : StoneCech α → β} (h₁ : Continuous g₁) (h₂ : Continuous g₂) (h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit) : g₁ = g₂

def stoneCechExtend {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g : α → β} (hg : Continuous g) [CompactSpace β] : StoneCech α → β

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

• stoneCechExtend hg = T2Quotient.lift ⋯

@[simp]

theorem stoneCechExtend_extends {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g : α → β} (hg : Continuous g) [CompactSpace β] : stoneCechExtend hg ∘ stoneCechUnit = g

@[simp]

theorem stoneCechExtend_stoneCechUnit {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g : α → β} (hg : Continuous g) [CompactSpace β] (a : α) : stoneCechExtend hg (stoneCechUnit a) = g a

theorem continuous_stoneCechExtend {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] {g : α → β} (hg : Continuous g) [CompactSpace β] : Continuous (stoneCechExtend hg)

theorem eq_if_stoneCechUnit_eq {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {a b : α} {f : α → β} (hcf : Continuous f) (h : stoneCechUnit a = stoneCechUnit b) : f a = f b