Closed balls as hemispheres of great spheres

Let ι : F →ₗᵢ[ℝ] E be a linear isometry of real inner product spaces and v a unit vector of E orthogonal to the range of ι. Inverse stereographic projection from v (Mathlib's stereoInvFun) carries the orthogonal complement vᗮ onto the unit sphere minus v, and the sphere of radius 2 in vᗮ onto the great sphere vᗮ ∩ Sⁿ, by w ↦ w / 2. So

LinearIsometry.closedBallHemisphereMap ι v x = stereoInvFun (2 ι x),

which is (2 ι x + (‖x‖² - 1) v) / (1 + ‖x‖²),

maps the closed unit ball of F onto the closed hemisphere centred at -v of the great sphere cut out by ι F ⊕ ℝ v, and agrees with ι on the unit sphere of F (LinearIsometry.closedBallHemisphereMap_apply_of_norm_eq_one). For F = ℂ this is a smooth disc in the unit sphere bounded by the great circle ι S¹, such as a Seifert surface of the unknot.

The hemispheres of TauCeti.prodHemisphereGraph and TauCeti.hemisphereHomeomorph are graphs of u ↦ √(1 - ‖u‖²), which is not differentiable on the boundary sphere; inverse stereographic projection is analytic up to the boundary.

The map is a smooth embedding of the closed ball, a manifold with boundary, into the sphere (LinearIsometry.isSmoothEmbedding_closedBallHemisphereMap). Read in a chart TauCeti.closedBallChart φ of the ball, an inversion y ↦ inversion (-e₀) √2 y of the model half-space followed by φ.symm, and in the stereographic chart from v, it is y ↦ 2 N (inversion (-e₀) √2 y) for the linear isometry N of model spaces through which the stereographic chart reads ι φ.symm. Composing that chart of the sphere with the inverse rescaled inversion z ↦ inversion (-e₀) √2 (z / 2) on the first factor of the decomposition N.prodOrthogonalRangeEquiv gives a chart of the sphere in which the map reads as the inclusion y ↦ (y, 0), so it is an immersion at every point, including on the boundary sphere.

Main definitions

• LinearIsometry.closedBallHemisphereMap ι v: the map x ↦ stereoInvFun (2 ι x) from the closed unit ball of F to the unit sphere of E.

Main results

• LinearIsometry.coe_closedBallHemisphereMap_apply: the formula of the hemisphere map.
• LinearIsometry.closedBallHemisphereMap_apply_of_norm_eq_one: on the unit sphere of F it is ι.
• LinearIsometry.isSmoothEmbedding_closedBallHemisphereMap: it is a smooth embedding of manifolds with boundary, at every order of differentiability.

Rescaled inversions

noncomputable def LinearIsometry.closedBallHemisphereMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (ι : F →ₗᵢ[ℝ] E) (v : ↑(Metric.sphere 0 1)) (hv : ∀ (x : F), inner ℝ (↑v) (ι x) = 0) : ↑(Metric.closedBall 0 1) → ↑(Metric.sphere 0 1)

The hemisphere map of a linear isometry ι : F →ₗᵢ[ℝ] E and a unit vector v orthogonal to its range: inverse stereographic projection from v of 2 ι x, for x in the closed unit ball of F. It maps the closed ball onto the closed hemisphere centred at -v of the great sphere cut out by ι F ⊕ ℝ v, and is ι on the unit sphere of F.

@[simp]

theorem LinearIsometry.coe_closedBallHemisphereMap_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (ι : F →ₗᵢ[ℝ] E) {v : ↑(Metric.sphere 0 1)} (hv : ∀ (x : F), inner ℝ (↑v) (ι x) = 0) (x : ↑(Metric.closedBall 0 1)) : ↑(ι.closedBallHemisphereMap v hv x) = (1 + ‖↑x‖ ^ 2)⁻¹ • (2 • ι ↑x + (‖↑x‖ ^ 2 - 1) • ↑v)

The hemisphere map sends x to (2 ι x + (‖x‖² - 1) v) / (1 + ‖x‖²).

theorem LinearIsometry.closedBallHemisphereMap_apply_of_norm_eq_one {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (ι : F →ₗᵢ[ℝ] E) {v : ↑(Metric.sphere 0 1)} (hv : ∀ (x : F), inner ℝ (↑v) (ι x) = 0) {x : ↑(Metric.closedBall 0 1)} (hx : ‖↑x‖ = 1) : ↑(ι.closedBallHemisphereMap v hv x) = ι ↑x

On the boundary sphere the hemisphere map is ι.

theorem LinearIsometry.continuous_closedBallHemisphereMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (ι : F →ₗᵢ[ℝ] E) {v : ↑(Metric.sphere 0 1)} (hv : ∀ (x : F), inner ℝ (↑v) (ι x) = 0) : Continuous (ι.closedBallHemisphereMap v hv)

theorem LinearIsometry.closedBallHemisphereMap_injective {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (ι : F →ₗᵢ[ℝ] E) {v : ↑(Metric.sphere 0 1)} (hv : ∀ (x : F), inner ℝ (↑v) (ι x) = 0) : Function.Injective (ι.closedBallHemisphereMap v hv)

theorem LinearIsometry.isEmbedding_closedBallHemisphereMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (ι : F →ₗᵢ[ℝ] E) {v : ↑(Metric.sphere 0 1)} (hv : ∀ (x : F), inner ℝ (↑v) (ι x) = 0) [FiniteDimensional ℝ F] : Topology.IsEmbedding (ι.closedBallHemisphereMap v hv)

The hemisphere map is a topological embedding: it is a continuous injection of the compact closed ball into the Hausdorff sphere.

The hemisphere map is an immersion

theorem LinearIsometry.isImmersionAt_closedBallHemisphereMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {m : ℕ} [NeZero m] [Fact (Module.finrank ℝ F = m)] (ι : F →ₗᵢ[ℝ] E) {v : ↑(Metric.sphere 0 1)} (hv : ∀ (x : F), inner ℝ (↑v) (ι x) = 0) {k : WithTop ℕ∞} (x : ↑(Metric.closedBall 0 1)) : Manifold.IsImmersionAt (modelWithCornersEuclideanHalfSpace m) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) k (ι.closedBallHemisphereMap v hv) x

The hemisphere map is an immersion at every point, including on the boundary sphere of the ball. In a chart closedBallChart φ of the ball and the stereographic chart from v followed by the inverse of the rescaled inversion on the first factor of N.prodOrthogonalRangeEquiv, it reads as the inclusion y ↦ (y, 0).

theorem LinearIsometry.isImmersion_closedBallHemisphereMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {m : ℕ} [NeZero m] [Fact (Module.finrank ℝ F = m)] (ι : F →ₗᵢ[ℝ] E) {v : ↑(Metric.sphere 0 1)} (hv : ∀ (x : F), inner ℝ (↑v) (ι x) = 0) {k : WithTop ℕ∞} : Manifold.IsImmersion (modelWithCornersEuclideanHalfSpace m) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) k (ι.closedBallHemisphereMap v hv)

The hemisphere map is a C^k immersion.

theorem LinearIsometry.isSmoothEmbedding_closedBallHemisphereMap {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {m : ℕ} [NeZero m] [Fact (Module.finrank ℝ F = m)] (ι : F →ₗᵢ[ℝ] E) {v : ↑(Metric.sphere 0 1)} (hv : ∀ (x : F), inner ℝ (↑v) (ι x) = 0) {k : WithTop ℕ∞} : Manifold.IsSmoothEmbedding (modelWithCornersEuclideanHalfSpace m) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) k (ι.closedBallHemisphereMap v hv)

The hemisphere map is a smooth embedding of the closed unit ball of F, a manifold with boundary, into the unit sphere of E, at every order of differentiability.