Riemannian metrics induced by immersions into inner product spaces

A C^(n+1) map f : M → F from a finite-dimensional manifold to a real inner product space whose differential is injective at every point pulls the inner product of F back to a C^n Riemannian metric on M:

g_x(v, w) = ⟪df_x v, df_x w⟫.

This is the first fundamental form of an immersed submanifold of Euclidean space, and the way the classical model spaces such as the round sphere receive their metrics.

Main definitions

• TauCeti.inducedRiemannianMetric: the C^n Riemannian metric induced by such a map.

Main statements

• TauCeti.inducedRiemannianMetric_inner: the induced inner product of two tangent vectors is the inner product of their images under the differential.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (induced metrics on immersed submanifolds).

theorem TauCeti.instIsNormableSpaceRealTangentSpace_tauCeti {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (x : M) : IsNormableSpace ℝ (TangentSpace I x)

Mathlib's derived IsNormableSpace instance on TangentSpace I x is stated with the model space's Module instance instead of the tangent space's own one, so instance search never finds it; restate it against the tangent space's structure.

noncomputable def TauCeti.inducedRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n : WithTop ℕ∞} [FiniteDimensional ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (f : M → F) (hf : ContMDiff I (modelWithCornersSelf ℝ F) (n + 1) f) (hinj : ∀ (x : M), Function.Injective ⇑(d% f x)) : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x

The Riemannian metric induced on M by a C^(n+1) map f : M → F into a real inner product space whose differential is injective at every point: the inner product of two tangent vectors is the inner product of their images under the differential mvfderiv I f x of f, read in F.

@[simp]

theorem TauCeti.inducedRiemannianMetric_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n : WithTop ℕ∞} [FiniteDimensional ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] (f : M → F) (hf : ContMDiff I (modelWithCornersSelf ℝ F) (n + 1) f) (hinj : ∀ (x : M), Function.Injective ⇑(d% f x)) (x : M) (v w : TangentSpace I x) : (((inducedRiemannianMetric f hf hinj).inner x) v) w = inner ℝ ((d% f x) v) ((d% f x) w)

The induced inner product of two tangent vectors is the inner product of their images under the differential.