Descending Riemannian metrics along local diffeomorphisms

Let f : M → N be a surjective local diffeomorphism and g a Riemannian metric on M. If the inner product of g is compatible with f, in the sense that tangent vectors at points of one fibre with the same images under the differential of f have the same inner products, then g descends to a Riemannian metric g.descend on N: at f x it is g at x read through the inverse of the differential of f at x. It is the unique metric on N whose pullback along f is g (Bundle.ContMDiffRiemannianMetric.pullback_eq_iff_eq_descend), so f is a local Riemannian isometry from g to g.descend. Near each point the descended metric is the pullback of g along a local inverse of f, which makes it as regular as g when f is one degree more regular. Since curvature is natural under local isometries, the descended metric has the scalar curvature of g: Scal(g.descend) (f x) = Scal(g) x.

The main example is the orbit projection of a free, properly discontinuous smooth action of a group G on M by isometries of g: then g descends to the orbit space M / G (Bundle.ContMDiffRiemannianMetric.quotient). Examples are the round metric on real projective spaces and lens spaces, product metrics on Dold manifolds (Sᵃ × ℂPᵇ) / C₂, and the metric dt² + g on the mapping torus of an isometry of g.

Main definitions and results

• Bundle.ContMDiffRiemannianMetric.descend: the metric descended along a surjective local diffeomorphism.
• Bundle.ContMDiffRiemannianMetric.descend_inner_mfderiv: the descended metric at f x, applied to the images of two tangent vectors at x, is their inner product for g.
• Bundle.ContMDiffRiemannianMetric.pullback_eq_iff_eq_descend: the descended metric is the unique metric on N whose pullback along f is g.
• Bundle.ContMDiffRiemannianMetric.isLocalRiemannianIsometry_descend: f is a local Riemannian isometry from g to the descended metric.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_descend: the descended metric has the scalar curvature of g.
• Bundle.ContMDiffRiemannianMetric.inner_eq_of_quotientMk_eq: a metric invariant under a free, properly discontinuous group action is compatible with the orbit projection.
• Bundle.ContMDiffRiemannianMetric.quotient: a metric invariant under a free, properly discontinuous smooth group action descends to the orbit space.
• Bundle.ContMDiffRiemannianMetric.pullback_eq_iff_eq_quotient: the metric on the orbit space is the unique metric whose pullback along the orbit projection is the invariant metric.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_quotient: the metric on the orbit space has the scalar curvature of the invariant metric.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (Riemannian coverings and quotients by isometric group actions) and Proposition 7.6 (naturality of curvature).

noncomputable def Bundle.ContMDiffRiemannianMetric.descend {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] {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] {n : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold J 1 N] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) {f : M → N} (hf : IsLocalDiffeomorph I J (n + 1) f) (hsurj : Function.Surjective f) (hg : ∀ (x x' : M) (v w : TangentSpace I x) (v' w' : TangentSpace I x'), f x = f x' → (mfderiv% f x) v = (mfderiv% f x') v' → (mfderiv% f x) w = (mfderiv% f x') w' → ((g.inner x) v) w = ((g.inner x') v') w') : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y

The Riemannian metric on N obtained by descending a metric g on M along a surjective local diffeomorphism f : M → N, when tangent vectors at points of one fibre with the same images under the differential of f have the same inner products. At y = f x it is g at x, evaluated on the preimages of tangent vectors under the differential of f at x; the hypothesis makes this independent of the choice of x.

theorem Bundle.ContMDiffRiemannianMetric.descend_inner_mfderiv_of_eq {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] {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] {n : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold J 1 N] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) {f : M → N} (hf : IsLocalDiffeomorph I J (n + 1) f) (hsurj : Function.Surjective f) (hg : ∀ (x x' : M) (v w : TangentSpace I x) (v' w' : TangentSpace I x'), f x = f x' → (mfderiv% f x) v = (mfderiv% f x') v' → (mfderiv% f x) w = (mfderiv% f x') w' → ((g.inner x) v) w = ((g.inner x') v') w') {x : M} {y : N} (h : f x = y) (v w : TangentSpace I x) : (((g.descend hf hsurj hg).inner y) ((mfderiv% f x) v)) ((mfderiv% f x) w) = ((g.inner x) v) w

The descended metric at y = f x, applied to the images under the differential of f at x of two tangent vectors at x, is their inner product for g.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.descend_inner_mfderiv {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] {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] {n : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold J 1 N] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) {f : M → N} (hf : IsLocalDiffeomorph I J (n + 1) f) (hsurj : Function.Surjective f) (hg : ∀ (x x' : M) (v w : TangentSpace I x) (v' w' : TangentSpace I x'), f x = f x' → (mfderiv% f x) v = (mfderiv% f x') v' → (mfderiv% f x) w = (mfderiv% f x') w' → ((g.inner x) v) w = ((g.inner x') v') w') (x : M) (v w : TangentSpace I x) : (((g.descend hf hsurj hg).inner (f x)) ((mfderiv% f x) v)) ((mfderiv% f x) w) = ((g.inner x) v) w

The descended metric at f x, applied to the images under the differential of f at x of two tangent vectors at x, is their inner product for g.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.pullback_descend {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] {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] {n : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold J 1 N] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) {f : M → N} (hf : IsLocalDiffeomorph I J (n + 1) f) (hsurj : Function.Surjective f) (hg : ∀ (x x' : M) (v w : TangentSpace I x) (v' w' : TangentSpace I x'), f x = f x' → (mfderiv% f x) v = (mfderiv% f x') v' → (mfderiv% f x) w = (mfderiv% f x') w' → ((g.inner x) v) w = ((g.inner x') v') w') [FiniteDimensional ℝ E] (hf' : ContMDiff I J (n + 1) f) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) : (g.descend hf hsurj hg).pullback f hf' hinj = g

Pulling the descended metric back along f recovers g.

theorem Bundle.ContMDiffRiemannianMetric.pullback_eq_iff_eq_descend {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] {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] {n : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold J 1 N] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) {f : M → N} (hf : IsLocalDiffeomorph I J (n + 1) f) (hsurj : Function.Surjective f) (hg : ∀ (x x' : M) (v w : TangentSpace I x) (v' w' : TangentSpace I x'), f x = f x' → (mfderiv% f x) v = (mfderiv% f x') v' → (mfderiv% f x) w = (mfderiv% f x') w' → ((g.inner x) v) w = ((g.inner x') v') w') [FiniteDimensional ℝ E] (h : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y) (hf' : ContMDiff I J (n + 1) f) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) : h.pullback f hf' hinj = g ↔ h = g.descend hf hsurj hg

The descended metric is the unique metric on N whose pullback along f is g.

theorem Bundle.ContMDiffRiemannianMetric.isLocalRiemannianIsometry_descend {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] {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 I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → N} (hf : IsLocalDiffeomorph I J (↑⊤ + 1) f) (hsurj : Function.Surjective f) (hg : ∀ (x x' : M) (v w : TangentSpace I x) (v' w' : TangentSpace I x'), f x = f x' → (mfderiv% f x) v = (mfderiv% f x') v' → (mfderiv% f x) w = (mfderiv% f x') w' → ((g.inner x) v) w = ((g.inner x') v') w') : TauCeti.IsLocalRiemannianIsometry I J f

With g installed on M and the descended metric on N, the map f is a local Riemannian isometry.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_descend {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] {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 I (↑⊤) E fun (x : M) => TangentSpace I x) {f : M → N} (hf : IsLocalDiffeomorph I J (↑⊤ + 1) f) (hsurj : Function.Surjective f) (hg : ∀ (x x' : M) (v w : TangentSpace I x) (v' w' : TangentSpace I x'), f x = f x' → (mfderiv% f x) v = (mfderiv% f x') v' → (mfderiv% f x) w = (mfderiv% f x') w' → ((g.inner x) v) w = ((g.inner x') v') w') [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [T2Space M] [T2Space N] (x : M) : (g.descend hf hsurj hg).scalarCurvature (f x) = g.scalarCurvature x

Scalar curvature of a descended metric. The descended metric has the scalar curvature of g: its scalar curvature at f x is the scalar curvature of g at x.

Quotients by isometric group actions

theorem Bundle.ContMDiffRiemannianMetric.inner_eq_of_quotientMk_eq {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] {n : WithTop ℕ∞} {G : Type u_7} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] [ContMDiffConstSMul I 1 G M] [IsManifold I 1 M] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (hg : ∀ (a : G) (x : M) (v w : TangentSpace I x), ((g.inner (a • x)) (((mfderiv% fun (x : M) => a • x) x) v)) (((mfderiv% fun (x : M) => a • x) x) w) = ((g.inner x) v) w) (x x' : M) (v w : TangentSpace I x) (v' w' : TangentSpace I x') (hx : ⟦x⟧ = ⟦x'⟧) (hv : (mfderiv% (Quotient.mk (MulAction.orbitRel G M)) x) v = (mfderiv% (Quotient.mk (MulAction.orbitRel G M)) x') v') (hw : (mfderiv% (Quotient.mk (MulAction.orbitRel G M)) x) w = (mfderiv% (Quotient.mk (MulAction.orbitRel G M)) x') w') : ((g.inner x) v) w = ((g.inner x') v') w'

A metric preserved by every element of G is compatible with the orbit projection of a free, properly discontinuous C^1 action: tangent vectors at points of one orbit with the same images in the orbit space have the same inner products. This is the compatibility hypothesis of Bundle.ContMDiffRiemannianMetric.descend for the orbit projection, for a metric of any regularity.

noncomputable def Bundle.ContMDiffRiemannianMetric.quotient {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] {G : Type u_7} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] [ContMDiffConstSMul I (↑⊤) G M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hg : ∀ (a : G) (x : M) (v w : TangentSpace I x), ((g.inner (a • x)) (((mfderiv% fun (x : M) => a • x) x) v)) (((mfderiv% fun (x : M) => a • x) x) w) = ((g.inner x) v) w) : ContMDiffRiemannianMetric I (↑⊤) E fun (x : MulAction.orbitRel.Quotient G M) => TangentSpace I x

The metric on the orbit space of a free, properly discontinuous smooth action of G by isometries of g, descended from g along the orbit projection.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.quotient_inner_mfderiv {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] {G : Type u_7} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] [ContMDiffConstSMul I (↑⊤) G M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hg : ∀ (a : G) (x : M) (v w : TangentSpace I x), ((g.inner (a • x)) (((mfderiv% fun (x : M) => a • x) x) v)) (((mfderiv% fun (x : M) => a • x) x) w) = ((g.inner x) v) w) (x : M) (v w : TangentSpace I x) : (((g.quotient hg).inner ⟦x⟧) ((mfderiv% (Quotient.mk (MulAction.orbitRel G M)) x) v)) ((mfderiv% (Quotient.mk (MulAction.orbitRel G M)) x) w) = ((g.inner x) v) w

The metric on the orbit space at the orbit of x, applied to the images of two tangent vectors at x, is their inner product for g.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.pullback_quotient {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] {G : Type u_7} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] [ContMDiffConstSMul I (↑⊤) G M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hg : ∀ (a : G) (x : M) (v w : TangentSpace I x), ((g.inner (a • x)) (((mfderiv% fun (x : M) => a • x) x) v)) (((mfderiv% fun (x : M) => a • x) x) w) = ((g.inner x) v) w) [FiniteDimensional ℝ E] (hq : ContMDiff I I (↑⊤ + 1) (Quotient.mk (MulAction.orbitRel G M))) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% (Quotient.mk (MulAction.orbitRel G M)) x)) : (g.quotient hg).pullback (Quotient.mk (MulAction.orbitRel G M)) hq hinj = g

Pulling the metric on the orbit space back along the orbit projection recovers g.

theorem Bundle.ContMDiffRiemannianMetric.pullback_eq_iff_eq_quotient {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] {G : Type u_7} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] [ContMDiffConstSMul I (↑⊤) G M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hg : ∀ (a : G) (x : M) (v w : TangentSpace I x), ((g.inner (a • x)) (((mfderiv% fun (x : M) => a • x) x) v)) (((mfderiv% fun (x : M) => a • x) x) w) = ((g.inner x) v) w) [FiniteDimensional ℝ E] (h : ContMDiffRiemannianMetric I (↑⊤) E fun (x : MulAction.orbitRel.Quotient G M) => TangentSpace I x) (hq : ContMDiff I I (↑⊤ + 1) (Quotient.mk (MulAction.orbitRel G M))) (hinj : ∀ (x : M), Function.Injective ⇑(mfderiv% (Quotient.mk (MulAction.orbitRel G M)) x)) : h.pullback (Quotient.mk (MulAction.orbitRel G M)) hq hinj = g ↔ h = g.quotient hg

The metric on the orbit space is the unique metric on the orbit space whose pullback along the orbit projection is g.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_quotient {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] {G : Type u_7} [Group G] [MulAction G M] [ProperlyDiscontinuousSMul G M] [ContinuousConstSMul G M] [IsCancelSMul G M] [T2Space M] [LocallyCompactSpace M] [ContMDiffConstSMul I (↑⊤) G M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hg : ∀ (a : G) (x : M) (v w : TangentSpace I x), ((g.inner (a • x)) (((mfderiv% fun (x : M) => a • x) x) v)) (((mfderiv% fun (x : M) => a • x) x) w) = ((g.inner x) v) w) [FiniteDimensional ℝ E] (x : M) : (g.quotient hg).scalarCurvature ⟦x⟧ = g.scalarCurvature x

The metric on the orbit space has the scalar curvature of g: at the orbit of x it is the scalar curvature of g at x.