Smoothness of the fibrewise Riesz dual

This file proves that the inverse of the fibrewise Fréchet–Riesz equivalence of a smooth finite-dimensional Riemannian bundle carries smoothly varying covectors to a smooth section. In a chart-local frame, its coefficients are obtained by multiplying the covector evaluations by the inverse Gram matrix.

The result is the linear-algebraic input needed to construct the Levi–Civita connection from the Koszul functional: the Koszul formula first produces a covector in the last argument, and the fibrewise Riesz dual turns it into the value of the connection.

The coordinate formula and smoothness argument are adapted from stages 6–7 of the Apache-2.0 Poincare-Conjecture source file DoCarmoLib/Riemannian/TensorBundle/MusicalIso.lean, revision 24f32e4d600878bfaac6bc2f2f9324175571c321. The source uses an explicit metric and manually trivializes the resulting section. Here Mathlib's fibrewise InnerProductSpace.toDual and local frame smoothness API replace those constructions.

Main results

• Riemannian.Tensor.rieszDual is the fibrewise Riesz equivalence supplied by the canonical metric.
• Riemannian.Tensor.rieszDual_eq_sum_chartLocalFrame gives the inverse-Gram-matrix coordinate formula for the Riesz dual.
• Riemannian.Tensor.norm_sq_eq_apply_rieszDual and Riemannian.Tensor.norm_sq_eq_dotProduct_chartInvGramMatrix_mulVec express the squared norm of a covector as its value on its Riesz dual, and in coordinates through the inverse Gram matrix.
• Riemannian.Tensor.contMDiffOn_rieszDual proves smoothness on a chart domain from smoothness of the covector's evaluations on the chart-local frame.
• Riemannian.Tensor.contMDiffAt_rieszDual is the corresponding pointwise criterion.

Since rieszDual is the fibrewise equivalence itself, its linearity in the functional is Mathlib's LinearIsometryEquiv API (map_add, map_smul, LinearIsometryEquiv.map_zero).

References

• M. P. do Carmo, Riemannian Geometry, Chapter 2.
• Poincare-Conjecture, DoCarmoLib/Riemannian/TensorBundle/MusicalIso.lean, stages 6–7, revision 24f32e4d600878bfaac6bc2f2f9324175571c321 (Apache-2.0).

noncomputable def Riemannian.Tensor.rieszDual {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] (x : M) : (TangentSpace I x →L[ℝ] ℝ) ≃ₗᵢ[ℝ] TangentSpace I x

The fibrewise Fréchet–Riesz equivalence of a tangent fibre: it sends a continuous linear functional to the vector representing it for the inner product supplied by the canonical Riemannian bundle instance. This packages InnerProductSpace.toDual together with the finite-dimensionality and completeness of the fibre, neither of which is available to instance search on TangentSpace I x.

@[simp]

theorem Riemannian.Tensor.inner_rieszDual {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] {x : M} (φ : TangentSpace I x →L[ℝ] ℝ) (v : TangentSpace I x) : inner ℝ ((rieszDual x) φ) v = φ v

The Riesz dual represents its functional by the fibre inner product.

theorem Riemannian.Tensor.eq_rieszDual_iff_inner_eq {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] {x : M} {v : TangentSpace I x} {φ : TangentSpace I x →L[ℝ] ℝ} : v = (rieszDual x) φ ↔ ∀ (w : TangentSpace I x), inner ℝ v w = φ w

A tangent vector is the Riesz dual of φ exactly when its inner product against every vector is the value of φ there.

theorem Riemannian.Tensor.rieszDual_eq_sum_chartLocalFrame {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] (a : M) {x : M} (hx : x ∈ (chartAt H a).source) (φ : TangentSpace I x →L[ℝ] ℝ) : (rieszDual x) φ = ∑ i : Fin (Module.finrank ℝ E), (chartInvGramMatrix a x).mulVec (fun (j : Fin (Module.finrank ℝ E)) => φ (chartLocalFrame a j x)) i • chartLocalFrame a i x

The coordinate formula for the fibrewise Riesz dual in a chart-local frame. Its coefficient vector is the inverse Gram matrix applied to the evaluations of the covector on the frame.

theorem Riemannian.Tensor.norm_sq_eq_apply_rieszDual {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] {x : M} (φ : TangentSpace I x →L[ℝ] ℝ) : ‖φ‖ ^ 2 = φ ((rieszDual x) φ)

The squared norm of a covector is its value on its Riesz dual.

theorem Riemannian.Tensor.norm_sq_eq_dotProduct_chartInvGramMatrix_mulVec {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] (a : M) {x : M} (hx : x ∈ (chartAt H a).source) (φ : TangentSpace I x →L[ℝ] ℝ) : ‖φ‖ ^ 2 = (fun (j : Fin (Module.finrank ℝ E)) => φ (chartLocalFrame a j x)) ⬝ᵥ (chartInvGramMatrix a x).mulVec fun (j : Fin (Module.finrank ℝ E)) => φ (chartLocalFrame a j x)

The coordinate formula for the squared norm of a covector: in a chart-local frame it is the quadratic form of the inverse Gram matrix on the components φ (eⱼ) of the covector.

theorem Riemannian.Tensor.contMDiffOn_rieszDual {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] (a : M) {Φ : (y : M) → TangentSpace I y →L[ℝ] ℝ} (hΦ : ∀ (j : Fin (Module.finrank ℝ E)), ContMDiffOn I (modelWithCornersSelf ℝ ℝ) n (fun (y : M) => (Φ y) (chartLocalFrame a j y)) (chartAt H a).source) : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) n (fun (y : M) => ⟨y, (rieszDual y) (Φ y)⟩) (chartAt H a).source

A field of covectors has a smooth fibrewise Riesz dual on a chart source if its evaluations on the chart-local frame are smooth there.

theorem Riemannian.Tensor.contMDiffAt_rieszDual {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] (a : M) {x : M} (hx : x ∈ (chartAt H a).source) {Φ : (y : M) → TangentSpace I y →L[ℝ] ℝ} (hΦ : ∀ (j : Fin (Module.finrank ℝ E)), ContMDiffAt I (modelWithCornersSelf ℝ ℝ) n (fun (y : M) => (Φ y) (chartLocalFrame a j y)) x) : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ E)) n (fun (y : M) => ⟨y, (rieszDual y) (Φ y)⟩) x

Pointwise version of contMDiffOn_rieszDual: smoothness of the frame evaluations at a point in a chart source implies smoothness of the fibrewise Riesz-dual section there.