The unit sphere is simply connected above rank two

The unit sphere of a real normed space E with 2 < Module.rank ℝ E is simply connected; in particular Sⁿ is simply connected for 2 ≤ n.

The proof is the classical one, in the form that avoids any smoothing or simplicial approximation. A loop γ is compared with the radial projection of the piecewise-linear interpolation through the N + 1 values γ(k/N), where N is chosen so fine that ‖γ s - γ t‖ < 1 whenever |s - t| ≤ 1/N. That comparison loop is written as a single global formula rather than by gluing pieces: it is the radial projection to the sphere of

L t = ∑ k ≤ N, Λ k t • γ (k/N), Λ k t = max 0 (1 - |N * t - k|),

the piecewise linear interpolation of the nodes through the hat functions of the subdivision. Two facts about L do all the work. Since Λ k t ≠ 0 forces |N * t - k| < 1, every contributing node is within distance one of γ t. The nonnegative hat functions sum to one, so ‖L t - γ t‖ < 1; consequently the straight-line homotopy from γ t to L t never meets the origin, and its radial projection is a homotopy of loops on the sphere. Also Λ k t ≠ 0 forces k to be ⌊N t⌋ or ⌊N t⌋ + 1, so L t lies in the span of two of the nodes. A finite family of proper subspaces of E cannot cover E (Submodule.exists_forall_notMem_of_forall_ne_top), and the spans of two vectors are proper exactly because the rank exceeds two, so the projected loop omits a point of the sphere. Loops omitting a point are null-homotopic by TauCeti.homotopic_refl_of_notMem_range.

Rank two is genuinely the boundary: the circle is not simply connected.

Main declarations

• TauCeti.exists_homotopic_notMem_range: every loop on the unit sphere is homotopic to a loop that omits a point of the sphere.
• TauCeti.simplyConnectedSpace_sphere: the unit sphere of a real normed space of rank greater than two is simply connected.
• TauCeti.simplyConnectedSpace_sphere_euclideanSpace: the case of Sⁿ for 2 ≤ n.

References

This is the missing input to the π₁(RPⁿ) line of TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13: TauCeti.RealProjectiveSpace.fundamentalGroupMulEquiv and its corollaries were stated against a simply connected covering sphere, and this file discharges that hypothesis. Hatcher, Algebraic Topology, Corollary 1.15 gives the classical theorem; the hat-function interpolation and finite-span avoidance argument used here is this repository's own arrangement.

Concurrent work by Joël Riou in mathlib4#28246 formalizes the same theorem upstream by a different route. This implementation is independent; if that pull request lands, a future Mathlib bump should replace this file's theorem with the upstream API. No Mathlib code is vendored.

theorem TauCeti.exists_homotopic_notMem_range {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 2 < Module.rank ℝ E) {x : ↑(Metric.sphere 0 1)} (γ : Path x x) : ∃ (γ' : Path x x), γ.Homotopic γ' ∧ ∃ (p : ↑(Metric.sphere 0 1)), p ∉ Set.range ⇑γ'

Every loop on the unit sphere of a real normed space of rank greater than two is homotopic to a loop that omits a point of the sphere. The comparison loop is the radial projection of the piecewise linear interpolation of finitely many values of the loop, and the point it omits is obtained by avoiding the finitely many planes those values span.

theorem TauCeti.simplyConnectedSpace_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : 2 < Module.rank ℝ E) : SimplyConnectedSpace ↑(Metric.sphere 0 1)

The unit sphere of a real normed space of rank greater than two is simply connected. Every loop is homotopic to one omitting a point, and the punctured sphere contracts to the antipode of the omitted point.

theorem TauCeti.simplyConnectedSpace_sphere_euclideanSpace {n : ℕ} (hn : 2 ≤ n) : SimplyConnectedSpace ↑(Metric.sphere 0 1)

The n-sphere is simply connected for 2 ≤ n.