Pulling a smooth metric back along a diffeomorphism

Let Φ : M → N be a diffeomorphism and g a smooth Riemannian metric on N. The pullback metric Φ^* g on M (Bundle.ContMDiffRiemannianMetric.pullback) is the metric for which Φ becomes a Riemannian isometry (M, Φ^* g) → (N, g). Every curvature quantity is natural under Riemannian isometries, so the curvature of Φ^* g at x is the curvature of g at Φ x. In particular the scalar curvature satisfies Scal(Φ^* g) = Scal(g) ∘ Φ; this is the diffeomorphism-invariance used for positive scalar curvature metrics, and the sectional curvature of Φ^* g on a plane is that of g on its image plane. Since curvature is natural under local Riemannian isometries, the same formula holds along any smooth map whose differential is invertible at every point, such as a reparametrisation of the ℝ factor of M × ℝ.

Main definitions and results

• Bundle.ContMDiffRiemannianMetric.pullbackRiemannianIsometry: a diffeomorphism Φ as a Riemannian isometry from the pulled-back metric Φ^* g to g.
• Bundle.ContMDiffRiemannianMetric.isLocalRiemannianIsometry_pullback_of_isInvertible: a smooth map f whose differential is invertible at every point is a local Riemannian isometry from f^* g to g.
• Bundle.ContMDiffRiemannianMetric.sectionalCurvature_pullback_of_isInvertible: the sectional curvature of f^* g on the plane spanned by u, v at x is that of g on the plane spanned by df_x u, df_x v at f x.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_pullback_of_isInvertible: the scalar curvature of f^* g at x is the scalar curvature of g at f x, for any smooth map f whose differential is invertible at every point.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_pullback: in particular, along a diffeomorphism Φ, Scal(Φ^* g) = Scal(g) ∘ Φ.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (pullback metrics) and Proposition 7.6 (naturality of curvature).

def Bundle.ContMDiffRiemannianMetric.pullbackRiemannianIsometry {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 1 M] [IsManifold J 1 N] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y) (Φ : Diffeomorph I J M N ↑⊤) (hf : ContMDiff I J (n + 1) ⇑Φ) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% ⇑Φ x)) : TauCeti.RiemannianIsometry I J M N

A diffeomorphism Φ : M → N is a Riemannian isometry from the metric Φ^* g pulled back along Φ to the metric g on N.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.toDiffeomorph_pullbackRiemannianIsometry {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 1 M] [IsManifold J 1 N] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y) (Φ : Diffeomorph I J M N ↑⊤) (hf : ContMDiff I J (n + 1) ⇑Φ) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% ⇑Φ x)) : (g.pullbackRiemannianIsometry Φ hf hinj).toDiffeomorph = Φ

The underlying diffeomorphism of pullbackRiemannianIsometry g Φ is Φ.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.coe_pullbackRiemannianIsometry {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 1 M] [IsManifold J 1 N] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y) (Φ : Diffeomorph I J M N ↑⊤) (hf : ContMDiff I J (n + 1) ⇑Φ) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% ⇑Φ x)) : ⇑(g.pullbackRiemannianIsometry Φ hf hinj) = ⇑Φ

As a function, pullbackRiemannianIsometry g Φ is Φ.

theorem Bundle.ContMDiffRiemannianMetric.isLocalRiemannianIsometry_pullback_of_isInvertible {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I (↑⊤) M] [IsManifold J (↑⊤) N] (g : ContMDiffRiemannianMetric J (↑⊤) F fun (y : N) => TangentSpace J y) {f : M → N} (hf : ContMDiff I J (↑⊤ + 1) f) (hinv : ∀ (x : M), (mfderiv% f x).IsInvertible) : TauCeti.IsLocalRiemannianIsometry I J f

A smooth map whose differential is invertible at every point is a local Riemannian isometry from the pulled-back metric f^* g to g.

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_pullback_of_isInvertible {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [FiniteDimensional ℝ F] [T2Space M] [T2Space N] [IsManifold I (↑⊤) M] [IsManifold J (↑⊤) N] (g : ContMDiffRiemannianMetric J (↑⊤) F fun (y : N) => TangentSpace J y) {f : M → N} (hf : ContMDiff I J (↑⊤ + 1) f) (hinv : ∀ (x : M), (mfderiv% f x).IsInvertible) (x : M) : (g.pullback f hf ⋯).scalarCurvature x = g.scalarCurvature (f x)

Scalar curvature of a pullback along a local diffeomorphism. If the differential of a smooth map f is invertible at every point, the scalar curvature of f^* g at x is the scalar curvature of g at f x.

theorem Bundle.ContMDiffRiemannianMetric.sectionalCurvature_pullback_of_isInvertible {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [FiniteDimensional ℝ F] [T2Space M] [T2Space N] [IsManifold I (↑⊤) M] [IsManifold J (↑⊤) N] (g : ContMDiffRiemannianMetric J (↑⊤) F fun (y : N) => TangentSpace J y) {f : M → N} (hf : ContMDiff I J (↑⊤ + 1) f) (hinv : ∀ (x : M), (mfderiv% f x).IsInvertible) (x : M) (u v : TangentSpace I x) : (CovariantDerivative.leviCivitaConnection I M).sectionalCurvature ⋯ x u v = (CovariantDerivative.leviCivitaConnection J N).sectionalCurvature ⋯ (f x) ((mfderiv% f x) u) ((mfderiv% f x) v)

Sectional curvature of a pullback along a local diffeomorphism. If the differential of a smooth map f is invertible at every point, the sectional curvature of f^* g on the plane spanned by u, v at x is the sectional curvature of g on the plane spanned by df_x u, df_x v at f x.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_pullback {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [FiniteDimensional ℝ F] [T2Space M] [T2Space N] [IsManifold I (↑⊤) M] [IsManifold J (↑⊤) N] (g : ContMDiffRiemannianMetric J (↑⊤) F fun (y : N) => TangentSpace J y) (Φ : Diffeomorph I J M N ↑⊤) (hf : ContMDiff I J (↑⊤ + 1) ⇑Φ) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% ⇑Φ x)) (x : M) : (g.pullback (⇑Φ) hf hinj).scalarCurvature x = g.scalarCurvature (Φ x)

Diffeomorphism invariance of scalar curvature. The scalar curvature of the metric Φ^* g pulled back along a diffeomorphism Φ is the scalar curvature of g composed with Φ.