Curvature of the round sphere

The unit sphere Sⁿ of a real inner product space E of dimension n + 1, with its round metric, has constant sectional curvature 1: its curvature tensor is

R(u, v) w = ⟪v, w⟫ u - ⟪u, w⟫ v,

its Ricci tensor is n - 1 times the metric, and its scalar curvature is n (n - 1).

The computation uses the gradients X_a of the height functions p ↦ ⟪a, p⟫, for a ∈ E. In ambient coordinates X_a p = a - ⟪a, p⟫ p is the tangential part of a, so these fields span every tangent space. The Gauss formula for the isometric inclusion Sⁿ → E gives ∇_{X_a} X_b = -⟪b, p⟫ X_a, and the differential of the inclusion gives the bracket [X_a, X_b] = ⟪a, p⟫ X_b - ⟪b, p⟫ X_a; the curvature of these fields follows by the Leibniz rule.

Main results

• TauCeti.curvatureTensor_sphere: the curvature tensor of the round sphere.
• TauCeti.hasConstantSectionalCurvature_sphere: the round sphere has constant sectional curvature 1.
• TauCeti.ricciTensor_sphere: the Ricci tensor of the round n-sphere is n - 1 times the metric.
• TauCeti.scalarCurvature_sphere: the scalar curvature of the round n-sphere is n (n - 1).
• TauCeti.scalarCurvature_sphereRoundMetric_ofLE and TauCeti.isConstantCurvatureTensor_sphereRoundMetric_ofLE: the scalar curvature and the constant-curvature tensor for the round metric regarded as a smooth metric.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Theorem 8.34 (the round sphere has constant sectional curvature) and Theorem 8.2 (the Gauss formula).

@[simp]

theorem TauCeti.curvatureTensor_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (p : ↑(Metric.sphere 0 1)) (u v w : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) p) : ((((CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)).curvatureTensor p) u) v) w = inner ℝ v w • u - inner ℝ u w • v

The round sphere has the constant-curvature tensor with parameter 1: R(u, v) w = ⟪v, w⟫ u - ⟪u, w⟫ v.

theorem TauCeti.hasConstantSectionalCurvature_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : (CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)).HasConstantSectionalCurvature ⋯ 1

The round sphere has constant sectional curvature 1.

@[simp]

theorem TauCeti.ricciTensor_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (p : ↑(Metric.sphere 0 1)) (u v : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) p) : (((CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)).ricciTensor p) u) v = (↑n - 1) * inner ℝ u v

The Ricci tensor of the round n-sphere is n - 1 times the round metric.

@[simp]

theorem TauCeti.scalarCurvature_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (p : ↑(Metric.sphere 0 1)) : (CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)).scalarCurvature p = ↑n * (↑n - 1)

The scalar curvature of the round n-sphere is n (n - 1).

@[simp]

theorem TauCeti.scalarCurvature_sphereRoundMetric_ofLE {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (p : ↑(Metric.sphere 0 1)) : (sphereRoundMetric.ofLE ⋯).scalarCurvature p = ↑n * (↑n - 1)

The scalar curvature of the round metric on the unit n-sphere, regarded as a smooth metric, is n (n - 1).

theorem TauCeti.isConstantCurvatureTensor_sphereRoundMetric_ofLE {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : (sphereRoundMetric.ofLE ⋯).IsConstantCurvatureTensor 1

The round metric on the unit sphere, regarded as a smooth metric, has the constant-curvature tensor with parameter 1.