mathlib3 documentation

topology.alexandroff

The Alexandroff Compactification #

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

We construct the Alexandroff compactification (the one-point compactification) of an arbitrary topological space X and prove some properties inherited from X.

Main definitions #

alexandroff: the Alexandroff compactification, we use coercion for the canonical embedding X → alexandroff X; when X is already compact, the compactification adds an isolated point to the space.
alexandroff.infty: the extra point

Main results #

The topological structure of alexandroff X
The connectedness of alexandroff X for a noncompact, preconnected X
alexandroff X is T₀ for a T₀ space X
alexandroff X is T₁ for a T₁ space X
alexandroff X is normal if X is a locally compact Hausdorff space

Tags #

one-point compactification, compactness

Definition and basic properties #

In this section we define alexandroff X to be the disjoint union of X and ∞, implemented as option X. Then we restate some lemmas about option X for alexandroff X.

def alexandroff (X : Type u_1) :

Type u_1

The Alexandroff extension of an arbitrary topological space X

Equations

alexandroff X = option X

Instances for alexandroff

@[protected, instance]

def alexandroff.has_repr {X : Type u_1} [has_repr X] :

has_repr (alexandroff X)

The repr uses the notation from the alexandroff locale.

Equations

alexandroff.has_repr = {repr := λ (o : alexandroff X), alexandroff.has_repr._match_1 o}
alexandroff.has_repr._match_1 (option.some a) = "↑" ++ repr a
alexandroff.has_repr._match_1 option.none = "∞"

def alexandroff.infty {X : Type u_1} :

The point at infinity

Equations

alexandroff.infty = option.none

@[protected, instance]

def alexandroff.has_coe_t {X : Type u_1} :

has_coe_t X (alexandroff X)

Equations

alexandroff.has_coe_t = {coe := option.some X}

@[protected, instance]

def alexandroff.inhabited {X : Type u_1} :

inhabited (alexandroff X)

Equations

alexandroff.inhabited = {default := alexandroff.infty X}

@[protected, instance]

def alexandroff.fintype {X : Type u_1} [fintype X] :

fintype (alexandroff X)

Equations

alexandroff.fintype = option.fintype

@[protected, instance]

def alexandroff.infinite {X : Type u_1} [infinite X] :

infinite (alexandroff X)

theorem alexandroff.coe_injective {X : Type u_1} :

function.injective coe

@[norm_cast]

theorem alexandroff.coe_eq_coe {X : Type u_1} {x y : X} :

↑x = ↑y ↔ x = y

@[simp]

theorem alexandroff.coe_ne_infty {X : Type u_1} (x : X) :

↑x ≠ alexandroff.infty

@[simp]

theorem alexandroff.infty_ne_coe {X : Type u_1} (x : X) :

alexandroff.infty ≠ ↑x

@[protected]

def alexandroff.rec {X : Type u_1} (C : alexandroff X → Sort u_2) (h₁ : C alexandroff.infty) (h₂ : Π (x : X), C ↑x) (z : alexandroff X) :

C z

Recursor for alexandroff using the preferred forms ∞ and ↑x.

Equations

alexandroff.rec C h₁ h₂ = option.rec h₁ h₂

theorem alexandroff.is_compl_range_coe_infty {X : Type u_1} :

is_compl (set.range coe) {alexandroff.infty}

@[simp]

theorem alexandroff.range_coe_union_infty {X : Type u_1} :

set.range coe ∪ {alexandroff.infty} = set.univ

@[simp]

theorem alexandroff.range_coe_inter_infty {X : Type u_1} :

set.range coe ∩ {alexandroff.infty} = ∅

@[simp]

theorem alexandroff.compl_range_coe {X : Type u_1} :

(set.range coe)ᶜ = {alexandroff.infty}

theorem alexandroff.compl_infty {X : Type u_1} :

{alexandroff.infty}ᶜ = set.range coe

theorem alexandroff.compl_image_coe {X : Type u_1} (s : set X) :

(coe '' s)ᶜ = coe '' sᶜ ∪ {alexandroff.infty}

theorem alexandroff.ne_infty_iff_exists {X : Type u_1} {x : alexandroff X} :

x ≠ alexandroff.infty ↔ ∃ (y : X), ↑y = x

@[protected, instance]

def alexandroff.can_lift {X : Type u_1} :

can_lift (alexandroff X) X coe (λ (x : alexandroff X), x ≠ alexandroff.infty)

Equations

alexandroff.can_lift = with_top.can_lift

theorem alexandroff.not_mem_range_coe_iff {X : Type u_1} {x : alexandroff X} :

x ∉ set.range coe ↔ x = alexandroff.infty

theorem alexandroff.infty_not_mem_range_coe {X : Type u_1} :

alexandroff.infty ∉ set.range coe

theorem alexandroff.infty_not_mem_image_coe {X : Type u_1} {s : set X} :

alexandroff.infty ∉ coe '' s

@[simp]

theorem alexandroff.coe_preimage_infty {X : Type u_1} :

coe ⁻¹' {alexandroff.infty} = ∅

Topological space structure on `alexandroff X` #

We define a topological space structure on alexandroff X so that s is open if and only if

coe ⁻¹' s is open in X;
if ∞ ∈ s, then (coe ⁻¹' s)ᶜ is compact.

Then we reformulate this definition in a few different ways, and prove that coe : X → alexandroff X is an open embedding. If X is not a compact space, then we also prove that coe has dense range, so it is a dense embedding.

@[protected, instance]

def alexandroff.topological_space {X : Type u_1} [topological_space X] :

topological_space (alexandroff X)

Equations

alexandroff.topological_space = {is_open := λ (s : set (alexandroff X)), (alexandroff.infty ∈ s → is_compact (coe ⁻¹' s)ᶜ) ∧ is_open (coe ⁻¹' s), is_open_univ := _, is_open_inter := _, is_open_sUnion := _}

theorem alexandroff.is_open_def {X : Type u_1} [topological_space X] {s : set (alexandroff X)} :

is_open s ↔ (alexandroff.infty ∈ s → is_compact (coe ⁻¹' s)ᶜ) ∧ is_open (coe ⁻¹' s)

theorem alexandroff.is_open_iff_of_mem' {X : Type u_1} [topological_space X] {s : set (alexandroff X)} (h : alexandroff.infty ∈ s) :

is_open s ↔ is_compact (coe ⁻¹' s)ᶜ ∧ is_open (coe ⁻¹' s)

theorem alexandroff.is_open_iff_of_mem {X : Type u_1} [topological_space X] {s : set (alexandroff X)} (h : alexandroff.infty ∈ s) :

is_open s ↔ is_closed (coe ⁻¹' s)ᶜ ∧ is_compact (coe ⁻¹' s)ᶜ

theorem alexandroff.is_open_iff_of_not_mem {X : Type u_1} [topological_space X] {s : set (alexandroff X)} (h : alexandroff.infty ∉ s) :

is_open s ↔ is_open (coe ⁻¹' s)

theorem alexandroff.is_closed_iff_of_mem {X : Type u_1} [topological_space X] {s : set (alexandroff X)} (h : alexandroff.infty ∈ s) :

is_closed s ↔ is_closed (coe ⁻¹' s)

theorem alexandroff.is_closed_iff_of_not_mem {X : Type u_1} [topological_space X] {s : set (alexandroff X)} (h : alexandroff.infty ∉ s) :

is_closed s ↔ is_closed (coe ⁻¹' s) ∧ is_compact (coe ⁻¹' s)

@[simp]

theorem alexandroff.is_open_image_coe {X : Type u_1} [topological_space X] {s : set X} :

is_open (coe '' s) ↔ is_open s

theorem alexandroff.is_open_compl_image_coe {X : Type u_1} [topological_space X] {s : set X} :

is_open (coe '' s)ᶜ ↔ is_closed s ∧ is_compact s

@[simp]

theorem alexandroff.is_closed_image_coe {X : Type u_1} [topological_space X] {s : set X} :

is_closed (coe '' s) ↔ is_closed s ∧ is_compact s

def alexandroff.opens_of_compl {X : Type u_1} [topological_space X] (s : set X) (h₁ : is_closed s) (h₂ : is_compact s) :

topological_space.opens (alexandroff X)

An open set in alexandroff X constructed from a closed compact set in X

Equations

alexandroff.opens_of_compl s h₁ h₂ = {carrier := (coe '' s)ᶜ, is_open' := _}

theorem alexandroff.infty_mem_opens_of_compl {X : Type u_1} [topological_space X] {s : set X} (h₁ : is_closed s) (h₂ : is_compact s) :

alexandroff.infty ∈ alexandroff.opens_of_compl s h₁ h₂

@[continuity]

theorem alexandroff.continuous_coe {X : Type u_1} [topological_space X] :

theorem alexandroff.is_open_map_coe {X : Type u_1} [topological_space X] :

is_open_map coe

theorem alexandroff.open_embedding_coe {X : Type u_1} [topological_space X] :

open_embedding coe

theorem alexandroff.is_open_range_coe {X : Type u_1} [topological_space X] :

is_open (set.range coe)

theorem alexandroff.is_closed_infty {X : Type u_1} [topological_space X] :

is_closed {alexandroff.infty}

theorem alexandroff.nhds_coe_eq {X : Type u_1} [topological_space X] (x : X) :

nhds ↑x = filter.map coe (nhds x)

theorem alexandroff.nhds_within_coe_image {X : Type u_1} [topological_space X] (s : set X) (x : X) :

nhds_within ↑x (coe '' s) = filter.map coe (nhds_within x s)

theorem alexandroff.nhds_within_coe {X : Type u_1} [topological_space X] (s : set (alexandroff X)) (x : X) :

nhds_within ↑x s = filter.map coe (nhds_within x (coe ⁻¹' s))

theorem alexandroff.comap_coe_nhds {X : Type u_1} [topological_space X] (x : X) :

filter.comap coe (nhds ↑x) = nhds x

@[protected, instance]

def alexandroff.nhds_within_compl_coe_ne_bot {X : Type u_1} [topological_space X] (x : X) [h : (nhds_within x {x}ᶜ).ne_bot] :

(nhds_within ↑x {↑x}ᶜ).ne_bot

If x is not an isolated point of X, then x : alexandroff X is not an isolated point of alexandroff X.

theorem alexandroff.nhds_within_compl_infty_eq {X : Type u_1} [topological_space X] :

nhds_within alexandroff.infty {alexandroff.infty}ᶜ = filter.map coe (filter.coclosed_compact X)

@[protected, instance]

def alexandroff.nhds_within_compl_infty_ne_bot {X : Type u_1} [topological_space X] [noncompact_space X] :

(nhds_within alexandroff.infty {alexandroff.infty}ᶜ).ne_bot

If X is a non-compact space, then ∞ is not an isolated point of alexandroff X.

@[protected, instance]

def alexandroff.nhds_within_compl_ne_bot {X : Type u_1} [topological_space X] [∀ (x : X), (nhds_within x {x}ᶜ).ne_bot] [noncompact_space X] (x : alexandroff X) :

(nhds_within x {x}ᶜ).ne_bot

theorem alexandroff.nhds_infty_eq {X : Type u_1} [topological_space X] :

nhds alexandroff.infty = filter.map coe (filter.coclosed_compact X) ⊔ has_pure.pure alexandroff.infty

theorem alexandroff.has_basis_nhds_infty {X : Type u_1} [topological_space X] :

(nhds alexandroff.infty).has_basis (λ (s : set X), is_closed s ∧ is_compact s) (λ (s : set X), coe '' sᶜ ∪ {alexandroff.infty})

@[simp]

theorem alexandroff.comap_coe_nhds_infty {X : Type u_1} [topological_space X] :

filter.comap coe (nhds alexandroff.infty) = filter.coclosed_compact X

theorem alexandroff.le_nhds_infty {X : Type u_1} [topological_space X] {f : filter (alexandroff X)} :

f ≤ nhds alexandroff.infty ↔ ∀ (s : set X), is_closed s → is_compact s → coe '' sᶜ ∪ {alexandroff.infty} ∈ f

theorem alexandroff.ultrafilter_le_nhds_infty {X : Type u_1} [topological_space X] {f : ultrafilter (alexandroff X)} :

↑f ≤ nhds alexandroff.infty ↔ ∀ (s : set X), is_closed s → is_compact s → coe '' s ∉ f

theorem alexandroff.tendsto_nhds_infty' {X : Type u_1} [topological_space X] {α : Type u_2} {f : alexandroff X → α} {l : filter α} :

filter.tendsto f (nhds alexandroff.infty) l ↔ filter.tendsto f (has_pure.pure alexandroff.infty) l ∧ filter.tendsto (f ∘ coe) (filter.coclosed_compact X) l

theorem alexandroff.tendsto_nhds_infty {X : Type u_1} [topological_space X] {α : Type u_2} {f : alexandroff X → α} {l : filter α} :

filter.tendsto f (nhds alexandroff.infty) l ↔ ∀ (s : set α), s ∈ l → (f alexandroff.infty ∈ s ∧ ∃ (t : set X), is_closed t ∧ is_compact t ∧ set.maps_to (f ∘ coe) tᶜ s)

theorem alexandroff.continuous_at_infty' {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : alexandroff X → Y} :

continuous_at f alexandroff.infty ↔ filter.tendsto (f ∘ coe) (filter.coclosed_compact X) (nhds (f alexandroff.infty))

theorem alexandroff.continuous_at_infty {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : alexandroff X → Y} :

continuous_at f alexandroff.infty ↔ ∀ (s : set Y), s ∈ nhds (f alexandroff.infty) → (∃ (t : set X), is_closed t ∧ is_compact t ∧ set.maps_to (f ∘ coe) tᶜ s)

theorem alexandroff.continuous_at_coe {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : alexandroff X → Y} {x : X} :

continuous_at f ↑x ↔ continuous_at (f ∘ coe) x

theorem alexandroff.dense_range_coe {X : Type u_1} [topological_space X] [noncompact_space X] :

dense_range coe

If X is not a compact space, then the natural embedding X → alexandroff X has dense range.

theorem alexandroff.dense_embedding_coe {X : Type u_1} [topological_space X] [noncompact_space X] :

dense_embedding coe

@[simp]

theorem alexandroff.specializes_coe {X : Type u_1} [topological_space X] {x y : X} :

↑x ⤳ ↑y ↔ x ⤳ y

@[simp]

theorem alexandroff.inseparable_coe {X : Type u_1} [topological_space X] {x y : X} :

inseparable ↑x ↑y ↔ inseparable x y

theorem alexandroff.not_specializes_infty_coe {X : Type u_1} [topological_space X] {x : X} :

¬alexandroff.infty ⤳ ↑x

theorem alexandroff.not_inseparable_infty_coe {X : Type u_1} [topological_space X] {x : X} :

¬inseparable alexandroff.infty ↑x

theorem alexandroff.not_inseparable_coe_infty {X : Type u_1} [topological_space X] {x : X} :

¬inseparable ↑x alexandroff.infty

theorem alexandroff.inseparable_iff {X : Type u_1} [topological_space X] {x y : alexandroff X} :

inseparable x y ↔ x = alexandroff.infty ∧ y = alexandroff.infty ∨ ∃ (x' : X), x = ↑x' ∧ ∃ (y' : X), y = ↑y' ∧ inseparable x' y'

Compactness and separation properties #

In this section we prove that alexandroff X is a compact space; it is a T₀ (resp., T₁) space if the original space satisfies the same separation axiom. If the original space is a locally compact Hausdorff space, then alexandroff X is a normal (hence, T₃ and Hausdorff) space.

Finally, if the original space X is not compact and is a preconnected space, then alexandroff X is a connected space.

@[protected, instance]

def alexandroff.compact_space {X : Type u_1} [topological_space X] :

compact_space (alexandroff X)

For any topological space X, its one point compactification is a compact space.

@[protected, instance]

def alexandroff.t0_space {X : Type u_1} [topological_space X] [t0_space X] :

t0_space (alexandroff X)

The one point compactification of a t0_space space is a t0_space.

@[protected, instance]

def alexandroff.t1_space {X : Type u_1} [topological_space X] [t1_space X] :

t1_space (alexandroff X)

The one point compactification of a t1_space space is a t1_space.

@[protected, instance]

def alexandroff.normal_space {X : Type u_1} [topological_space X] [locally_compact_space X] [t2_space X] :

normal_space (alexandroff X)

The one point compactification of a locally compact Hausdorff space is a normal (hence, Hausdorff and regular) topological space.

@[protected, instance]

def alexandroff.connected_space {X : Type u_1} [topological_space X] [preconnected_space X] [noncompact_space X] :

connected_space (alexandroff X)

If X is not a compact space, then alexandroff X is a connected space.

theorem alexandroff.not_continuous_cofinite_topology_of_symm {X : Type u_1} [topological_space X] [infinite X] [discrete_topology X] :

¬continuous ⇑(cofinite_topology.of.symm)

If X is an infinite type with discrete topology (e.g., ℕ), then the identity map from cofinite_topology (alexandroff X) to alexandroff X is not continuous.

theorem continuous.homeo_of_equiv_compact_to_t2.t1_counterexample :

∃ (α β : Type) (Iα : topological_space α) (Iβ : topological_space β), compact_space α ∧ t1_space β ∧ ∃ (f : α ≃ β), continuous ⇑f ∧ ¬continuous ⇑(f.symm)

A concrete counterexample shows that continuous.homeo_of_equiv_compact_to_t2 cannot be generalized from t2_space to t1_space.

Let α = alexandroff ℕ be the one-point compactification of ℕ, and let β be the same space alexandroff ℕ with the cofinite topology. Then α is compact, β is T1, and the identity map id : α → β is a continuous equivalence that is not a homeomorphism.