The equator of a unit sphere

Removing from the unit sphere of a real inner product space E the points of a subspace K (with an orthogonal projection) leaves a space homotopy equivalent to the unit sphere of the orthogonal complement Kᗮ. One map is the inclusion of that sphere; the other is radial projection of the orthogonal projection onto Kᗮ. Retracting the sphere of Kᗮ this way fixes it, and the deformation of the complement normalizes the segment from a point to its orthogonal projection onto Kᗮ, which never meets K.

For the line K = ℝ ∙ p through a unit vector p, the complement is the sphere minus p and -p, and the sphere of Kᗮ is the equator. Together with the contractibility of a sphere minus one point, this is the geometric input to the Mayer–Vietoris computation of the homology of spheres. For a plane K in a four-dimensional space, the complement is that of a great circle in the three-sphere, and the sphere of Kᗮ is the complementary great circle.

When E is two-dimensional, the equator is a zero-sphere, so the circle minus p and -p consists of two open arcs: for any point x of it, the path components of x and of -x are distinct and are the only two path components.

Main declarations

• TauCeti.sphereDiffHomotopyEquiv: the unit sphere minus the points of K is homotopy equivalent to the unit sphere of Kᗮ, with TauCeti.coe_sphereDiffHomotopyEquiv_apply and TauCeti.coe_sphereDiffHomotopyEquiv_symm_apply computing both maps.
• TauCeti.equatorHomotopyEquiv: the unit sphere minus p and -p is homotopy equivalent to the unit sphere of (ℝ ∙ p)ᗮ, with TauCeti.coe_equatorHomotopyEquiv_apply and TauCeti.coe_equatorHomotopyEquiv_symm_apply computing both maps.
• TauCeti.zerothHomotopy_mk_neg_ne_of_finrank_eq_two and TauCeti.zerothHomotopy_mk_eq_or_eq_neg_of_finrank_eq_two: in dimension two, the circle minus p and -p has exactly two path components, those of x and of -x.

References

This is the deformation retraction of Sⁿ ∖ {±p} onto the equator Sⁿ⁻¹ used in Hatcher, Algebraic Topology, Section 2.2, to compute the homology of spheres.

theorem TauCeti.neg_mem_compl_singleton_inter_compl_singleton_neg {E : Type u_1} [SeminormedAddCommGroup E] {p x : ↑(Metric.sphere 0 1)} (hx : x ∈ {p}ᶜ ∩ {-p}ᶜ) : -x ∈ {p}ᶜ ∩ {-p}ᶜ

The unit sphere minus two antipodal points is invariant under the antipodal map.

The complement of a subspace in the unit sphere

noncomputable def TauCeti.sphereDiffHomotopyEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Submodule ℝ E) [K.HasOrthogonalProjection] : ContinuousMap.HomotopyEquiv ↑{x : ↑(Metric.sphere 0 1) | ↑x ∉ K} ↑(Metric.sphere 0 1)

The unit sphere minus a subspace is homotopy equivalent to the unit sphere of its orthogonal complement. For a subspace K of a real inner product space E with an orthogonal projection, the points of the unit sphere of E outside K form a space homotopy equivalent to the unit sphere of Kᗮ: radial projection of the orthogonal projection onto Kᗮ is a homotopy inverse of the inclusion.

Equations

• TauCeti.sphereDiffHomotopyEquiv K = { toFun := TauCeti.toSphereOrthogonal✝ K, invFun := TauCeti.ofSphereOrthogonal✝ K, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.coe_sphereDiffHomotopyEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Submodule ℝ E) [K.HasOrthogonalProjection] (x : ↑{x : ↑(Metric.sphere 0 1) | ↑x ∉ K}) : ↑↑((sphereDiffHomotopyEquiv K).toFun x) = NormedSpace.normalize (Kᗮ.starProjection ↑↑x)

The homotopy equivalence TauCeti.sphereDiffHomotopyEquiv is radial projection of the orthogonal projection onto Kᗮ.

@[simp]

theorem TauCeti.coe_sphereDiffHomotopyEquiv_symm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (K : Submodule ℝ E) [K.HasOrthogonalProjection] (y : ↑(Metric.sphere 0 1)) : ↑↑((sphereDiffHomotopyEquiv K).symm.toFun y) = ↑↑y

The homotopy inverse of TauCeti.sphereDiffHomotopyEquiv is the inclusion of the unit sphere of Kᗮ.

The equator

noncomputable def TauCeti.equatorHomotopyEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : ContinuousMap.HomotopyEquiv ↑({p}ᶜ ∩ {-p}ᶜ) ↑(Metric.sphere 0 1)

The sphere minus two antipodal points is homotopy equivalent to the equator. For a point p of the unit sphere of a real inner product space E, the unit sphere minus p and -p is homotopy equivalent to the unit sphere of the orthogonal complement (ℝ ∙ p)ᗮ: radial projection of the orthogonal projection is a homotopy inverse of the inclusion.

Equations

• TauCeti.equatorHomotopyEquiv p = (Homeomorph.setCongr ⋯).toHomotopyEquiv.trans (TauCeti.sphereDiffHomotopyEquiv (ℝ ∙ ↑p))

@[simp]

theorem TauCeti.coe_equatorHomotopyEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (x : ↑({p}ᶜ ∩ {-p}ᶜ)) : ↑↑((equatorHomotopyEquiv p).toFun x) = NormedSpace.normalize ((ℝ ∙ ↑p)ᗮ.starProjection ↑↑x)

The homotopy equivalence TauCeti.equatorHomotopyEquiv is radial projection of the orthogonal projection onto (ℝ ∙ p)ᗮ.

@[simp]

theorem TauCeti.coe_equatorHomotopyEquiv_symm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (y : ↑(Metric.sphere 0 1)) : ↑↑((equatorHomotopyEquiv p).symm.toFun y) = ↑↑y

The homotopy inverse of TauCeti.equatorHomotopyEquiv is the inclusion of the equator.

theorem TauCeti.zerothHomotopy_mk_neg_ne_of_finrank_eq_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {p : ↑(Metric.sphere 0 1)} (hE : Module.finrank ℝ E = 2) {x : ↑(Metric.sphere 0 1)} (hx : x ∈ {p}ᶜ ∩ {-p}ᶜ) : ZerothHomotopy.mk ⟨-x, ⋯⟩ ≠ ZerothHomotopy.mk ⟨x, hx⟩

The two arcs of a punctured circle are distinct. On the unit circle of a two-dimensional real inner product space minus two antipodal points p and -p, a point x and its antipode -x lie in distinct path components.

theorem TauCeti.zerothHomotopy_mk_eq_or_eq_neg_of_finrank_eq_two {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {p : ↑(Metric.sphere 0 1)} (hE : Module.finrank ℝ E = 2) {x : ↑(Metric.sphere 0 1)} (hx : x ∈ {p}ᶜ ∩ {-p}ᶜ) (y : ↑({p}ᶜ ∩ {-p}ᶜ)) : ZerothHomotopy.mk y = ZerothHomotopy.mk ⟨x, hx⟩ ∨ ZerothHomotopy.mk y = ZerothHomotopy.mk ⟨-x, ⋯⟩

A punctured circle has no third arc. On the unit circle of a two-dimensional real inner product space minus two antipodal points p and -p, every point lies in the path component of x or in that of -x.