A set converging along the cofinite filter is a one-point compactification

Let s be a subset of a Hausdorff space X whose inclusion tends to a point a along the cofinite filter: every neighbourhood of a contains all but finitely many points of s. Away from a the set s is then discrete (Filter.Tendsto.discreteTopology_diff_singleton), and adding a to it produces a compact space in which a is the only point that may be non-isolated, so insert a s is the one-point compactification of the discrete space s \ {a}, with a as the point at infinity (Filter.Tendsto.onePointHomeomorphInsert).

This is the topological form of a set converging to 1 in a profinite group: for such a set s, the pointed space (insert 1 s, 1) is the pointed one-point compactification ((s \ {1})⁺, ∞), which is what identifies the free pro-p group on it with the free pro-p group on a pointed one-point compactification.

Main results

• Filter.Tendsto.discreteTopology_diff_singleton: a set converging to a along the cofinite filter is discrete once a is removed.
• Filter.Tendsto.onePointHomeomorphInsert: the homeomorphism (s \ {a})⁺ ≃ₜ insert a s sending ∞ to a.

theorem Filter.Tendsto.discreteTopology_diff_singleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {a : X} (h : Tendsto Subtype.val cofinite (nhds a)) : DiscreteTopology ↑(s \ {a})

A set whose inclusion tends to a along the cofinite filter is discrete once a is removed.

noncomputable def Filter.Tendsto.onePointHomeomorphInsert {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {a : X} (h : Tendsto Subtype.val cofinite (nhds a)) : OnePoint ↑(s \ {a}) ≃ₜ ↑(insert a s)

A set converging to a along the cofinite filter, with a added, is the one-point compactification of its complement of a: the homeomorphism (s \ {a})⁺ ≃ₜ insert a s that is the inclusion on s \ {a} and sends ∞ to a.

Equations

• h.onePointHomeomorphInsert = OnePoint.equivOfIsEmbeddingOfRangeEq ⟨a, ⋯⟩ (Set.inclusion ⋯) ⋯ ⋯

@[simp]

theorem Filter.Tendsto.onePointHomeomorphInsert_apply_coe {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {a : X} (h : Tendsto Subtype.val cofinite (nhds a)) (x : ↑(s \ {a})) : h.onePointHomeomorphInsert ↑x = ⟨↑x, ⋯⟩

The homeomorphism (s \ {a})⁺ ≃ₜ insert a s is the inclusion on s \ {a}.

@[simp]

theorem Filter.Tendsto.onePointHomeomorphInsert_apply_infty {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {a : X} (h : Tendsto Subtype.val cofinite (nhds a)) : h.onePointHomeomorphInsert OnePoint.infty = ⟨a, ⋯⟩

The homeomorphism (s \ {a})⁺ ≃ₜ insert a s sends the point at infinity to a.

@[simp]

theorem Filter.Tendsto.onePointHomeomorphInsert_symm_apply_left {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {a : X} (h : Tendsto Subtype.val cofinite (nhds a)) : h.onePointHomeomorphInsert.symm ⟨a, ⋯⟩ = OnePoint.infty

The inverse of the homeomorphism (s \ {a})⁺ ≃ₜ insert a s sends a to the point at infinity.

@[simp]

theorem Filter.Tendsto.onePointHomeomorphInsert_symm_apply_of_ne {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {a : X} (h : Tendsto Subtype.val cofinite (nhds a)) (y : ↑(insert a s)) (hy : ↑y ≠ a) : h.onePointHomeomorphInsert.symm y = ↑⟨↑y, ⋯⟩

The inverse of the homeomorphism (s \ {a})⁺ ≃ₜ insert a s is the inclusion on the points other than a.