# 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.
Basis for the topology on ultrafilter α.
Equations
- ultrafilter_basis α = {t : set (filter.ultrafilter α) | ∃ (s : set α), t = {u : filter.ultrafilter α | s ∈ u.val}}
The basic open sets for the topology on ultrafilters are open.
The basic open sets for the topology on ultrafilters are also closed.
Every ultrafilter u on ultrafilter α converges to a unique
point of ultrafilter α, namely mjoin u.
Equations
Equations
pure : α → ultrafilter α defines a dense inducing of α in ultrafilter α.
pure : α → ultrafilter α defines a dense embedding of α in ultrafilter α.
The extension of a function α → γ to a function ultrafilter α → γ.
When γ is a compact Hausdorff space it will be continuous.
Equations
- ultrafilter.extend f = let _inst : topological_space α := ⊥ in dense_inducing_pure.extend f
The value of ultrafilter.extend f on an ultrafilter b is the
unique limit of the ultrafilter b.map f in γ.
Equations
- stone_cech_setoid α = {r := λ (x y : filter.ultrafilter α), ∀ (γ : Type u) [_inst_2 : topological_space γ] [_inst_3 : t2_space γ] [_inst_4 : compact_space γ] (f : α → γ), continuous f → ultrafilter.extend f x = ultrafilter.extend f y, iseqv := _}
The Stone-Čech compactification of a topological space.
Equations
- stone_cech α = quotient (stone_cech_setoid α)
Equations
- stone_cech.topological_space = stone_cech.topological_space._proof_1.mpr quotient.topological_space
Equations
- stone_cech.inhabited = stone_cech.inhabited._proof_1.mpr quotient.inhabited
The natural map from α to its Stone-Čech compactification.
Equations
The image of stone_cech_unit is dense. (But stone_cech_unit need not be an embedding, for example if α is not Hausdorff.)
The extension of a continuous function from α to a compact Hausdorff space γ to the Stone-Čech compactification of α.