Maps on one-point compactifications

The extension OnePoint.map f sends infinity to infinity. Its range is the range of f, embedded in the target compactification, together with infinity, and it is injective exactly when f is injective. For a proper map between arbitrary topological spaces, this extension is continuous. Closed embeddings extend to closed embeddings. These lemmas allow proper parametrizations to be compactified, with an explicit description of their range after adjoining infinity and a criterion for injectivity.

@[simp]

theorem TauCeti.onePointMap_injective_iff {X : Type u_1} {Y : Type u_2} {f : X → Y} : Function.Injective (OnePoint.map f) ↔ Function.Injective f

Extension to one-point compactifications preserves and reflects injectivity.

@[simp]

theorem TauCeti.range_onePointMap {X : Type u_1} {Y : Type u_2} (f : X → Y) : Set.range (OnePoint.map f) = insert OnePoint.infty (OnePoint.some '' Set.range f)

The range of the extension to one-point compactifications is the embedded range together with the point at infinity.

theorem TauCeti.continuous_onePointMap_of_isProperMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsProperMap f) : Continuous (OnePoint.map f)

A proper map between arbitrary topological spaces extends continuously to the one-point compactifications, sending infinity to infinity.

theorem TauCeti.isClosedEmbedding_onePointMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsClosedEmbedding f) : Topology.IsClosedEmbedding (OnePoint.map f)

A closed embedding between arbitrary topological spaces extends to a closed embedding of their one-point compactifications.