The Levi-Civita connection of an isometric immersion

Let f : M → F be a C² map from a Riemannian manifold to a real inner product space whose differential preserves inner products, ⟪v, w⟫ = ⟪df v, df w⟫. For a vector field Y on M, df Y : y ↦ df_y (Y y) is an F-valued function on M, and D_X (df Y) denotes its derivative along a vector field X. The Gauss formula says that the Levi-Civita connection of M is the tangential part of this ambient derivative:

⟪∇_X Y, w⟫ = ⟪D_X (df Y), df w⟫ for every tangent vector w.

Equivalently, df (∇_X Y) is the orthogonal projection of D_X (df Y) onto the image of df. This computes the connection of a submanifold of Euclidean space, such as the round sphere, from ordinary derivatives in the ambient space.

The proof evaluates the Koszul formula: the derivative of ⟪Y, Z⟫ = ⟪df Y, df Z⟫ follows the product rule TauCeti.mvfderiv_inner_apply, and df [X, Y] = D_X (df Y) - D_Y (df X) by mvfderiv_mlieBracket.

Main result

• CovariantDerivative.IsLeviCivitaConnection.inner_apply_eq_inner_mvfderiv: the Gauss formula.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Theorem 8.2 (the Gauss formula) and Theorem 5.10 (the Koszul formula).
• M. P. do Carmo, Riemannian Geometry, Birkhäuser (1992), Chapter 6, §2.

theorem CovariantDerivative.IsLeviCivitaConnection.inner_apply_eq_inner_mvfderiv {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {f : M → F} {x : M} (h : IsLeviCivitaConnection I cov) (hf : ContMDiffAt I (modelWithCornersSelf ℝ F) 2 f x) (hg : ∀ (y : M) (v w : TangentSpace I y), inner ℝ v w = inner ℝ ((d% f y) v) ((d% f y) w)) {X Y : (y : M) → TangentSpace I y} (hX : (MDiffAt fun (y : M) => ⟨y, X y⟩) x) (hY : (MDiffAt fun (y : M) => ⟨y, Y y⟩) x) (w : TangentSpace I x) : inner ℝ ((↑cov Y x) (X x)) w = inner ℝ (((d% fun (y : M) => (d% f y) (Y y)) x) (X x)) ((d% f x) w)

The Gauss formula. If f : M → F is a C² map into a real inner product space whose differential preserves inner products, then ⟪∇_X Y, w⟫ = ⟪D_X (df Y), df w⟫ for a Levi-Civita connection ∇: it is the tangential part of the ambient derivative of df Y : y ↦ df_y (Y y).