Riemannian metrics on open submanifolds

This file restricts a C^n Riemannian metric to an open submanifold. Mathlib models the tangent space of a manifold on the model vector space itself, so the restricted metric is pointwise the ambient metric; the content is that this family is C^n for the inherited manifold and tangent bundle structures.

Main definitions

• Bundle.RiemannianMetric.restrictOpenTangentSpace: restriction of a fibrewise Riemannian metric.
• Bundle.ContMDiffRiemannianMetric.restrictOpenTangentSpace: restriction of a C^n Riemannian metric.
• TauCeti.Manifold.contMDiffRiemannianMetricOpen: the ambient instance metric restricted to an open submanifold.
• TauCeti.Manifold.instRiemannianBundleOpen, TauCeti.Manifold.instIsContinuousRiemannianBundleOpen, and TauCeti.Manifold.instIsContMDiffRiemannianBundleOpen: the corresponding scoped instances.
• TauCeti.Manifold.pathELength_subtypeVal_comp: the length of a curve in an open submanifold equals the length of its composition with the inclusion into the ambient manifold.
• TopologicalSpace.Opens.riemannianEDist_le_riemannianEDist_subtype: restriction to an open submanifold cannot decrease Riemannian distance.

The three instances are in the TauCeti scope; use open scoped TauCeti to install them. In particular, under the usual separation hypotheses this makes EMetricSpace.ofRiemannianMetric available on the open submanifold.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 1, §2.

noncomputable def Bundle.RiemannianMetric.restrictOpenTangentSpace {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 : RiemannianMetric fun (x : M) => TangentSpace I x) (U : TopologicalSpace.Opens M) : RiemannianMetric fun (x : ↥U) => TangentSpace I x

Restrict a Riemannian metric on a tangent bundle to an open submanifold.

Equations

• g.restrictOpenTangentSpace U = { inner := Bundle.RiemannianMetric.restrictedTangentInner✝ g, symm := ⋯, pos := ⋯, continuousAt := ⋯, isVonNBounded := ⋯ }

@[simp]

theorem Bundle.RiemannianMetric.restrictOpenTangentSpace_inner {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 : RiemannianMetric fun (x : M) => TangentSpace I x) (U : TopologicalSpace.Opens M) (x : ↥U) (v w : TangentSpace I x) : (((g.restrictOpenTangentSpace U).inner x) v) w = ((g.inner ↑x) ((TauCeti.Manifold.tangentSpaceOpenEquiv x) v)) ((TauCeti.Manifold.tangentSpaceOpenEquiv x) w)

Restricting a Riemannian metric evaluates the ambient metric through the canonical tangent-space identification.

theorem Bundle.RiemannianMetric.restrictOpenTangentSpace_inner_mfderiv_subtype_val {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 : RiemannianMetric fun (x : M) => TangentSpace I x) (U : TopologicalSpace.Opens M) (x : ↥U) (v w : TangentSpace I x) : (((g.restrictOpenTangentSpace U).inner x) v) w = ((g.inner ↑x) ((mfderiv% Subtype.val x) v)) ((mfderiv% Subtype.val x) w)

The restricted metric is the pullback of the ambient metric along the differential of the open-submanifold inclusion.

noncomputable def Bundle.ContMDiffRiemannianMetric.restrictOpenTangentSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (U : TopologicalSpace.Opens M) : ContMDiffRiemannianMetric I n E fun (x : ↥U) => TangentSpace I x

Restrict a C^n Riemannian metric on a manifold to an open submanifold.

Equations

• g.restrictOpenTangentSpace U = { inner := (g.toRiemannianMetric.restrictOpenTangentSpace U).inner, symm := ⋯, pos := ⋯, isVonNBounded := ⋯, contMDiff := ⋯ }

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.restrictOpenTangentSpace_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (U : TopologicalSpace.Opens M) (x : ↥U) (v w : TangentSpace I x) : (((g.restrictOpenTangentSpace U).inner x) v) w = ((g.inner ↑x) ((TauCeti.Manifold.tangentSpaceOpenEquiv x) v)) ((TauCeti.Manifold.tangentSpaceOpenEquiv x) w)

Restricting a C^n Riemannian metric evaluates the ambient metric through the canonical tangent-space identification.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.restrictOpenTangentSpace_toRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (U : TopologicalSpace.Opens M) : (g.restrictOpenTangentSpace U).toRiemannianMetric = g.toRiemannianMetric.restrictOpenTangentSpace U

Forgetting C^n regularity after restricting a metric gives its fibrewise restriction.

noncomputable def TauCeti.Manifold.contMDiffRiemannianMetricOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x] (U : TopologicalSpace.Opens M) : Bundle.ContMDiffRiemannianMetric I n E fun (x : ↥U) => TangentSpace I x

The C^n Riemannian metric on an open submanifold obtained by restricting the ambient metric.

Equations

• TauCeti.Manifold.contMDiffRiemannianMetricOpen U = Bundle.ContMDiffRiemannianMetric.ofIsContMDiffRiemannianBundle.restrictOpenTangentSpace U

@[simp]

theorem TauCeti.Manifold.contMDiffRiemannianMetricOpen_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x] (U : TopologicalSpace.Opens M) (x : ↥U) (v w : TangentSpace I x) : (((contMDiffRiemannianMetricOpen U).inner x) v) w = ((Bundle.RiemannianBundle.g.inner ↑x) ((tangentSpaceOpenEquiv x) v)) ((tangentSpaceOpenEquiv x) w)

The restricted Riemannian metric is the ambient metric under the canonical identification of tangent spaces.

@[instance_reducible]

noncomputable def TauCeti.Manifold.instRiemannianBundleOpen {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (U : TopologicalSpace.Opens M) : Bundle.RiemannianBundle fun (x : ↥U) => TangentSpace I x

An open submanifold inherits the ambient Riemannian bundle (fibrewise inner product).

Equations

• TauCeti.Manifold.instRiemannianBundleOpen U = { g := Bundle.RiemannianBundle.g.restrictOpenTangentSpace U }

theorem TauCeti.Manifold.instIsContinuousRiemannianBundleOpen {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (U : TopologicalSpace.Opens M) : IsContinuousRiemannianBundle E fun (x : ↥U) => TangentSpace I x

The restricted Riemannian bundle is continuous whenever the ambient bundle is continuous.

theorem TauCeti.Manifold.instIsContMDiffRiemannianBundleOpen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x] (U : TopologicalSpace.Opens M) : IsContMDiffRiemannianBundle I n E fun (x : ↥U) => TangentSpace I x

The restricted Riemannian bundle is as C^n as the ambient one.

@[simp]

theorem TauCeti.Manifold.riemannianBundleOpen_g {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (U : TopologicalSpace.Opens M) : Bundle.RiemannianBundle.g = Bundle.RiemannianBundle.g.restrictOpenTangentSpace U

The metric installed on an open submanifold is the fibrewise restriction of the ambient metric.

@[simp]

theorem TauCeti.Manifold.inner_tangentSpace_open {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (U : TopologicalSpace.Opens M) (x : ↥U) (v w : TangentSpace I x) : inner ℝ v w = ((Bundle.RiemannianBundle.g.inner ↑x) ((tangentSpaceOpenEquiv x) v)) ((tangentSpaceOpenEquiv x) w)

The inner product installed on an open submanifold is the ambient inner product under the canonical tangent-space identification.

@[simp]

theorem TauCeti.Manifold.norm_tangentSpace_open {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (U : TopologicalSpace.Opens M) (x : ↥U) (v : TangentSpace I x) : ‖v‖ = ‖(tangentSpaceOpenEquiv x) v‖

The norm installed on an open submanifold is the ambient Riemannian norm under the canonical tangent-space identification.

@[simp]

theorem TauCeti.Manifold.enorm_tangentSpace_open {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (U : TopologicalSpace.Opens M) (x : ↥U) (v : TangentSpace I x) : ‖v‖ₑ = ‖(tangentSpaceOpenEquiv x) v‖ₑ

The extended norm installed on an open submanifold is the ambient Riemannian extended norm under the canonical tangent-space identification.

@[simp]

theorem TauCeti.Manifold.pathELength_subtypeVal_comp {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {U : TopologicalSpace.Opens M} {γ : ℝ → ↥U} {a b : ℝ} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) : Manifold.pathELength I γ a b = Manifold.pathELength I (Subtype.val ∘ γ) a b

Path length is intrinsic: restricting the metric of M to an open submanifold U does not change the length of a C¹ curve read in U.

theorem TopologicalSpace.Opens.riemannianEDist_le_riemannianEDist_subtype {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (U : Opens M) (x y : ↥U) : Manifold.riemannianEDist I ↑x ↑y ≤ Manifold.riemannianEDist I x y

Restricting the Riemannian metric to an open submanifold cannot decrease distance: every curve in the submanifold is an ambient curve of the same length.