The punctured unit sphere

Removing a point p from the unit sphere of a real normed space leaves a set that can be swept onto the antipode -p: for x ≠ p on the sphere the straight segment from x to -p never meets the origin, so normalising it gives a contraction of the punctured sphere inside the sphere. Consequently the inclusion of the punctured sphere into the sphere is null-homotopic, and a loop on the sphere that misses even a single point is null-homotopic.

This is the easy half of the computation of π₁(Sⁿ): the work left over is to homotope an arbitrary loop off a point, which is done in TauCeti.AlgebraicTopology.Sphere.SimplyConnected.

Main declarations

• Path.homotopic_of_segment_ne_zero: radial projection of a straight-line homotopy between sphere paths.
• TauCeti.contractibleSpace_sphere_compl_singleton: the sphere minus one point is contractible.
• TauCeti.compl_singleton_union_compl_singleton_neg: the complements of two antipodal points cover the sphere.
• TauCeti.nullhomotopic_inclusion_sphere_compl_singleton: the inclusion of the sphere minus a point into the sphere is null-homotopic.
• Path.homotopic_refl_of_notMem_range: a loop on the unit sphere omitting a point of the sphere is null-homotopic.

References

The contraction of a punctured sphere onto the antipode of the puncture is the standard one, as in Hatcher, Algebraic Topology, Section 1.1.

theorem Path.homotopic_of_segment_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ↑(Metric.sphere 0 1)} (γ γ' : Path a b) (f : ↑unitInterval → E) (hf : Continuous f) (hγ' : ∀ (t : ↑unitInterval), ↑(γ' t) = NormedSpace.normalize (f t)) (hf_zero : f 0 = ↑a) (hf_one : f 1 = ↑b) (h : ∀ (z : ↑unitInterval × ↑unitInterval), (1 - ↑z.1) • ↑(γ z.2) + ↑z.1 • f z.2 ≠ 0) : γ.Homotopic γ'

A path in the unit sphere is homotopic to the radial projection of a continuous comparison map when every point of their pointwise straight-line homotopy avoids the origin and the comparison map itself takes the source and target values at the two endpoints.

theorem TauCeti.contractibleSpace_sphere_compl_singleton {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : ContractibleSpace ↑{p}ᶜ

The unit sphere minus one point is contractible. Radial projection of the segment towards the antipode of the deleted point gives a contraction that stays inside the punctured sphere.

theorem TauCeti.compl_singleton_union_compl_singleton_neg {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : {p}ᶜ ∪ {-p}ᶜ = Set.univ

The complements of two antipodal points cover the unit sphere.

theorem TauCeti.nullhomotopic_inclusion_sphere_compl_singleton {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : { toFun := Subtype.val, continuous_toFun := ⋯ }.Nullhomotopic

The inclusion of the unit sphere minus one point into the sphere is null-homotopic.

theorem Path.homotopic_refl_of_notMem_range {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x : ↑(Metric.sphere 0 1)} (γ : Path x x) {p : ↑(Metric.sphere 0 1)} (hp : p ∉ Set.range ⇑γ) : γ.Homotopic (refl x)

A loop on the unit sphere that omits a point of the sphere is null-homotopic. The loop runs in the punctured sphere, whose inclusion into the sphere is null-homotopic.