Euclidean space is flat

A finite-dimensional real inner-product space F, with its standard Riemannian metric, has vanishing curvature: its Levi-Civita connection is the ordinary Fréchet derivative, so constant vector fields are parallel, and evaluating the curvature operator on constant fields gives 0. Consequently the Ricci tensor and the scalar curvature of the Euclidean metric vanish too.

This is the flat model of every curvature computation: for instance, on Euclidean space the conformal Laplacian aₙ Δ⁺ + Scal of the Yamabe problem reduces to aₙ Δ⁺.

Main results

• TauCeti.Manifold.curvatureTensor_leviCivitaConnection_model_space: the curvature tensor of the Euclidean metric vanishes.
• TauCeti.Manifold.ricciTensor_leviCivitaConnection_model_space and TauCeti.Manifold.scalarCurvature_leviCivitaConnection_model_space: so do its Ricci tensor and scalar curvature.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7 (flat metrics and the curvature of Euclidean space).

@[simp]

theorem TauCeti.Manifold.curvatureTensor_leviCivitaConnection_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (x : F) : (CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ F) F).curvatureTensor x = 0

Euclidean space is flat: the curvature tensor of the standard Riemannian metric on a finite-dimensional real inner-product space vanishes.

theorem TauCeti.Manifold.ricciTensor_leviCivitaConnection_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (x : F) : (CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ F) F).ricciTensor x = 0

The Ricci tensor of the standard Riemannian metric on a finite-dimensional real inner-product space vanishes.

@[simp]

theorem TauCeti.Manifold.scalarCurvature_leviCivitaConnection_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (x : F) : (CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ F) F).scalarCurvature x = 0

The scalar curvature of the standard Riemannian metric on a finite-dimensional real inner-product space vanishes.