The round metric in stereographic coordinates

Let v be a unit vector of a real inner product space E of dimension n + 1. Mathlib's stereographic projection stereographic' n v from v is a chart of the unit sphere Sⁿ with values in ℝⁿ; it projects onto the hyperplane orthogonal to v through -v, so its inverse is

σ⁻¹(w) = (‖w‖² + 4)⁻¹ (4 w + (‖w‖² - 4) v)

(stereoInvFunAux), up to the linear isometry of (ℝ ∙ v)ᗮ with ℝⁿ used by stereographic'. This file proves that σ⁻¹ is conformal, and computes its conformal factor: for w, a, b orthogonal to v,

⟪dσ⁻¹_w a, dσ⁻¹_w b⟫ = (4 / (‖w‖² + 4))² ⟪a, b⟫.

Equivalently, the round metric of the sphere (TauCeti.sphereRoundMetric) reads in the stereographic chart as (4 / (‖y‖² + 4))² times the Euclidean metric of ℝⁿ. For the more common projection onto the equatorial hyperplane, which is y ↦ σ⁻¹(2 y), the factor is the familiar (2 / (1 + ‖y‖²))².

Main results

• TauCeti.fderiv_stereoInvFunAux_apply: the differential of σ⁻¹.
• TauCeti.inner_fderiv_stereoInvFunAux: the conformal factor of σ⁻¹ on the hyperplane orthogonal to v.
• TauCeti.inner_fderiv_stereoInvFunAux_two_smul: the conformal factor (2 / (1 + ‖y‖²))² of y ↦ σ⁻¹ (2 J y) for a linear isometry J into that hyperplane.
• TauCeti.inner_mfderiv_stereographic'_symm: the round metric pulled back along the inverse of the stereographic chart stereographic' n v.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 3 (stereographic coordinates on the round sphere).
• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), 37–91, Section 3.

theorem TauCeti.fderiv_stereoInvFunAux_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v w a : E) : (fderiv ℝ (stereoInvFunAux v) w) a = (‖w‖ ^ 2 + 4)⁻¹ • (4 • a + (2 * inner ℝ w a) • v) - (2 * inner ℝ w a / (‖w‖ ^ 2 + 4) ^ 2) • (4 • w + (‖w‖ ^ 2 - 4) • v)

The differential at w of the inverse stereoInvFunAux v of stereographic projection, which is w ↦ (‖w‖² + 4)⁻¹ (4 w + (‖w‖² - 4) v).

theorem TauCeti.inner_fderiv_stereoInvFunAux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1) {w a b : E} (hw : w ∈ (ℝ ∙ v)ᗮ) (ha : a ∈ (ℝ ∙ v)ᗮ) (hb : b ∈ (ℝ ∙ v)ᗮ) : inner ℝ ((fderiv ℝ (stereoInvFunAux v) w) a) ((fderiv ℝ (stereoInvFunAux v) w) b) = (4 / (‖w‖ ^ 2 + 4)) ^ 2 * inner ℝ a b

Inverse stereographic projection is conformal. For a unit vector v and vectors w, a, b orthogonal to v, the differential of σ⁻¹ = stereoInvFunAux v at w satisfies ⟪dσ⁻¹_w a, dσ⁻¹_w b⟫ = (4 / (‖w‖² + 4))² ⟪a, b⟫.

theorem TauCeti.inner_fderiv_stereoInvFunAux_two_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {v : E} {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (hv : ‖v‖ = 1) (J : F →ₗᵢ[ℝ] E) (hJ : ∀ (c : F), J c ∈ (ℝ ∙ v)ᗮ) (y a b : F) : inner ℝ ((fderiv ℝ (fun (w : F) => stereoInvFunAux v (2 • J w)) y) a) ((fderiv ℝ (fun (w : F) => stereoInvFunAux v (2 • J w)) y) b) = (2 / (1 + ‖y‖ ^ 2)) ^ 2 * inner ℝ a b

The conformal factor of equatorial stereographic coordinates. For a unit vector v and a linear isometry J of a real inner product space F into the hyperplane orthogonal to v, the map y ↦ σ⁻¹ (2 J y) satisfies ⟪dσ⁻¹ a, dσ⁻¹ b⟫ = (2 / (1 + ‖y‖²))² ⟪a, b⟫ at y.

theorem TauCeti.inner_mfderiv_stereographic'_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) (y a b : EuclideanSpace ℝ (Fin n)) : inner ℝ ((mfderiv% ↑(stereographic' n v).symm y) a) ((mfderiv% ↑(stereographic' n v).symm y) b) = (4 / (‖y‖ ^ 2 + 4)) ^ 2 * inner ℝ a b

The round metric in stereographic coordinates. Pulled back along the inverse of the stereographic chart stereographic' n v of the unit sphere, the round metric is (4 / (‖y‖² + 4))² times the Euclidean metric of ℝⁿ at y.