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]

The repr uses the notation from the alexandroff locale.

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

The point at infinity

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[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 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
@[protected, instance]
Equations

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]

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

Equations
@[continuity]
@[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]

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]

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.