Restrictions of Riemannian metrics

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.

It also restricts a C^n metric on M × ℝ to the manifold with boundary M × [a, b], as the pullback along the inclusion, whose differential is invertible also at the boundary.

Main definitions

• Bundle.RiemannianMetric.restrictOpenTangentSpace: restriction of a fibrewise Riemannian metric.
• Bundle.ContMDiffRiemannianMetric.restrictOpenTangentSpace: restriction of a C^n Riemannian metric.
• Bundle.ContMDiffRiemannianMetric.restrictOpenTangentSpace_eq_of_inner_eq: metrics that agree on an open set have equal restrictions to it.
• 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.
• Bundle.ContMDiffRiemannianMetric.restrictIcc: the restriction of a metric on M × ℝ to M × [a, b].

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.

@[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.

@[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.

theorem Bundle.ContMDiffRiemannianMetric.restrictOpenTangentSpace_eq_pullback {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] [FiniteDimensional ℝ E] (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (U : TopologicalSpace.Opens M) : g.restrictOpenTangentSpace U = g.pullback Subtype.val ⋯ ⋯

Restriction to an open submanifold is pullback along its inclusion.

@[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.

theorem Bundle.ContMDiffRiemannianMetric.restrictOpenTangentSpace_eq_of_inner_eq {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₁ g₂ : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x} (U : TopologicalSpace.Opens M) (h : ∀ x ∈ U, g₁.inner x = g₂.inner x) : g₁.restrictOpenTangentSpace U = g₂.restrictOpenTangentSpace U

Two C^n Riemannian metrics that agree on an open set U have equal restrictions to U.

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.

@[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).

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} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [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 : ℝ} : 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 curve read in U. (Where the curve is not differentiable both integrands take the junk value 0.)

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.

noncomputable def Bundle.ContMDiffRiemannianMetric.restrictIcc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] (a b : ℝ) [Fact (a < b)] (G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) n (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p) : ContMDiffRiemannianMetric (I.prod (modelWithCornersEuclideanHalfSpace 1)) n (E × EuclideanSpace ℝ (Fin 1)) fun (p : M × ↑(Set.Icc a b)) => TangentSpace (I.prod (modelWithCornersEuclideanHalfSpace 1)) p

The restriction of a metric G on M × ℝ to the manifold with boundary M × [a, b]: the pullback of G along the inclusion.

theorem Bundle.ContMDiffRiemannianMetric.restrictIcc_eq_pullback {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] {a b : ℝ} [Fact (a < b)] (G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) n (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p) : restrictIcc a b G = G.pullback (Prod.map id Subtype.val) ⋯ ⋯

The restriction of G to M × [a, b] is the pullback of G along the inclusion.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.restrictIcc_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] {a b : ℝ} [Fact (a < b)] (G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) n (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p) (p : M × ↑(Set.Icc a b)) (v w : TangentSpace (I.prod (modelWithCornersEuclideanHalfSpace 1)) p) : (((restrictIcc a b G).inner p) v) w = ((G.inner (p.1, ↑p.2)) ((mfderiv% (Prod.map id Subtype.val) p) v)) ((mfderiv% (Prod.map id Subtype.val) p) w)

The restriction of G to M × [a, b] at (x, t) is G at (x, t), evaluated on the images of the tangent vectors under the differential of the inclusion.

theorem Bundle.ContMDiffRiemannianMetric.restrictIcc_inner_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] {a b : ℝ} [Fact (a < b)] {G G' : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) n (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} {p : M × ↑(Set.Icc a b)} (h : G.inner (p.1, ↑p.2) = G'.inner (p.1, ↑p.2)) : (restrictIcc a b G).inner p = (restrictIcc a b G').inner p

The restriction of G to M × [a, b] at (x, t) only depends on G at (x, t).