Spheres are simply connected above rank two

Every sphere of nonnegative radius in a real normed space E with 2 < Module.rank ℝ E is simply connected; in particular Sⁿ is simply connected for 2 ≤ n. Spheres of positive radius are obtained from the unit sphere by dilation and translation; a sphere of radius zero is a singleton.

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 each two-vector span is proper because the rank exceeds two, so the projected loop omits a point of the sphere. Loops omitting a point are null-homotopic by Path.homotopic_refl_of_notMem_range.

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

Main declarations

• Path.exists_homotopic_notMem_range: every path on the unit sphere is homotopic to a path with the same endpoints that omits a point of the sphere.
• TauCeti.simplyConnectedSpace_sphere: spheres of nonnegative radius in real normed spaces of rank greater than two are simply connected.
• TauCeti.simplyConnectedSpace_sphere_euclideanSpace: the case of Sⁿ for 2 ≤ n.
• TauCeti.simplyConnectedSpace_sphere_euclideanSpace_complex: the case of the unit sphere S²ᵏ⁺¹ of ℂᵏ⁺¹ for 1 ≤ k.

References

Simple connectivity of the covering sphere gives the fundamental groups of real projective spaces and lens spaces through their covering maps. 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.

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

Every path on the unit sphere of a real normed space of rank greater than two is homotopic, with fixed endpoints, to a path that omits a point of the sphere.

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

Every sphere of nonnegative radius in a real normed space of rank greater than two is simply connected.

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

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

theorem TauCeti.simplyConnectedSpace_sphere_euclideanSpace_complex {k : ℕ} (hk : 1 ≤ k) : SimplyConnectedSpace ↑(Metric.sphere 0 1)

The unit sphere S²ᵏ⁺¹ of ℂᵏ⁺¹ is simply connected for 1 ≤ k.