Isometry invariance of the Riemannian volume

A homeomorphism Φ : M ≃ₜ N between manifolds with continuous Riemannian metrics which is differentiable, and whose tangent maps preserve the Riemannian inner products, carries the Riemannian volume of M to the Riemannian volume of N. In particular isometric manifolds have the same Riemannian volume, which is what makes the total volume a Riemannian invariant.

The isometry condition is stated pointwise, on the tangent maps, and no orientation is used, so orientation-reversing isometries and manifolds with boundary or corners are covered. The two manifolds may be modelled on different model spaces H and H' over the same vector space E.

The statement is the invariance of the Riemannian density under isometries, as in J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (Riemannian volume forms and densities).

Main results

• TauCeti.chartVolumeDensity_eq_abs_det_mul_of_inner_mfderiv: the chart volume densities of two Riemannian manifolds differ by the absolute Jacobian determinant of a map whose tangent map preserves the inner products.
• TauCeti.chartRiemannianVolume_image_of_inner_mfderiv: such a map, injective on a subset of a chart source, carries its chart volume to the chart volume of its image.
• Homeomorph.measurePreserving_riemannianVolume: a differentiable homeomorphism whose tangent maps preserve the inner products preserves the Riemannian volume.

theorem TauCeti.chartVolumeDensity_eq_abs_det_mul_of_inner_mfderiv {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 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {H' : Type u_4} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E H'} {N : Type u_5} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' 1 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace I' y] {Φ : M → N} {α x : M} {β : N} (hxα : x ∈ (chartAt H α).source) (hxβ : Φ x ∈ (chartAt H' β).source) (hinner : ∀ (v w : TangentSpace I x), inner ℝ ((mfderiv% Φ x) v) ((mfderiv% Φ x) w) = inner ℝ v w) : chartVolumeDensity α x = |(mfderiv% ↑(extChartAt I' β) (Φ x) ∘SL mfderiv% Φ x ∘SL mfderiv[Set.range ↑I] ↑(extChartAt I α).symm (↑(extChartAt I α) x)).det| * chartVolumeDensity β (Φ x)

If the tangent map of Φ at x preserves the Riemannian inner products, then the volume density of M in the chart at α is the volume density of N in the chart at β multiplied by the absolute Jacobian determinant of Φ read in these two charts.

theorem TauCeti.chartRiemannianVolume_image_of_inner_mfderiv {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 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {H' : Type u_4} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E H'} {N : Type u_5} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' 1 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace I' y] [MeasurableSpace M] [BorelSpace M] [MeasurableSpace N] [BorelSpace N] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (y : N) => TangentSpace I' y] {Φ : M → N} {α : M} {β : N} {s : Set M} (hs : MeasurableSet s) (hΦs : MeasurableSet (Φ '' s)) (hinj : Set.InjOn Φ s) (hsα : s ⊆ (chartAt H α).source) (hsβ : Set.MapsTo Φ s (chartAt H' β).source) (hΦ : ∀ x ∈ s, MDiffAt Φ x) (hinner : ∀ x ∈ s, ∀ (v w : TangentSpace I x), inner ℝ ((mfderiv% Φ x) v) ((mfderiv% Φ x) w) = inner ℝ v w) : (chartRiemannianVolume β) (Φ '' s) = (chartRiemannianVolume α) s

A map which is injective and differentiable on a measurable subset s of the chart source at α, maps s into the chart source at β, and whose tangent maps at points of s preserve the Riemannian inner products, carries the chart volume of s at α to the chart volume of its image at β.

theorem Homeomorph.measurePreserving_riemannianVolume {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 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {H' : Type u_4} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E H'} {N : Type u_5} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' 1 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace I' y] [MeasurableSpace M] [BorelSpace M] [MeasurableSpace N] [BorelSpace N] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (y : N) => TangentSpace I' y] [LindelofSpace M] [LindelofSpace N] (Φ : M ≃ₜ N) (hΦ : MDiff ⇑Φ) (hinner : ∀ (x : M) (v w : TangentSpace I x), inner ℝ ((mfderiv% ⇑Φ x) v) ((mfderiv% ⇑Φ x) w) = inner ℝ v w) : MeasureTheory.MeasurePreserving (⇑Φ) (TauCeti.riemannianVolume I M) (TauCeti.riemannianVolume I' N)

Isometry invariance of the Riemannian volume. A differentiable homeomorphism whose tangent maps preserve the Riemannian inner products carries the Riemannian volume of M to the Riemannian volume of N.

theorem TauCeti.RiemannianIsometry.measurePreserving_riemannianVolume {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 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {H' : Type u_4} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E H'} {N : Type u_5} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I' 1 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace I' y] [MeasurableSpace M] [BorelSpace M] [MeasurableSpace N] [BorelSpace N] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (y : N) => TangentSpace I' y] [LindelofSpace M] [LindelofSpace N] (Φ : RiemannianIsometry I I' M N) : MeasureTheory.MeasurePreserving (⇑Φ) (riemannianVolume I M) (riemannianVolume I' N)

A Riemannian isometry preserves the Riemannian volume measure.

This packages the general homeomorphism theorem at the canonical RiemannianIsometry API.