Curvature and the Laplacian under constant rescaling of a metric

Let g be a Riemannian metric on M and c a positive constant, and let c g be the rescaled metric Bundle.ContMDiffRiemannianMetric.rescale by the constant function c. The Koszul formula is homogeneous of degree one in the metric when c is constant, so g and c g have the same Levi-Civita connection, and hence the same (1,3) curvature tensor and the same Ricci tensor. Scalar curvature is the metric trace of the Ricci tensor, and the trace for c g is c⁻¹ times the trace for g, so

Scal(c g) = c⁻¹ Scal(g).

Sectional curvature is the quotient ⟪R(u, v) v, u⟫ / (|u|²|v|² - ⟪u, v⟫²), whose numerator scales by c and whose denominator scales by c², so K(c g) = c⁻¹ K(g). Hence c g has constant sectional curvature k exactly when g has constant sectional curvature c k; for example the round sphere of radius r has sectional curvature 1 / r².

The gradient of a function is the dual of its differential through the metric, so grad_{c g} f = c⁻¹ grad_g f; since the Levi-Civita connections agree, the Laplace–Beltrami operator Δ = div ∘ grad scales in the same way, Δ_{c g} = c⁻¹ Δ_g.

Both metrics are installed in turn as the RiemannianBundle instance of the tangent bundle of M. Connections and curvature tensors do not depend on the metric, so they are compared directly on M. Mathlib's CovariantDerivative.leviCivitaConnection is unconstrained on vector fields which are not differentiable at the point, so the two Levi-Civita connections are compared on differentiable fields; this determines the curvature tensor.

Main results

• Bundle.ContMDiffRiemannianMetric.isMetricCompatible_rescale_const_iff: a connection is compatible with c g exactly when it is compatible with g.
• Bundle.ContMDiffRiemannianMetric.isLeviCivitaConnection_rescale_const_iff: a connection is Levi-Civita for c g exactly when it is Levi-Civita for g.
• Bundle.ContMDiffRiemannianMetric.leviCivitaConnection_rescale_const_apply: the Levi-Civita connections of c g and g agree on differentiable vector fields.
• Bundle.ContMDiffRiemannianMetric.curvatureTensor_leviCivitaConnection_rescale_const and Bundle.ContMDiffRiemannianMetric.ricciTensor_leviCivitaConnection_rescale_const: the curvature and Ricci tensors of c g and g coincide.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale_const: Scal(c g) = c⁻¹ Scal(g).
• Bundle.ContMDiffRiemannianMetric.sectionalCurvature_leviCivitaConnection_rescale_const: K(c g) = c⁻¹ K(g).
• Bundle.ContMDiffRiemannianMetric.isConstantCurvatureTensor_rescale_const_iff and its sectional-curvature form hasConstantSectionalCurvature_leviCivitaConnection_rescale_const_iff: c g has constant curvature k exactly when g has constant curvature c k.
• Bundle.ContMDiffRiemannianMetric.mgradient_rescale_const and Bundle.ContMDiffRiemannianMetric.laplaceBeltrami_rescale_const: grad_{c g} = c⁻¹ grad_g and Δ_{c g} = c⁻¹ Δ_g.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 5 (the Koszul formula) and Chapter 7 (curvature conventions).
• M. Gromov, H. B. Lawson, The classification of simply connected manifolds of positive scalar curvature, Ann. of Math. 111 (1980), 423–434.

theorem Bundle.ContMDiffRiemannianMetric.isMetricCompatible_rescale_const_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (TotalSpace F V)] [(x : M) → TopologicalSpace (V x)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle 1 F V I] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric I n F V) (hn : 1 ≤ n) {c : ℝ} (hc : 0 < c) (cov : CovariantDerivative I F V) : cov.IsMetricCompatible ↔ cov.IsMetricCompatible

Multiplying a C¹ bundle metric by a positive constant does not change which connections are compatible with it.

theorem Bundle.ContMDiffRiemannianMetric.isLeviCivitaConnection_rescale_const_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (hn : 1 ≤ n) {c : ℝ} (hc : 0 < c) (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) : CovariantDerivative.IsLeviCivitaConnection I cov ↔ CovariantDerivative.IsLeviCivitaConnection I cov

Multiplying a C¹ metric by a positive constant does not change which connections are Levi-Civita connections.

theorem Bundle.ContMDiffRiemannianMetric.leviCivitaConnection_rescale_const_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (hn : 1 ≤ n) {c : ℝ} (hc : 0 < c) {Y : (x : M) → TangentSpace I x} {x : M} (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) : ↑(CovariantDerivative.leviCivitaConnection I M) Y x = ↑(CovariantDerivative.leviCivitaConnection I M) Y x

The Levi-Civita connections of a C¹ metric and of a positive constant multiple of it agree on every vector field differentiable at the point.

theorem Bundle.ContMDiffRiemannianMetric.mgradient_rescale_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I 1 M] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) {c : ℝ} (hc : 0 < c) (f : M → ℝ) (x : M) : TauCeti.Manifold.mgradient I f x = c⁻¹ • TauCeti.Manifold.mgradient I f x

Multiplying a metric by a positive constant c multiplies the gradient of every function by c⁻¹.

theorem Bundle.ContMDiffRiemannianMetric.laplaceBeltrami_rescale_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I 2 M] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (hn : 1 ≤ n) {c : ℝ} (hc : 0 < c) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (x : M) : TauCeti.Manifold.laplaceBeltrami I f x = c⁻¹ * TauCeti.Manifold.laplaceBeltrami I f x

Scaling of the Laplacian. Multiplying a C¹ metric by a positive constant c multiplies the Laplace–Beltrami operator of every C² function by c⁻¹.

theorem Bundle.ContMDiffRiemannianMetric.curvatureTensor_leviCivitaConnection_rescale_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {c : ℝ} (hc : 0 < c) (x : M) : (CovariantDerivative.leviCivitaConnection I M).curvatureTensor x = (CovariantDerivative.leviCivitaConnection I M).curvatureTensor x

Multiplying a smooth metric by a positive constant does not change the (1,3) curvature tensor of its Levi-Civita connection.

theorem Bundle.ContMDiffRiemannianMetric.ricciTensor_leviCivitaConnection_rescale_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {c : ℝ} (hc : 0 < c) (x : M) : (CovariantDerivative.leviCivitaConnection I M).ricciTensor x = (CovariantDerivative.leviCivitaConnection I M).ricciTensor x

Multiplying a smooth metric by a positive constant does not change the Ricci tensor of its Levi-Civita connection.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {c : ℝ} (hc : 0 < c) (x : M) : (g.rescale (fun (x : M) => c) ⋯ ⋯).scalarCurvature x = c⁻¹ * g.scalarCurvature x

Scaling of scalar curvature. Multiplying a smooth metric by a positive constant c multiplies its scalar curvature by c⁻¹.

theorem Bundle.ContMDiffRiemannianMetric.sectionalCurvature_leviCivitaConnection_rescale_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {c : ℝ} (hc : 0 < c) (x : M) (u v : TangentSpace I x) : (CovariantDerivative.leviCivitaConnection I M).sectionalCurvature ⋯ x u v = c⁻¹ * (CovariantDerivative.leviCivitaConnection I M).sectionalCurvature ⋯ x u v

Scaling of sectional curvature. Multiplying a smooth metric by a positive constant c multiplies the sectional curvature of every pair of tangent vectors by c⁻¹.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.hasSectionalCurvatureAt_leviCivitaConnection_rescale_const_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {c : ℝ} (hc : 0 < c) (x : M) (k : ℝ) : (CovariantDerivative.leviCivitaConnection I M).HasSectionalCurvatureAt ⋯ x k ↔ (CovariantDerivative.leviCivitaConnection I M).HasSectionalCurvatureAt ⋯ x (c * k)

Multiplying a smooth metric by a positive constant c turns sectional curvature c * k at a point into sectional curvature k.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.hasConstantSectionalCurvature_leviCivitaConnection_rescale_const_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {c : ℝ} (hc : 0 < c) (k : ℝ) : (CovariantDerivative.leviCivitaConnection I M).HasConstantSectionalCurvature ⋯ k ↔ (CovariantDerivative.leviCivitaConnection I M).HasConstantSectionalCurvature ⋯ (c * k)

Scaling of constant sectional curvature. Multiplying a smooth metric by a positive constant c turns constant sectional curvature c * k into constant sectional curvature k.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.isConstantCurvatureTensor_rescale_const_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {c : ℝ} (hc : 0 < c) (κ : ℝ) : (g.rescale (fun (x : M) => c) ⋯ ⋯).IsConstantCurvatureTensor κ ↔ g.IsConstantCurvatureTensor (c * κ)

Multiplying a smooth metric by a positive constant c turns the constant-curvature tensor with parameter c * κ into the one with parameter κ.