The Riemannian metric of an (Isom X, X)-manifold

Let X be a Riemannian manifold and M an (Isom X, X)-manifold: a space with an X-valued atlas whose transition maps are locally Riemannian isometries of X ([ChartedSpace X M] [HasGroupoid M (smulGroupoid (Isom I X) X)]). For a model geometry X, this is a geometric structure on M modelled on X. Such an M inherits a Riemannian metric from X: read the metric of X through any chart. The transition maps preserve the metric of X, so the result does not depend on the chart, and it is the unique metric on M for which every chart is a local isometry. This is the metric with respect to which completeness of the geometric structure is measured (Thurston, Proposition 3.4.15).

Throughout, M carries the composite charts ChartedSpace.comp H X M, obtained by following its X-valued charts with the charts of X; this is the smooth structure of isManifold_of_hasGroupoid_smulGroupoid, and it is not an instance, so the statements install it with letI. A (G, X)-manifold for a group G acting on X through Riemannian isometries is an (Isom X, X)-manifold by smulGroupoid_le, so everything here applies to it.

Main definitions

• TauCeti.chartRiemannianMetric: the metric of X read on M through the preferred charts.
• TauCeti.contMDiffChartRiemannianMetric: the same metric, bundled with its smoothness: it is C^n whenever the metric of X is.

Main results

• TauCeti.chartRiemannianMetric_inner: at x, the metric is the metric of X pulled back along the derivative of the preferred chart at x.
• TauCeti.inner_mfderiv_of_mem_atlas: every chart of M is a local isometry to X.
• TauCeti.eq_chartRiemannianMetric_iff: the metric read through the charts is the only Riemannian metric on M for which every chart is a local isometry.
• TauCeti.isContMDiffRiemannianBundle_chartRiemannianMetric: installed as the Riemannian bundle structure of M, the metric is C^n whenever the metric of X is.
• TauCeti.isLocalRiemannianIsometry_restrict_of_mem_atlas: a chart of M, restricted to its source, is a local Riemannian isometry to X.

References

• W. P. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Princeton University Press, 1997, Section 3.3 ((G, X)-manifolds) and Section 3.4 (the metric a (G, X)-manifold inherits from a G-invariant metric on X, Proposition 3.4.15).

The metric read through the charts

def TauCeti.chartRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (X : Type u_3) [TopologicalSpace X] [ChartedSpace H X] [Bundle.RiemannianBundle fun (x : X) => TangentSpace I x] (M : Type u_4) [TopologicalSpace M] [ChartedSpace X M] : Bundle.RiemannianMetric fun (x : M) => TangentSpace I x

The Riemannian metric of X read on M through its preferred X-valued charts: at x, it is the inner product of X at chartAt X x x. The tangent spaces of M are those of the composite charts ChartedSpace.comp H X M.

@[simp]

theorem TauCeti.chartRiemannianMetric_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] [Bundle.RiemannianBundle fun (x : X) => TangentSpace I x] {M : Type u_4} [TopologicalSpace M] [ChartedSpace X M] (x : M) (v w : TangentSpace I x) : (((chartRiemannianMetric I X M).inner x) v) w = inner ℝ ((mfderiv% ↑(chartAt X x) x) v) ((mfderiv% ↑(chartAt X x) x) w)

At x, the metric read through the charts is the metric of X pulled back along the derivative of the preferred chart at x.

theorem TauCeti.inner_mfderiv_of_mem_atlas {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] [Bundle.RiemannianBundle fun (x : X) => TangentSpace I x] {M : Type u_4} [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid (Isom I X) X)] {e : OpenPartialHomeomorph M X} (he : e ∈ atlas X M) {y : M} (hy : y ∈ e.source) (v w : TangentSpace I y) : inner ℝ ((mfderiv% ↑e y) v) ((mfderiv% ↑e y) w) = (((chartRiemannianMetric I X M).inner y) v) w

Every chart of an (Isom X, X)-manifold is a local isometry from the metric read through the charts to the metric of X.

theorem TauCeti.eq_chartRiemannianMetric_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] [Bundle.RiemannianBundle fun (x : X) => TangentSpace I x] {M : Type u_4} [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid (Isom I X) X)] (g : Bundle.RiemannianMetric fun (x : M) => TangentSpace I x) : g = chartRiemannianMetric I X M ↔ ∀ e ∈ atlas X M, ∀ y ∈ e.source, ∀ (v w : TangentSpace I y), inner ℝ ((mfderiv% ↑e y) v) ((mfderiv% ↑e y) w) = ((g.inner y) v) w

The metric read through the charts is the only Riemannian metric on an (Isom X, X)-manifold for which every chart is a local isometry to X.

Smoothness

def TauCeti.contMDiffChartRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (X : Type u_3) [TopologicalSpace X] [ChartedSpace H X] [Bundle.RiemannianBundle fun (x : X) => TangentSpace I x] (M : Type u_4) [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid (Isom I X) X)] [IsManifold I 1 X] (n : WithTop ℕ∞) [IsContMDiffRiemannianBundle I n E fun (x : X) => TangentSpace I x] : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x

The metric of an (Isom X, X)-manifold read through its charts, bundled as a C^n Riemannian metric for the smooth structure of the composite charts, when the metric of X is C^n.

@[simp]

theorem TauCeti.contMDiffChartRiemannianMetric_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] [Bundle.RiemannianBundle fun (x : X) => TangentSpace I x] {M : Type u_4} [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid (Isom I X) X)] [IsManifold I 1 X] {n : WithTop ℕ∞} [IsContMDiffRiemannianBundle I n E fun (x : X) => TangentSpace I x] : (contMDiffChartRiemannianMetric I X M n).inner = (chartRiemannianMetric I X M).inner

The inner product of contMDiffChartRiemannianMetric is that of the metric read through the charts.

@[simp]

theorem TauCeti.contMDiffChartRiemannianMetric_toRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] [Bundle.RiemannianBundle fun (x : X) => TangentSpace I x] {M : Type u_4} [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid (Isom I X) X)] [IsManifold I 1 X] {n : WithTop ℕ∞} [IsContMDiffRiemannianBundle I n E fun (x : X) => TangentSpace I x] : (contMDiffChartRiemannianMetric I X M n).toRiemannianMetric = chartRiemannianMetric I X M

Forgetting smoothness of contMDiffChartRiemannianMetric gives the metric read through the charts.

theorem TauCeti.isContMDiffRiemannianBundle_chartRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] [Bundle.RiemannianBundle fun (x : X) => TangentSpace I x] {M : Type u_4} [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid (Isom I X) X)] [IsManifold I 1 X] {n : WithTop ℕ∞} [IsContMDiffRiemannianBundle I n E fun (x : X) => TangentSpace I x] : IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x

Installed as the Riemannian bundle structure of an (Isom X, X)-manifold, the metric read through the charts is C^n whenever the metric of X is.

Charts as local isometries

theorem TauCeti.isLocalRiemannianIsometry_restrict_of_mem_atlas {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {X : Type u_3} [TopologicalSpace X] [ChartedSpace H X] [Bundle.RiemannianBundle fun (x : X) => TangentSpace I x] {M : Type u_4} [TopologicalSpace M] [ChartedSpace X M] [HasGroupoid M (smulGroupoid (Isom I X) X)] [IsManifold I (↑⊤) X] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : X) => TangentSpace I x] {e : OpenPartialHomeomorph M X} (he : e ∈ atlas X M) : IsLocalRiemannianIsometry I I fun (y : ↥{ carrier := e.source, is_open' := ⋯ }) => ↑e ↑y

A chart e of an (Isom X, X)-manifold, restricted to its source, is a local Riemannian isometry from the chart metric restricted to the source to the metric of X.