mathlib3 documentation

topology.stone_cech

Stone-Čech compactification #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Construction of the Stone-Čech compactification using ultrafilters.

Parts of the formalization are based on "Ultrafilters and Topology" by Marius Stekelenburg, particularly section 5.

source
def ultrafilter_basis (α : Type u) :
set (set (ultrafilter α))

Basis for the topology on ultrafilter α.

Equations
source
@[protected, instance]
def ultrafilter.topological_space {α : Type u} :
topological_space (ultrafilter α)
Equations
source
theorem ultrafilter_basis_is_basis {α : Type u} :
topological_space.is_topological_basis (ultrafilter_basis α)
source
theorem ultrafilter_is_open_basic {α : Type u} (s : set α) :
is_open {u : ultrafilter α | s ∈ u}

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

source
theorem ultrafilter_is_closed_basic {α : Type u} (s : set α) :
is_closed {u : ultrafilter α | s ∈ u}

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

source
theorem ultrafilter_converges_iff {α : Type u} {u : ultrafilter (ultrafilter α)} {x : ultrafilter α} :
↑u ≤ nhds x ↔ x = mjoin u

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

source
@[protected, instance]
def ultrafilter_compact {α : Type u} :
compact_space (ultrafilter α)
source
@[protected, instance]
def ultrafilter.t2_space {α : Type u} :
t2_space (ultrafilter α)
source
@[protected, instance]
def ultrafilter.totally_disconnected_space {α : Type u} :
totally_disconnected_space (ultrafilter α)
source
theorem ultrafilter_comap_pure_nhds {α : Type u} (b : ultrafilter α) :
filter.comap has_pure.pure (nhds b) ≤ ↑b
source
theorem ultrafilter_pure_injective {α : Type u} :
function.injective has_pure.pure
source
theorem dense_range_pure {α : Type u} :
dense_range has_pure.pure

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

source
theorem induced_topology_pure {α : Type u} :
topological_space.induced has_pure.pure ultrafilter.topological_space = ⊥

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

source
theorem dense_inducing_pure {α : Type u} :
dense_inducing has_pure.pure

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

source
theorem dense_embedding_pure {α : Type u} :
dense_embedding has_pure.pure

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

source
noncomputable def ultrafilter.extend {α : Type u} {γ : Type u_1} [topological_space γ] (f : α → γ) :
ultrafilter α → γ

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

Equations
source
theorem ultrafilter_extend_extends {α : Type u} {γ : Type u_1} [topological_space γ] [t2_space γ] (f : α → γ) :
ultrafilter.extend f ∘ has_pure.pure = f
source
theorem continuous_ultrafilter_extend {α : Type u} {γ : Type u_1} [topological_space γ] [t2_space γ] [compact_space γ] (f : α → γ) :
continuous (ultrafilter.extend f)
source
theorem ultrafilter_extend_eq_iff {α : Type u} {γ : Type u_1} [topological_space γ] [t2_space γ] [compact_space γ] {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 γ.

source
@[protected, instance]
def stone_cech_setoid (α : Type u) [topological_space α] :
setoid (ultrafilter α)
Equations
source
def stone_cech (α : Type u) [topological_space α] :
Type u

The Stone-Čech compactification of a topological space.

Equations
Instances for stone_cech
source
@[protected, instance]
def stone_cech.topological_space {α : Type u} [topological_space α] :
topological_space (stone_cech α)
Equations
source
@[protected, instance]
def stone_cech.inhabited {α : Type u} [topological_space α] [inhabited α] :
inhabited (stone_cech α)
Equations
source
def stone_cech_unit {α : Type u} [topological_space α] (x : α) :
stone_cech α

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

Equations
source
theorem dense_range_stone_cech_unit {α : Type u} [topological_space α] :
dense_range stone_cech_unit

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

source
noncomputable def stone_cech_extend {α : Type u} [topological_space α] {γ : Type u} [topological_space γ] [t2_space γ] [compact_space γ] {f : α → γ} (hf : continuous f) :
stone_cech α → γ

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

Equations
source
theorem stone_cech_extend_extends {α : Type u} [topological_space α] {γ : Type u} [topological_space γ] [t2_space γ] [compact_space γ] {f : α → γ} (hf : continuous f) :
stone_cech_extend hf ∘ stone_cech_unit = f
source
theorem continuous_stone_cech_extend {α : Type u} [topological_space α] {γ : Type u} [topological_space γ] [t2_space γ] [compact_space γ] {f : α → γ} (hf : continuous f) :
continuous (stone_cech_extend hf)
source
theorem stone_cech_hom_ext {α : Type u} [topological_space α] {γ' : Type u} [topological_space γ'] [t2_space γ'] {g₁ g₂ : stone_cech α → γ'} (h₁ : continuous g₁) (h₂ : continuous g₂) (h : g₁ ∘ stone_cech_unit = g₂ ∘ stone_cech_unit) :
g₁ = g₂
source
theorem convergent_eqv_pure {α : Type u} [topological_space α] {u : ultrafilter α} {x : α} (ux : ↑u ≤ nhds x) :
u ≈ has_pure.pure x
source
theorem continuous_stone_cech_unit {α : Type u} [topological_space α] :
continuous stone_cech_unit
source
@[protected, instance]
def stone_cech.t2_space {α : Type u} [topological_space α] :
t2_space (stone_cech α)
source
@[protected, instance]
def stone_cech.compact_space {α : Type u} [topological_space α] :
compact_space (stone_cech α)