The round sphere of radius r

The round n-sphere Sⁿ(r) of radius r > 0 is the unit sphere Sⁿ of a real inner product space E of dimension n + 1, carrying r² times its round metric. This is the metric induced by the embedding p ↦ r • p of the unit sphere into E, whose image is the sphere of radius r.

Since the unit sphere has scalar curvature n (n - 1) and multiplying a metric by c > 0 multiplies its scalar curvature by c⁻¹, the scalar curvature of Sⁿ(r) is n (n - 1) / r². Hence Sⁿ(r) has positive scalar curvature exactly when n ≥ 2: the two-point sphere S⁰ and the circle S¹ are flat.

Likewise the unit sphere has constant sectional curvature 1, and multiplying a metric by c > 0 multiplies its sectional curvature by c⁻¹, so Sⁿ(r) has constant sectional curvature 1 / r².

Main definitions

• TauCeti.sphereRoundMetricOfRadius: the round metric of radius r on the unit sphere.

Main statements

• TauCeti.sphereRoundMetricOfRadius_inner_eq_inner_mvfderiv_smul: the round metric of radius r is induced by the embedding p ↦ r • p.
• TauCeti.isConstantCurvatureTensor_sphereRoundMetricOfRadius and TauCeti.hasConstantSectionalCurvature_sphereRoundMetricOfRadius: the round sphere of radius r has constant sectional curvature 1 / r².
• TauCeti.scalarCurvature_sphereRoundMetricOfRadius: the round n-sphere of radius r has scalar curvature n (n - 1) / r².
• TauCeti.hasPositiveScalarCurvature_sphereRoundMetricOfRadius_iff: the round n-sphere of radius r has positive scalar curvature if and only if 2 ≤ n.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 3 (the round sphere of radius R) and Chapter 8 (its curvature).

noncomputable def TauCeti.sphereRoundMetricOfRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (r : ℝ) (hr : 0 < r) : Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) (EuclideanSpace ℝ (Fin n)) fun (x : ↑(Metric.sphere 0 1)) => TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x

The round metric of radius r > 0 on the unit n-sphere: r² times the round metric. It is the metric induced by the embedding p ↦ r • p onto the sphere of radius r; see sphereRoundMetricOfRadius_inner_eq_inner_mvfderiv_smul.

@[simp]

theorem TauCeti.sphereRoundMetricOfRadius_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {r : ℝ} (hr : 0 < r) (p : ↑(Metric.sphere 0 1)) (v w : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) p) : (((sphereRoundMetricOfRadius r hr).inner p) v) w = r ^ 2 * inner ℝ v w

The round metric of radius r is r² times the round inner product.

theorem TauCeti.sphereRoundMetricOfRadius_inner_eq_inner_mvfderiv_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {r : ℝ} (hr : 0 < r) (p : ↑(Metric.sphere 0 1)) (v w : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) p) : (((sphereRoundMetricOfRadius r hr).inner p) v) w = inner ℝ (((d% fun (q : ↑(Metric.sphere 0 1)) => r • ↑q) p) v) (((d% fun (q : ↑(Metric.sphere 0 1)) => r • ↑q) p) w)

The round metric of radius r is the metric induced by the embedding p ↦ r • p of the unit sphere into E, whose image is the sphere of radius r.

theorem TauCeti.isConstantCurvatureTensor_sphereRoundMetricOfRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {r : ℝ} (hr : 0 < r) : (sphereRoundMetricOfRadius r hr).IsConstantCurvatureTensor (r ^ 2)⁻¹

The round sphere of radius r has the constant-curvature tensor with parameter 1 / r²: R(w, u) v = r⁻² (⟪u, v⟫ w - ⟪w, v⟫ u) for its metric ⟪·, ·⟫.

theorem TauCeti.hasConstantSectionalCurvature_sphereRoundMetricOfRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {r : ℝ} (hr : 0 < r) : (CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)).HasConstantSectionalCurvature ⋯ (r ^ 2)⁻¹

Sectional curvature of the round sphere. The round sphere of radius r has constant sectional curvature 1 / r².

@[simp]

theorem TauCeti.scalarCurvature_sphereRoundMetricOfRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {r : ℝ} (hr : 0 < r) (p : ↑(Metric.sphere 0 1)) : (sphereRoundMetricOfRadius r hr).scalarCurvature p = ↑n * (↑n - 1) / r ^ 2

Scalar curvature of the round sphere. The round n-sphere of radius r has scalar curvature n (n - 1) / r².

@[simp]

theorem TauCeti.hasPositiveScalarCurvature_sphereRoundMetricOfRadius_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {r : ℝ} (hr : 0 < r) : (sphereRoundMetricOfRadius r hr).HasPositiveScalarCurvature ↔ 2 ≤ n

The round n-sphere of radius r has positive scalar curvature if and only if 2 ≤ n.

theorem TauCeti.hasPositiveScalarCurvature_sphereRoundMetricOfRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {r : ℝ} (hr : 0 < r) (hn : 2 ≤ n) : (sphereRoundMetricOfRadius r hr).HasPositiveScalarCurvature

The round n-sphere of every radius has positive scalar curvature when 2 ≤ n.