Covariant differentiation on a parametrized surface

A parametrized surface in a manifold M is a map f of two scalar parameters, here written in curried form so that f u and fun q ↦ f q v are the two families of parameter curves through the point f u v. Each family carries a velocity field: fun r ↦ γ'(u) for γ = fun q ↦ f q r is a section of the tangent bundle along the curve f u, and symmetrically with the two parameters exchanged. These are the fields written ∂f/∂u and ∂f/∂v in the classical notation, and differentiating them covariantly along the other parameter curve is the two-parameter operation on which variational arguments rest.

This file computes that mixed derivative in a chart and proves that it is symmetric in the two parameters: D/∂v (∂f/∂u) = D/∂u (∂f/∂v) for a torsion-free connection. In a chart the mixed derivative is ∂²f/∂v∂u + Γ (∂f/∂u, ∂f/∂v), so the symmetry comes from two independent symmetries: iterated partial derivatives of the chart reading commute, and the Christoffel map of a torsion-free connection is a symmetric bilinear map. Both partial velocity fields are read through the moving-chart operator CovariantDerivative.alongCurve of AlongCurve/Basic.lean.

The symmetry is what lets the radial derivative of a family exp_p (t • v s) be exchanged with its transverse derivative, and in that form it is the step behind the Gauss lemma and the first-variation formula for the energy of a curve.

Main results

• CovariantDerivative.alongCurveInChartWithin_curveVelocity_fst and CovariantDerivative.alongCurveInChartWithin_curveVelocity_snd: the moving-chart coordinate formula for the field of first-parameter velocities along a second-parameter curve is the classical expression ∂²f/∂v∂u + Γ (∂f/∂u, ∂f/∂v), and symmetrically with the two parameters exchanged.
• ContMDiffAt.differentiableAt_sectionCoord_curveVelocity_fst and ContMDiffAt.differentiableAt_sectionCoord_curveVelocity_snd: the corresponding coordinate readings are differentiable when the surface is C².
• CovariantDerivative.alongCurve_curveVelocity_comm: the symmetry lemma, that for a torsion-free connection the two mixed covariant derivatives of a C² parametrized surface agree.

References

• M. P. do Carmo, Riemannian Geometry, Birkhauser, 1992, Ch. 3, §3, Lemma 3.4, the symmetry lemma preceding the Gauss lemma.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2nd ed., 2018, Lemma 6.2.

theorem CovariantDerivative.alongCurveInChartWithin_curveVelocity_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] {f : 𝕜 → 𝕜 → M} {u v : 𝕜} {x : M} (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (hf : ContMDiffAt (modelWithCornersSelf 𝕜 (𝕜 × 𝕜)) I 1 (fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, v)) (hx : f u v ∈ (trivializationAt E (TangentSpace I) x).baseSet) : cov.alongCurveInChartWithin (f u) (fun (r : 𝕜) => TauCeti.Manifold.curveVelocity I (fun (q : 𝕜) => f q r) u) Set.univ x v = deriv (fun (r : 𝕜) => deriv (fun (q : 𝕜) => ↑(extChartAt I x) (f q r)) u) v + ((TauCeti.Manifold.christoffelMap (Module.finBasis 𝕜 E) ⋯ (f u v)) (deriv (fun (q : 𝕜) => ↑(extChartAt I x) (f q v)) u)) (deriv (fun (r : 𝕜) => ↑(extChartAt I x) (f u r)) v)

The chart formula for the mixed derivative of a parametrized surface. Reading the surface f in the extended chart at x, the moving-chart coordinate formula for the field of first-parameter velocities along the second-parameter curve f u is the classical second-order expression ∂²f/∂v∂u + Γ (∂f/∂u, ∂f/∂v). The chart need not be the one centred at the point f u v of the surface.

theorem CovariantDerivative.alongCurveInChartWithin_curveVelocity_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] {f : 𝕜 → 𝕜 → M} {u v : 𝕜} {x : M} (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (hf : ContMDiffAt (modelWithCornersSelf 𝕜 (𝕜 × 𝕜)) I 1 (fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, v)) (hx : f u v ∈ (trivializationAt E (TangentSpace I) x).baseSet) : cov.alongCurveInChartWithin (fun (q : 𝕜) => f q v) (fun (q : 𝕜) => TauCeti.Manifold.curveVelocity I (f q) v) Set.univ x u = deriv (fun (q : 𝕜) => deriv (fun (r : 𝕜) => ↑(extChartAt I x) (f q r)) v) u + ((TauCeti.Manifold.christoffelMap (Module.finBasis 𝕜 E) ⋯ (f u v)) (deriv (fun (r : 𝕜) => ↑(extChartAt I x) (f u r)) v)) (deriv (fun (q : 𝕜) => ↑(extChartAt I x) (f q v)) u)

The chart formula for the mixed derivative of a parametrized surface, with the two parameters exchanged: the moving-chart coordinate formula for the field of second-parameter velocities along the first-parameter curve fun q ↦ f q v is ∂²f/∂u∂v + Γ (∂f/∂v, ∂f/∂u). The chart need not be the one centred at the point f u v of the surface.

theorem CovariantDerivative.alongCurve_curveVelocity_comm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [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] [ContMDiffVectorBundle 1 E (TangentSpace I) I] {f : 𝕜 → 𝕜 → M} {u v : 𝕜} [IsManifold I (minSmoothness 𝕜 2) M] (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (hcov : cov.IsTorsionFree) (hf : ContMDiffAt (modelWithCornersSelf 𝕜 (𝕜 × 𝕜)) I (minSmoothness 𝕜 2) (fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, v)) : cov.alongCurve (f u) (fun (r : 𝕜) => TauCeti.Manifold.curveVelocity I (fun (q : 𝕜) => f q r) u) v = cov.alongCurve (fun (q : 𝕜) => f q v) (fun (q : 𝕜) => TauCeti.Manifold.curveVelocity I (f q) v) u

The symmetry lemma. For a torsion-free connection and a parametrized surface f which is smooth enough at (u, v) for its chart reading to have a symmetric second derivative, the covariant derivative along f u of the first-parameter velocity field agrees with the covariant derivative along fun q ↦ f q v of the second-parameter velocity field: in the classical notation, D/∂v (∂f/∂u) = D/∂u (∂f/∂v).

theorem ContMDiffAt.differentiableAt_sectionCoord_curveVelocity_fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : 𝕜 → 𝕜 → M} {u v : 𝕜} {x : M} [IsManifold I 2 M] (hf : ContMDiffAt (modelWithCornersSelf 𝕜 (𝕜 × 𝕜)) I 2 (fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, v)) (hx : f u v ∈ (trivializationAt E (TangentSpace I) x).baseSet) : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord (f u) (fun (r : 𝕜) => TauCeti.Manifold.curveVelocity I (fun (q : 𝕜) => f q r) u) x) v

The coordinate reading of the first-parameter velocity field of a C² parametrized surface is differentiable along the second-parameter curve.

theorem ContMDiffAt.differentiableAt_sectionCoord_curveVelocity_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : 𝕜 → 𝕜 → M} {u v : 𝕜} {x : M} [IsManifold I 2 M] (hf : ContMDiffAt (modelWithCornersSelf 𝕜 (𝕜 × 𝕜)) I 2 (fun (z : 𝕜 × 𝕜) => f z.1 z.2) (u, v)) (hx : f u v ∈ (trivializationAt E (TangentSpace I) x).baseSet) : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord (fun (q : 𝕜) => f q v) (fun (q : 𝕜) => TauCeti.Manifold.curveVelocity I (f q) v) x) u

The coordinate reading of the second-parameter velocity field of a C² parametrized surface is differentiable along the first-parameter curve.