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

Basis for the topology on Ultrafilter α.

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

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

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 : 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 instTotallyDisconnectedSpaceUltrafilterTopologicalSpace {α : 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

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

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 denseInducing_pure {α : Type u} : DenseInducing pure

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

theorem denseEmbedding_pure {α : Type u} : DenseEmbedding 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.

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

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 γ.

instance stoneCechSetoid (α : Type u) [TopologicalSpace α] : Setoid (Ultrafilter α)

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

The Stone-Čech compactification of a topological space.

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

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

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

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

theorem denseRange_stoneCechUnit {α : Type u} [TopologicalSpace α] : 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} [TopologicalSpace α] {γ : Type u} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] {f : α → γ} (hf : Continuous f) : StoneCech α → γ

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

theorem stoneCechExtend_extends {α : Type u} [TopologicalSpace α] {γ : Type u} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] {f : α → γ} (hf : Continuous f) : stoneCechExtend hf ∘ stoneCechUnit = f

theorem continuous_stoneCechExtend {α : Type u} [TopologicalSpace α] {γ : Type u} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] {f : α → γ} (hf : Continuous f) : Continuous (stoneCechExtend hf)

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

theorem convergent_eqv_pure {α : Type u} [TopologicalSpace α] {u : Ultrafilter α} {x : α} (ux : ↑u ≤ nhds x) : u ≈ pure x

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

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

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