feat: One-point compactification of Euclidean space homeomorphic to sphere (#18711)

The one-point compactification of n-dimensional Euclidean space is homeomorphic to the n-sphere.



Co-authored-by: Bjørn Kjos-Hanssen <bjoernkh@hawaii.edu>

Author: ocfnash

Mathlib.lean

@@ -6093,6 +6093,7 @@ import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Compactification.OnePoint
 import Mathlib.Topology.Compactification.OnePoint.Basic
 import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
+import Mathlib.Topology.Compactification.OnePoint.Sphere
 import Mathlib.Topology.Compactification.OnePointEquiv
 import Mathlib.Topology.Compactness.Bases
 import Mathlib.Topology.Compactness.Compact

Mathlib/Geometry/Manifold/Instances/Sphere.lean

@@ -288,6 +288,22 @@ theorem stereographic_neg_apply (v : sphere (0 : E) 1) :
   ext1
   simp
 
+theorem surjective_stereographic (hv : ‖v‖ = 1) :
+    Surjective (stereographic hv) :=
+  (stereographic hv).surjective_of_target_eq_univ rfl
+
+@[simp]
+theorem range_stereographic_symm (hv : ‖v‖ = 1) (hv' : v ∈ sphere 0 1 := by simpa) :
+    Set.range (stereographic hv).symm = {⟨v, hv'⟩}ᶜ := by
+  refine le_antisymm ?_ (stereographic hv).symm.target_subset_range
+  rintro x ⟨y, rfl⟩
+  suffices y ∈ (stereographic hv).target from (fun _ ↦ (stereographic hv).map_target) y this
+  simp
+
+lemma isOpenEmbedding_stereographic_symm (hv : ‖v‖ = 1) :
+    Topology.IsOpenEmbedding (stereographic hv).symm :=
+  (stereographic hv).symm.to_isOpenEmbedding (by simp)
+
 end StereographicProjection
 
 section ChartedSpace

Mathlib/Logic/Equiv/PartialEquiv.lean

@@ -196,6 +196,9 @@ theorem left_inv {x : α} (h : x ∈ e.source) : e.symm (e x) = x :=
 theorem right_inv {x : β} (h : x ∈ e.target) : e (e.symm x) = x :=
   e.right_inv' h
 
+theorem target_subset_range : e.target ⊆ range e :=
+  fun x hx ↦ ⟨e.symm x, right_inv e hx⟩
+
 theorem eq_symm_apply {x : α} {y : β} (hx : x ∈ e.source) (hy : y ∈ e.target) :
     x = e.symm y ↔ e x = y :=
   ⟨fun h => by rw [← e.right_inv hy, h], fun h => by rw [← e.left_inv hx, h]⟩
@@ -876,6 +879,22 @@ theorem pi_trans (ei : ∀ i, PartialEquiv (αi i) (βi i)) (ei' : ∀ i, Partia
 
 end Pi
 
+lemma surjective_of_target_eq_univ (h : e.target = univ) :
+    Surjective e :=
+  surjective_iff_surjOn_univ.mpr <| e.surjOn.mono (by simp) (by simp [h])
+
+lemma injective_of_source_eq_univ (h : e.source = univ) :
+    Injective e := by
+  simpa [injective_iff_injOn_univ, h] using e.injOn
+
+lemma injective_symm_of_target_eq_univ (h : e.target = univ) :
+    Injective e.symm :=
+  e.symm.injective_of_source_eq_univ h
+
+lemma surjective_symm_of_source_eq_univ (h : e.source = univ) :
+    Surjective e.symm :=
+  e.symm.surjective_of_target_eq_univ h
+
 end PartialEquiv
 
 namespace Set

Mathlib/Tactic/Linter/DirectoryDependency.lean

@@ -583,6 +583,7 @@ def overrideAllowedImportDirs : NamePrefixRel := .ofArray #[
   (`Mathlib.Algebra.Notation, `Mathlib.Algebra.Notation),
   (`Mathlib.Deprecated, `Mathlib.Deprecated),
   (`Mathlib.Topology.Algebra, `Mathlib.Algebra),
+  (`Mathlib.Topology.Compactification, `Mathlib.Geometry.Manifold)
 ]
 
 end DirectoryDependency

Mathlib/Topology/Compactification/OnePoint/Sphere.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2025 Bjørn Kjos-Hanssen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bjørn Kjos-Hanssen, Oliver Nash
+-/
+import Mathlib.Topology.Compactification.OnePoint.Basic
+import Mathlib.Geometry.Manifold.Instances.Sphere
+
+/-!
+
+# One-point compactification of Euclidean space is homeomorphic to the sphere.
+
+-/
+
+open Function Metric Module Set Submodule
+
+noncomputable section
+
+/-- A homeomorphism from the one-point compactification of a hyperplane in Euclidean space to the
+sphere. -/
+def onePointHyperplaneHomeoUnitSphere
+    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+    {v : E} (hv : ‖v‖ = 1) :
+    OnePoint (ℝ ∙ v)ᗮ ≃ₜ sphere (0 : E) 1 :=
+  OnePoint.equivOfIsEmbeddingOfRangeEq _ _
+    (isOpenEmbedding_stereographic_symm hv).toIsEmbedding (range_stereographic_symm hv)
+
+/-- A homeomorphism from the one-point compactification of a finite-dimensional real vector space to
+the sphere. -/
+def onePointEquivSphereOfFinrankEq {ι V : Type*} [Fintype ι]
+    [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V]
+    [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] [T2Space V]
+    (h : finrank ℝ V + 1 = Fintype.card ι) :
+    OnePoint V ≃ₜ sphere (0 : EuclideanSpace ℝ ι) 1 := by
+  classical
+  have : Nonempty ι := Fintype.card_pos_iff.mp <| by omega
+  let v : EuclideanSpace ℝ ι := .single (Classical.arbitrary ι) 1
+  have hv : ‖v‖ = 1 := by simp [v]
+  have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
+  have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
+  have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
+  letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some
+  exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv