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

• OnePoint X = Option X

instance instReprOnePoint {X : Type u_1} [Repr X] : Repr (OnePoint X)

The repr uses the notation from the OnePoint locale.

Equations

• instReprOnePoint = { reprPrec := fun (o : OnePoint X) (x : ℕ) => match o with | none => Std.Format.text "∞" | some a => Std.Format.text "↑" ++ repr a }

@[match_pattern]

def OnePoint.infty {X : Type u_1} : OnePoint X

The point at infinity

Equations

• OnePoint.infty = none

def OnePoint.«term∞» : Lean.ParserDescr

The point at infinity

Equations

• OnePoint.«term∞» = Lean.ParserDescr.node `OnePoint.term∞ 1024 (Lean.ParserDescr.symbol "∞")

@[match_pattern]

def OnePoint.some {X : Type u_1} : X → OnePoint X

Coercion from X to OnePoint X.

Equations

• OnePoint.some = some

instance OnePoint.instCoeTC {X : Type u_1} : CoeTC X (OnePoint X)

Equations

• OnePoint.instCoeTC = { coe := OnePoint.some }

instance OnePoint.instInhabited {X : Type u_1} : Inhabited (OnePoint X)

Equations

• OnePoint.instInhabited = { default := OnePoint.infty }

theorem OnePoint.forall {X : Type u_1} {p : OnePoint X → Prop} : (∀ (x : OnePoint X), p x) ↔ p OnePoint.infty ∧ ∀ (x : X), p ↑x

theorem OnePoint.exists {X : Type u_1} {p : OnePoint X → Prop} : (∃ (x : OnePoint X), p x) ↔ p OnePoint.infty ∨ ∃ (x : X), p ↑x

instance OnePoint.instFintype {X : Type u_1} [Fintype X] : Fintype (OnePoint X)

Equations

• OnePoint.instFintype = inferInstanceAs (Fintype (Option X))

instance OnePoint.infinite {X : Type u_1} [Infinite X] : Infinite (OnePoint X)

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 : OnePoint X → Sort u_2} (h₁ : C OnePoint.infty) (h₂ : (x : X) → C ↑x) (z : OnePoint X) : C z

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

Equations

• OnePoint.rec h₁ h₂ x = match x with | none => h₁ | some x => h₂ x

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 : OnePoint X} : x ≠ OnePoint.infty ↔ ∃ (y : X), ↑y = x

instance OnePoint.canLift {X : Type u_1} : CanLift (OnePoint X) X OnePoint.some fun (x : OnePoint X) => x ≠ OnePoint.infty

Equations

• ⋯ = ⋯

theorem OnePoint.not_mem_range_coe_iff {X : Type u_1} {x : OnePoint X} : x ∉ Set.range OnePoint.some ↔ x = OnePoint.infty

theorem OnePoint.infty_not_mem_range_coe {X : Type u_1} : OnePoint.infty ∉ Set.range OnePoint.some

theorem OnePoint.infty_not_mem_image_coe {X : Type u_1} {s : Set X} : OnePoint.infty ∉ OnePoint.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} [TopologicalSpace X] : TopologicalSpace (OnePoint X)

Equations

• One or more equations did not get rendered due to their size.

theorem OnePoint.isOpen_def {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} : IsOpen s ↔ (OnePoint.infty ∈ s → IsCompact (OnePoint.some ⁻¹' s)ᶜ) ∧ IsOpen (OnePoint.some ⁻¹' s)

theorem OnePoint.isOpen_iff_of_mem' {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.infty ∈ s) : IsOpen s ↔ IsCompact (OnePoint.some ⁻¹' s)ᶜ ∧ IsOpen (OnePoint.some ⁻¹' s)

theorem OnePoint.isOpen_iff_of_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.infty ∈ s) : IsOpen s ↔ IsClosed (OnePoint.some ⁻¹' s)ᶜ ∧ IsCompact (OnePoint.some ⁻¹' s)ᶜ

theorem OnePoint.isOpen_iff_of_not_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.infty ∉ s) : IsOpen s ↔ IsOpen (OnePoint.some ⁻¹' s)

theorem OnePoint.isClosed_iff_of_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.infty ∈ s) : IsClosed s ↔ IsClosed (OnePoint.some ⁻¹' s)

theorem OnePoint.isClosed_iff_of_not_mem {X : Type u_1} [TopologicalSpace X] {s : Set (OnePoint X)} (h : OnePoint.infty ∉ s) : IsClosed s ↔ IsClosed (OnePoint.some ⁻¹' s) ∧ IsCompact (OnePoint.some ⁻¹' s)

@[simp]

theorem OnePoint.isOpen_image_coe {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsOpen (OnePoint.some '' s) ↔ IsOpen s

theorem OnePoint.isOpen_compl_image_coe {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsOpen (OnePoint.some '' s)ᶜ ↔ IsClosed s ∧ IsCompact s

@[simp]

theorem OnePoint.isClosed_image_coe {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsClosed (OnePoint.some '' s) ↔ IsClosed s ∧ IsCompact s

def OnePoint.opensOfCompl {X : Type u_1} [TopologicalSpace X] (s : Set X) (h₁ : IsClosed s) (h₂ : IsCompact s) : TopologicalSpace.Opens (OnePoint X)

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

Equations

• OnePoint.opensOfCompl s h₁ h₂ = { carrier := (OnePoint.some '' s)ᶜ, is_open' := ⋯ }

theorem OnePoint.infty_mem_opensOfCompl {X : Type u_1} [TopologicalSpace X] {s : Set X} (h₁ : IsClosed s) (h₂ : IsCompact s) : OnePoint.infty ∈ OnePoint.opensOfCompl s h₁ h₂

theorem OnePoint.continuous_coe {X : Type u_1} [TopologicalSpace X] : Continuous OnePoint.some

theorem OnePoint.isOpenMap_coe {X : Type u_1} [TopologicalSpace X] : IsOpenMap OnePoint.some

theorem OnePoint.openEmbedding_coe {X : Type u_1} [TopologicalSpace X] : OpenEmbedding OnePoint.some

theorem OnePoint.isOpen_range_coe {X : Type u_1} [TopologicalSpace X] : IsOpen (Set.range OnePoint.some)

theorem OnePoint.isClosed_infty {X : Type u_1} [TopologicalSpace X] : IsClosed {OnePoint.infty}

theorem OnePoint.nhds_coe_eq {X : Type u_1} [TopologicalSpace X] (x : X) : nhds ↑x = Filter.map OnePoint.some (nhds x)

theorem OnePoint.nhdsWithin_coe_image {X : Type u_1} [TopologicalSpace X] (s : Set X) (x : X) : nhdsWithin (↑x) (OnePoint.some '' s) = Filter.map OnePoint.some (nhdsWithin x s)

theorem OnePoint.nhdsWithin_coe {X : Type u_1} [TopologicalSpace X] (s : Set (OnePoint X)) (x : X) : nhdsWithin (↑x) s = Filter.map OnePoint.some (nhdsWithin x (OnePoint.some ⁻¹' s))

theorem OnePoint.comap_coe_nhds {X : Type u_1} [TopologicalSpace X] (x : X) : Filter.comap OnePoint.some (nhds ↑x) = nhds x

instance OnePoint.nhdsWithin_compl_coe_neBot {X : Type u_1} [TopologicalSpace X] (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} [TopologicalSpace X] : nhdsWithin OnePoint.infty {OnePoint.infty}ᶜ = Filter.map OnePoint.some (Filter.coclosedCompact X)

instance OnePoint.nhdsWithin_compl_infty_neBot {X : Type u_1} [TopologicalSpace X] [NoncompactSpace X] : (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} [TopologicalSpace X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] [NoncompactSpace X] (x : OnePoint X) : (nhdsWithin x {x}ᶜ).NeBot

Equations

• ⋯ = ⋯

theorem OnePoint.nhds_infty_eq {X : Type u_1} [TopologicalSpace X] : nhds OnePoint.infty = Filter.map OnePoint.some (Filter.coclosedCompact X) ⊔ pure OnePoint.infty

theorem OnePoint.tendsto_coe_infty {X : Type u_1} [TopologicalSpace X] : Filter.Tendsto OnePoint.some (Filter.coclosedCompact X) (nhds OnePoint.infty)

theorem OnePoint.hasBasis_nhds_infty {X : Type u_1} [TopologicalSpace X] : (nhds OnePoint.infty).HasBasis (fun (s : Set X) => IsClosed s ∧ IsCompact s) fun (s : Set X) => OnePoint.some '' sᶜ ∪ {OnePoint.infty}

@[simp]

theorem OnePoint.comap_coe_nhds_infty {X : Type u_1} [TopologicalSpace X] : Filter.comap OnePoint.some (nhds OnePoint.infty) = Filter.coclosedCompact X

theorem OnePoint.le_nhds_infty {X : Type u_1} [TopologicalSpace X] {f : Filter (OnePoint X)} : f ≤ nhds OnePoint.infty ↔ ∀ (s : Set X), IsClosed s → IsCompact s → OnePoint.some '' sᶜ ∪ {OnePoint.infty} ∈ f

theorem OnePoint.ultrafilter_le_nhds_infty {X : Type u_1} [TopologicalSpace X] {f : Ultrafilter (OnePoint X)} : ↑f ≤ nhds OnePoint.infty ↔ ∀ (s : Set X), IsClosed s → IsCompact s → OnePoint.some '' s ∉ f

theorem OnePoint.tendsto_nhds_infty' {X : Type u_1} [TopologicalSpace X] {α : Type u_2} {f : OnePoint X → α} {l : Filter α} : Filter.Tendsto f (nhds OnePoint.infty) l ↔ Filter.Tendsto f (pure OnePoint.infty) l ∧ Filter.Tendsto (f ∘ OnePoint.some) (Filter.coclosedCompact X) l

theorem OnePoint.tendsto_nhds_infty {X : Type u_1} [TopologicalSpace X] {α : Type u_2} {f : OnePoint X → α} {l : Filter α} : Filter.Tendsto f (nhds OnePoint.infty) l ↔ ∀ s ∈ l, f OnePoint.infty ∈ s ∧ ∃ (t : Set X), IsClosed t ∧ IsCompact t ∧ Set.MapsTo (f ∘ OnePoint.some) tᶜ s

theorem OnePoint.continuousAt_infty' {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : OnePoint X → Y} : ContinuousAt f OnePoint.infty ↔ Filter.Tendsto (f ∘ OnePoint.some) (Filter.coclosedCompact X) (nhds (f OnePoint.infty))

theorem OnePoint.continuousAt_infty {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : OnePoint X → Y} : ContinuousAt f OnePoint.infty ↔ ∀ s ∈ nhds (f OnePoint.infty), ∃ (t : Set X), IsClosed t ∧ IsCompact t ∧ Set.MapsTo (f ∘ OnePoint.some) tᶜ s

theorem OnePoint.continuousAt_coe {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {f : OnePoint X → Y} {x : X} : ContinuousAt f ↑x ↔ ContinuousAt (f ∘ OnePoint.some) x

theorem OnePoint.continuous_iff {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] (f : OnePoint X → Y) : Continuous f ↔ Filter.Tendsto (fun (x : X) => f ↑x) (Filter.coclosedCompact X) (nhds (f OnePoint.infty)) ∧ Continuous fun (x : X) => f ↑x

def OnePoint.continuousMapMk {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] (f : C(X, Y)) (y : Y) (h : Filter.Tendsto (⇑f) (Filter.coclosedCompact X) (nhds y)) : C(OnePoint X, Y)

A constructor for continuous maps out of a one point compactification, given a continuous map from the underlying space and a limit value at infinity.

Equations

• OnePoint.continuousMapMk f y h = { toFun := fun (x : OnePoint X) => match x with | none => y | some x => f x, continuous_toFun := ⋯ }

theorem OnePoint.continuous_iff_from_discrete {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] [DiscreteTopology X] (f : OnePoint X → Y) : Continuous f ↔ Filter.Tendsto (fun (x : X) => f ↑x) Filter.cofinite (nhds (f OnePoint.infty))

def OnePoint.continuousMapMkDiscrete {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] [DiscreteTopology X] (f : X → Y) (y : Y) (h : Filter.Tendsto f Filter.cofinite (nhds y)) : C(OnePoint X, Y)

A constructor for continuous maps out of a one point compactification of a discrete space, given a map from the underlying space and a limit value at infinity.

Equations

• OnePoint.continuousMapMkDiscrete f y h = OnePoint.continuousMapMk { toFun := f, continuous_toFun := ⋯ } y ⋯

noncomputable def OnePoint.continuousMapDiscreteEquiv (X : Type u_1) [TopologicalSpace X] (Y : Type u_2) [DiscreteTopology X] [TopologicalSpace Y] [T2Space Y] [Infinite X] : C(OnePoint X, Y) ≃ { f : X → Y // ∃ (L : Y), Filter.Tendsto (fun (x : X) => f x) Filter.cofinite (nhds L) }

Continuous maps out of the one point compactification of an infinite discrete space to a Hausdorff space correspond bijectively to "convergent" maps out of the discrete space.

Equations

• One or more equations did not get rendered due to their size.

theorem OnePoint.continuous_iff_from_nat {Y : Type u_2} [TopologicalSpace Y] (f : OnePoint ℕ → Y) : Continuous f ↔ Filter.Tendsto (fun (x : ℕ) => f ↑x) Filter.atTop (nhds (f OnePoint.infty))

def OnePoint.continuousMapMkNat {Y : Type u_2} [TopologicalSpace Y] (f : ℕ → Y) (y : Y) (h : Filter.Tendsto f Filter.atTop (nhds y)) : C(OnePoint ℕ, Y)

A constructor for continuous maps out of the one point compactification of ℕ, given a sequence and a limit value at infinity.

Equations

• OnePoint.continuousMapMkNat f y h = OnePoint.continuousMapMkDiscrete f y ⋯

noncomputable def OnePoint.continuousMapNatEquiv (Y : Type u_2) [TopologicalSpace Y] [T2Space Y] : C(OnePoint ℕ, Y) ≃ { f : ℕ → Y // ∃ (L : Y), Filter.Tendsto (fun (x : ℕ) => f x) Filter.atTop (nhds L) }

Continuous maps out of the one point compactification of ℕ to a Hausdorff space Y correspond bijectively to convergent sequences in Y.

Equations

• One or more equations did not get rendered due to their size.

theorem OnePoint.denseRange_coe {X : Type u_1} [TopologicalSpace X] [NoncompactSpace X] : 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} [TopologicalSpace X] [NoncompactSpace X] : DenseEmbedding OnePoint.some

@[simp]

theorem OnePoint.specializes_coe {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} : ↑x ⤳ ↑y ↔ x ⤳ y

@[simp]

theorem OnePoint.inseparable_coe {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} : Inseparable ↑x ↑y ↔ Inseparable x y

theorem OnePoint.not_specializes_infty_coe {X : Type u_1} [TopologicalSpace X] {x : X} : ¬OnePoint.infty ⤳ ↑x

theorem OnePoint.not_inseparable_infty_coe {X : Type u_1} [TopologicalSpace X] {x : X} : ¬Inseparable OnePoint.infty ↑x

theorem OnePoint.not_inseparable_coe_infty {X : Type u_1} [TopologicalSpace X] {x : X} : ¬Inseparable (↑x) OnePoint.infty

theorem OnePoint.inseparable_iff {X : Type u_1} [TopologicalSpace X] {x : OnePoint X} {y : OnePoint X} : Inseparable 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} [TopologicalSpace X] : CompactSpace (OnePoint X)

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

Equations

• ⋯ = ⋯

instance OnePoint.instT0Space {X : Type u_1} [TopologicalSpace X] [T0Space X] : T0Space (OnePoint X)

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

Equations

• ⋯ = ⋯

instance OnePoint.instT1Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : T1Space (OnePoint X)

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

Equations

• ⋯ = ⋯

instance OnePoint.instNormalSpaceOfLocallyCompactSpaceOfR1Space {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [R1Space X] : NormalSpace (OnePoint X)

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

Equations

• ⋯ = ⋯

instance OnePoint.instConnectedSpaceOfPreconnectedSpaceOfNoncompactSpace {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] [NoncompactSpace X] : ConnectedSpace (OnePoint X)

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} [TopologicalSpace X] [Infinite X] [DiscreteTopology X] : ¬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.

instance OnePoint.instTotallySeparatedSpaceOfDiscreteTopology (X : Type u_2) [TopologicalSpace X] [DiscreteTopology X] : TotallySeparatedSpace (OnePoint X)

Equations

• ⋯ = ⋯

theorem Continuous.homeoOfEquivCompactToT2.t1_counterexample : ∃ (α : Type) (β : Type) (x : TopologicalSpace α) (x_1 : TopologicalSpace β), CompactSpace α ∧ T1Space β ∧ ∃ (f : α ≃ β), Continuous ⇑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.