The norm of covectors on a Riemannian manifold

A Riemannian metric g on a finite-dimensional manifold M induces a norm on each cotangent space T*ₓM: the operator norm of a covector p for the norm of g on TₓM, which is the norm of its Riesz dual, ‖p‖² = p(p♯). This file studies the function z ↦ ‖z.2‖ on the total space of the cotangent bundle T*M = TauCeti.CotangentBundle I M.

In the chart-local frame (eᵢ) of TM at a point, ‖p‖² = Σᵢⱼ gⁱʲ p(eᵢ) p(eⱼ), where gⁱʲ is the inverse Gram matrix of the frame. The components p(eᵢ) are the bundle coordinates of p, so this formula shows that z ↦ ‖z.2‖² is C^n on T*M when g is (TauCeti.CotangentBundle.contMDiff_norm_snd_sq). Consequently the norm itself is continuous, and C^n away from the zero section.

Along the fibre ray t ↦ t • z the norm is t ↦ |t| ‖z.2‖, so its differential does not vanish off the zero section: every nonzero value is a regular value of z ↦ ‖z.2‖ (TauCeti.CotangentBundle.isRegularValue_norm_snd). Its levels are the cosphere bundles of g, which are therefore smooth hypersurfaces of T*M when M has no boundary.

Main results

• TauCeti.CotangentBundle.contMDiff_norm_snd_sq: the squared norm of covectors is as smooth as the metric.
• TauCeti.CotangentBundle.continuous_norm_snd: the norm of covectors is continuous on T*M.
• TauCeti.CotangentBundle.contMDiffAt_norm_snd: it is as smooth as the metric off the zero section.
• TauCeti.CotangentBundle.mfderiv_norm_snd_vectorBundleEulerField: the differential of the norm sends the Euler vector field p ∂_p to the norm.
• TauCeti.CotangentBundle.isRegularPoint_norm_snd and TauCeti.CotangentBundle.isRegularValue_norm_snd: every covector other than zero is a regular point, and every nonzero value a regular value.

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.2 (unit cotangent bundles).
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (the metric on covectors).

theorem TauCeti.CotangentBundle.contMDiff_norm_snd_sq {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] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] [IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x] : ContMDiff (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) (modelWithCornersSelf ℝ ℝ) n fun (z : CotangentBundle I M) => ‖z.snd‖ ^ 2

The squared norm of covectors is smooth. For a C^n Riemannian metric, the function z ↦ ‖z.2‖² on the cotangent bundle is C^n.

theorem TauCeti.CotangentBundle.contMDiffAt_norm_snd {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] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] [IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x] {z : CotangentBundle I M} (hz : z.snd ≠ 0) : ContMDiffAt (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) (modelWithCornersSelf ℝ ℝ) n (fun (z : CotangentBundle I M) => ‖z.snd‖) z

Off the zero section, the norm of covectors is as smooth as the metric.

theorem TauCeti.CotangentBundle.continuous_norm_snd {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] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 0 E fun (x : M) => TangentSpace I x] : Continuous fun (z : CotangentBundle I M) => ‖z.snd‖

The norm of covectors is continuous on the cotangent bundle of a manifold with a continuous Riemannian metric.

theorem TauCeti.CotangentBundle.mfderiv_norm_snd_vectorBundleEulerField {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] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {z : CotangentBundle I M} (hz : z.snd ≠ 0) : ((mfderiv% fun (z : CotangentBundle I M) => ‖z.snd‖) z) (vectorBundleEulerField I z) = ‖z.snd‖

The norm of covectors along the Euler vector field. At a covector z other than zero, the differential of z ↦ ‖z.2‖ sends the Euler vector field p ∂_p to ‖z.2‖: along the fibre ray t ↦ t • z the norm is t ↦ |t| ‖z.2‖.

theorem TauCeti.CotangentBundle.isRegularPoint_norm_snd {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] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {z : CotangentBundle I M} (hz : z.snd ≠ 0) : IsRegularPoint (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) (modelWithCornersSelf ℝ ℝ) (fun (z : CotangentBundle I M) => ‖z.snd‖) z

Covectors other than zero are regular points of the norm. Every covector z with z.2 ≠ 0 is a regular point of z ↦ ‖z.2‖.

theorem TauCeti.CotangentBundle.isRegularValue_norm_snd {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] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {c : ℝ} (hc : c ≠ 0) : IsRegularValue (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) (modelWithCornersSelf ℝ ℝ) (fun (z : CotangentBundle I M) => ‖z.snd‖) c

Every nonzero value is a regular value of the norm of covectors. Its levels are the cosphere bundles of the metric.