mathlib documentation

topology.alexandroff

The Alexandroff Compactification #

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

Main definitions #

Main results #

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.

@[protected, instance]
def alexandroff.has_repr {X : Type u_1} [has_repr X] :

The repr uses the notation from the alexandroff locale.

Equations
def alexandroff.infty {X : Type u_1} :

The point at infinity

Equations
@[protected, instance]
def alexandroff.has_coe_t {X : Type u_1} :
Equations
@[protected, instance]
def alexandroff.inhabited {X : Type u_1} :
Equations
@[protected, instance]
def alexandroff.fintype {X : Type u_1} [fintype X] :
Equations
@[protected, instance]
def alexandroff.infinite {X : Type u_1} [infinite X] :
@[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) :
@[simp]
theorem alexandroff.infty_ne_coe {X : Type u_1} (x : X) :
@[protected]
def alexandroff.rec {X : Type u_1} (C : alexandroff XSort 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
@[simp]
theorem alexandroff.compl_image_coe {X : Type u_1} (s : set X) :
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} :
Equations
@[simp]

Topological space structure on alexandroff X #

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

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.

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

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

Equations
@[continuity]
theorem alexandroff.nhds_coe_eq {X : Type u_1} [topological_space X] (x : X) :
theorem alexandroff.nhds_within_coe_image {X : Type u_1} [topological_space X] (s : set X) (x : X) :
theorem alexandroff.comap_coe_nhds {X : Type u_1} [topological_space X] (x : X) :
@[protected, instance]

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

@[protected, instance]

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

@[protected, instance]
theorem alexandroff.tendsto_nhds_infty {X : Type u_1} [topological_space X] {α : Type u_2} {f : alexandroff X → α} {l : filter α} :
theorem alexandroff.continuous_at_infty {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {f : alexandroff X → Y} :
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} :

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

@[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} :
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]

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

@[protected, instance]

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

@[protected, instance]

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

@[protected, instance]

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

@[protected, instance]

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

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.

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.