The OnePoint Compactification #

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

Main definitions #

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

Main results #

• The topological structure of OnePoint X
• The connectedness of OnePoint X for a noncompact, preconnected X
• OnePoint X is T₀ for a T₀ space X
• OnePoint X is T₁ for a T₁ space X
• OnePoint 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 OnePoint X to be the disjoint union of X and ∞, implemented as Option X. Then we restate some lemmas about Option X for OnePoint X.

def OnePoint (X : Type u_2) :
Type u_2

The OnePoint extension of an arbitrary topological space X

Equations
Instances For
instance instReprOnePoint {X : Type u_1} [Repr X] :
Repr ()

The repr uses the notation from the OnePoint locale.

Equations
• One or more equations did not get rendered due to their size.
@[match_pattern]
def OnePoint.infty {X : Type u_1} :

The point at infinity

Equations
• OnePoint.infty = none
Instances For

The point at infinity

Equations
Instances For
@[match_pattern]
def OnePoint.some {X : Type u_1} :
X

Coercion from X to OnePoint X.

Equations
• OnePoint.some = some
Instances For
instance OnePoint.instCoeTC {X : Type u_1} :
CoeTC X ()
Equations
• OnePoint.instCoeTC = { coe := OnePoint.some }
instance OnePoint.instInhabited {X : Type u_1} :
Equations
• OnePoint.instInhabited = { default := OnePoint.infty }
instance OnePoint.instFintype {X : Type u_1} [] :
Equations
instance OnePoint.infinite {X : Type u_1} [] :
Equations
• =
theorem OnePoint.coe_injective {X : Type u_1} :
Function.Injective OnePoint.some
theorem OnePoint.coe_eq_coe {X : Type u_1} {x : X} {y : X} :
x = y x = y
@[simp]
theorem OnePoint.coe_ne_infty {X : Type u_1} (x : X) :
x OnePoint.infty
@[simp]
theorem OnePoint.infty_ne_coe {X : Type u_1} (x : X) :
OnePoint.infty x
def OnePoint.rec {X : Type u_1} {C : Sort u_2} (h₁ : C OnePoint.infty) (h₂ : (x : X) → C x) (z : ) :
C z

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

Equations
Instances For
theorem OnePoint.isCompl_range_coe_infty {X : Type u_1} :
IsCompl (Set.range OnePoint.some) {OnePoint.infty}
theorem OnePoint.range_coe_union_infty {X : Type u_1} :
Set.range OnePoint.some {OnePoint.infty} = Set.univ
@[simp]
theorem OnePoint.insert_infty_range_coe {X : Type u_1} :
insert OnePoint.infty (Set.range OnePoint.some) = Set.univ
@[simp]
theorem OnePoint.range_coe_inter_infty {X : Type u_1} :
Set.range OnePoint.some {OnePoint.infty} =
@[simp]
theorem OnePoint.compl_range_coe {X : Type u_1} :
(Set.range OnePoint.some) = {OnePoint.infty}
theorem OnePoint.compl_infty {X : Type u_1} :
{OnePoint.infty} = Set.range OnePoint.some
theorem OnePoint.compl_image_coe {X : Type u_1} (s : Set X) :
(OnePoint.some '' s) = OnePoint.some '' s {OnePoint.infty}
theorem OnePoint.ne_infty_iff_exists {X : Type u_1} {x : } :
x OnePoint.infty ∃ (y : X), y = x
instance OnePoint.canLift {X : Type u_1} :
CanLift () X OnePoint.some fun (x : ) => x OnePoint.infty
Equations
• =
theorem OnePoint.not_mem_range_coe_iff {X : Type u_1} {x : } :
xSet.range OnePoint.some x = OnePoint.infty
theorem OnePoint.infty_not_mem_range_coe {X : Type u_1} :
OnePoint.inftySet.range OnePoint.some
theorem OnePoint.infty_not_mem_image_coe {X : Type u_1} {s : Set X} :
OnePoint.inftyOnePoint.some '' s
@[simp]
theorem OnePoint.coe_preimage_infty {X : Type u_1} :
OnePoint.some ⁻¹' {OnePoint.infty} =

Topological space structure on OnePoint X#

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

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

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

instance OnePoint.instTopologicalSpace {X : Type u_1} [] :
Equations
• One or more equations did not get rendered due to their size.
theorem OnePoint.isOpen_def {X : Type u_1} [] {s : Set ()} :
(OnePoint.infty sIsCompact (OnePoint.some ⁻¹' s)) IsOpen (OnePoint.some ⁻¹' s)
theorem OnePoint.isOpen_iff_of_mem' {X : Type u_1} [] {s : Set ()} (h : OnePoint.infty s) :
IsCompact (OnePoint.some ⁻¹' s) IsOpen (OnePoint.some ⁻¹' s)
theorem OnePoint.isOpen_iff_of_mem {X : Type u_1} [] {s : Set ()} (h : OnePoint.infty s) :
IsClosed (OnePoint.some ⁻¹' s) IsCompact (OnePoint.some ⁻¹' s)
theorem OnePoint.isOpen_iff_of_not_mem {X : Type u_1} [] {s : Set ()} (h : OnePoint.inftys) :
IsOpen (OnePoint.some ⁻¹' s)
theorem OnePoint.isClosed_iff_of_mem {X : Type u_1} [] {s : Set ()} (h : OnePoint.infty s) :
IsClosed (OnePoint.some ⁻¹' s)
theorem OnePoint.isClosed_iff_of_not_mem {X : Type u_1} [] {s : Set ()} (h : OnePoint.inftys) :
IsClosed (OnePoint.some ⁻¹' s) IsCompact (OnePoint.some ⁻¹' s)
@[simp]
theorem OnePoint.isOpen_image_coe {X : Type u_1} [] {s : Set X} :
IsOpen (OnePoint.some '' s)
theorem OnePoint.isOpen_compl_image_coe {X : Type u_1} [] {s : Set X} :
IsOpen (OnePoint.some '' s)
@[simp]
theorem OnePoint.isClosed_image_coe {X : Type u_1} [] {s : Set X} :
IsClosed (OnePoint.some '' s)
def OnePoint.opensOfCompl {X : Type u_1} [] (s : Set X) (h₁ : ) (h₂ : ) :

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

Equations
• = { carrier := (OnePoint.some '' s), is_open' := }
Instances For
theorem OnePoint.infty_mem_opensOfCompl {X : Type u_1} [] {s : Set X} (h₁ : ) (h₂ : ) :
OnePoint.infty
theorem OnePoint.continuous_coe {X : Type u_1} [] :
Continuous OnePoint.some
theorem OnePoint.isOpenMap_coe {X : Type u_1} [] :
IsOpenMap OnePoint.some
theorem OnePoint.openEmbedding_coe {X : Type u_1} [] :
OpenEmbedding OnePoint.some
theorem OnePoint.isOpen_range_coe {X : Type u_1} [] :
IsOpen (Set.range OnePoint.some)
theorem OnePoint.isClosed_infty {X : Type u_1} [] :
IsClosed {OnePoint.infty}
theorem OnePoint.nhds_coe_eq {X : Type u_1} [] (x : X) :
nhds x = Filter.map OnePoint.some (nhds x)
theorem OnePoint.nhdsWithin_coe_image {X : Type u_1} [] (s : Set X) (x : X) :
nhdsWithin (x) (OnePoint.some '' s) = Filter.map OnePoint.some ()
theorem OnePoint.nhdsWithin_coe {X : Type u_1} [] (s : Set ()) (x : X) :
nhdsWithin (x) s = Filter.map OnePoint.some (nhdsWithin x (OnePoint.some ⁻¹' s))
theorem OnePoint.comap_coe_nhds {X : Type u_1} [] (x : X) :
Filter.comap OnePoint.some (nhds x) = nhds x
instance OnePoint.nhdsWithin_compl_coe_neBot {X : Type u_1} [] (x : X) [h : (nhdsWithin x {x}).NeBot] :
(nhdsWithin x {x}).NeBot

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

Equations
• =
theorem OnePoint.nhdsWithin_compl_infty_eq {X : Type u_1} [] :
nhdsWithin OnePoint.infty {OnePoint.infty} = Filter.map OnePoint.some
instance OnePoint.nhdsWithin_compl_infty_neBot {X : Type u_1} [] [] :
(nhdsWithin OnePoint.infty {OnePoint.infty}).NeBot

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

Equations
• =
@[instance 900]
instance OnePoint.nhdsWithin_compl_neBot {X : Type u_1} [] [∀ (x : X), (nhdsWithin x {x}).NeBot] [] (x : ) :
(nhdsWithin x {x}).NeBot
Equations
• =
theorem OnePoint.nhds_infty_eq {X : Type u_1} [] :
nhds OnePoint.infty = Filter.map OnePoint.some pure OnePoint.infty
theorem OnePoint.hasBasis_nhds_infty {X : Type u_1} [] :
(nhds OnePoint.infty).HasBasis (fun (s : Set X) => ) fun (s : Set X) => OnePoint.some '' s {OnePoint.infty}
@[simp]
theorem OnePoint.comap_coe_nhds_infty {X : Type u_1} [] :
Filter.comap OnePoint.some (nhds OnePoint.infty) =
theorem OnePoint.le_nhds_infty {X : Type u_1} [] {f : Filter ()} :
f nhds OnePoint.infty ∀ (s : Set X), OnePoint.some '' s {OnePoint.infty} f
theorem OnePoint.ultrafilter_le_nhds_infty {X : Type u_1} [] {f : } :
f nhds OnePoint.infty ∀ (s : Set X), OnePoint.some '' sf
theorem OnePoint.tendsto_nhds_infty' {X : Type u_1} [] {α : Type u_2} {f : α} {l : } :
Filter.Tendsto f (nhds OnePoint.infty) l Filter.Tendsto f (pure OnePoint.infty) l Filter.Tendsto (f OnePoint.some) l
theorem OnePoint.tendsto_nhds_infty {X : Type u_1} [] {α : Type u_2} {f : α} {l : } :
Filter.Tendsto f (nhds OnePoint.infty) l sl, f OnePoint.infty s ∃ (t : Set X), Set.MapsTo (f OnePoint.some) t s
theorem OnePoint.continuousAt_infty' {X : Type u_1} [] {Y : Type u_2} [] {f : Y} :
ContinuousAt f OnePoint.infty Filter.Tendsto (f OnePoint.some) (nhds (f OnePoint.infty))
theorem OnePoint.continuousAt_infty {X : Type u_1} [] {Y : Type u_2} [] {f : Y} :
ContinuousAt f OnePoint.infty snhds (f OnePoint.infty), ∃ (t : Set X), Set.MapsTo (f OnePoint.some) t s
theorem OnePoint.continuousAt_coe {X : Type u_1} [] {Y : Type u_2} [] {f : Y} {x : X} :
ContinuousAt f x ContinuousAt (f OnePoint.some) x
theorem OnePoint.denseRange_coe {X : Type u_1} [] [] :
DenseRange OnePoint.some

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

theorem OnePoint.denseEmbedding_coe {X : Type u_1} [] [] :
DenseEmbedding OnePoint.some
@[simp]
theorem OnePoint.specializes_coe {X : Type u_1} [] {x : X} {y : X} :
x y x y
@[simp]
theorem OnePoint.inseparable_coe {X : Type u_1} [] {x : X} {y : X} :
Inseparable x y
theorem OnePoint.not_specializes_infty_coe {X : Type u_1} [] {x : X} :
¬OnePoint.infty x
theorem OnePoint.not_inseparable_infty_coe {X : Type u_1} [] {x : X} :
¬Inseparable OnePoint.infty x
theorem OnePoint.not_inseparable_coe_infty {X : Type u_1} [] {x : X} :
¬Inseparable (x) OnePoint.infty
theorem OnePoint.inseparable_iff {X : Type u_1} [] {x : } {y : } :
x = OnePoint.infty y = OnePoint.infty ∃ (x' : X), x = x' ∃ (y' : X), y = y' Inseparable x' y'

Compactness and separation properties #

In this section we prove that OnePoint 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 OnePoint X is a normal (hence, T₃ and Hausdorff) space.

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

instance OnePoint.instCompactSpace {X : Type u_1} [] :

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

Equations
• =
instance OnePoint.instT0Space {X : Type u_1} [] [] :

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

Equations
• =
instance OnePoint.instT1Space {X : Type u_1} [] [] :

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

Equations
• =

The one point compactification of a locally compact R₁ space is a normal topological space.

Equations
• =

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

Equations
• =
theorem OnePoint.not_continuous_cofiniteTopology_of_symm {X : Type u_1} [] [] [] :
¬Continuous CofiniteTopology.of.symm

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

theorem Continuous.homeoOfEquivCompactToT2.t1_counterexample :
∃ (α : Type) (β : Type) (x : ) (x_1 : ), ∃ (f : α β), ¬Continuous f.symm

A concrete counterexample shows that Continuous.homeoOfEquivCompactToT2 cannot be generalized from T2Space to T1Space.

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