Chart Gram matrices of a Riemannian metric

This file constructs the Gram matrix of the metric supplied by a RiemannianBundle instance in the local frame induced by a tangent-bundle trivialization and proves that its entries and the entries of its inverse are smooth on the trivialization base set. The construction uses Bundle.Trivialization.localFrame and Bundle.Trivialization.basisAt, so it applies unchanged when the model space has dimension zero.

The Gram-matrix and inverse-matrix declarations are adapted from stages 1--5 of the Apache-2.0 Poincare-Conjecture source file DoCarmoLib/Riemannian/TensorBundle/MusicalIso.lean, revision 24f32e4d600878bfaac6bc2f2f9324175571c321. That source uses an explicit metric and a custom chart frame; here the metric supplied by Mathlib's RiemannianBundle instance and its local-frame API replace them.

Main definitions and results

• Riemannian.Tensor.chartLocalFrame and Riemannian.Tensor.chartLocalFrame_def: the frame induced by the tangent trivialization at a chart centre and Module.finBasis, and its identification with that trivialization's local frame.
• Riemannian.Tensor.chartGramMatrix: the metric Gram matrix in this frame.
• Riemannian.Tensor.posDef_chartGramMatrix: positive-definiteness on the base set.
• Riemannian.Tensor.chartGramMatrix_det_pos: strict positivity of its determinant there.
• Riemannian.Tensor.contMDiffOn_chartGramMatrix_entry: smoothness of Gram-matrix entries.
• Riemannian.Tensor.chartInvGramMatrix: the inverse Gram matrix.
• Riemannian.Tensor.contMDiffOn_chartInvGramMatrix_entry: smoothness of inverse entries.

References

• Geodesics, the exponential map, and the Hopf--Rinow theorem roadmap, Layer 1, "Regularity of the Levi-Civita connection".
• M. P. do Carmo, Riemannian Geometry, Chapter 2.
• Poincare-Conjecture, DoCarmoLib/Riemannian/TensorBundle/MusicalIso.lean, stages 1--5, revision 24f32e4d600878bfaac6bc2f2f9324175571c321 (Apache-2.0).

noncomputable def Riemannian.Tensor.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] (α : M) : Fin (Module.finrank ℝ E) → (x : M) → TangentSpace I x

The chart-local frame obtained from the tangent-bundle trivialization centred at α and the chosen Module.finBasis basis of the model space. Outside the trivialization base set it has Mathlib's standard junk value 0.

Equations

• Riemannian.Tensor.chartLocalFrame α = (trivializationAt E (TangentSpace I) α).localFrame (Module.finBasis ℝ E)

theorem Riemannian.Tensor.chartLocalFrame_def {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] (α : M) : chartLocalFrame α = (trivializationAt E (TangentSpace I) α).localFrame (Module.finBasis ℝ E)

The chart-local frame is the local frame of the tangent trivialization at α for the Module.finBasis basis. This unfolds Riemannian.Tensor.chartLocalFrame outside the module where it is defined.

@[simp]

theorem Riemannian.Tensor.chartLocalFrame_apply_of_mem_chart_source {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] (α : M) {x : M} (hx : x ∈ (chartAt H α).source) (i : Fin (Module.finrank ℝ E)) : chartLocalFrame α i x = ((trivializationAt E (TangentSpace I) α).basisAt (Module.finBasis ℝ E) ⋯) i

On the chart source, the local frame agrees with the basis supplied by the tangent trivialization. The source membership is the simplified form of the trivialization base set.

theorem Riemannian.Tensor.contMDiffOn_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] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] (α : M) (i : Fin (Module.finrank ℝ E)) : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) n (fun (x : M) => ⟨x, chartLocalFrame α i x⟩) (trivializationAt E (TangentSpace I) α).baseSet

Each member of chartLocalFrame is C^n on the tangent-trivialization base set.

noncomputable def Riemannian.Tensor.chartGramMatrix {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) : Matrix (Fin (Module.finrank ℝ E)) (Fin (Module.finrank ℝ E)) ℝ

The Gram matrix of chartLocalFrame α for the fiber inner product supplied by the RiemannianBundle instance at x. Its entries are the coordinate metric coefficients used in do Carmo, Riemannian Geometry, Chapter 2.

Equations

• Riemannian.Tensor.chartGramMatrix α x = Matrix.gram ℝ fun (i : Fin (Module.finrank ℝ E)) => Riemannian.Tensor.chartLocalFrame α i x

@[simp]

theorem Riemannian.Tensor.chartGramMatrix_apply {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) (i j : Fin (Module.finrank ℝ E)) : chartGramMatrix α x i j = inner ℝ (chartLocalFrame α i x) (chartLocalFrame α j x)

An entry of the chart Gram matrix is the inner product of the corresponding frame vectors.

theorem Riemannian.Tensor.posDef_chartGramMatrix {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] (α : M) {x : M} (hx : x ∈ (trivializationAt E (TangentSpace I) α).baseSet) : (chartGramMatrix α x).PosDef

The Gram matrix of the chart-local frame is positive-definite on the tangent-trivialization base set.

theorem Riemannian.Tensor.chartGramMatrix_det_pos {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] (α : M) {x : M} (hx : x ∈ (trivializationAt E (TangentSpace I) α).baseSet) : 0 < (chartGramMatrix α x).det

The determinant of the chart Gram matrix is strictly positive on the tangent-trivialization base set.

theorem Riemannian.Tensor.contMDiffOn_chartGramMatrix_entry {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] (α : M) (i j : Fin (Module.finrank ℝ E)) : ContMDiffOn I (modelWithCornersSelf ℝ ℝ) n (fun (x : M) => chartGramMatrix α x i j) (trivializationAt E (TangentSpace I) α).baseSet

Every entry of the chart Gram matrix is C^n on the tangent-trivialization base set.

noncomputable def Riemannian.Tensor.chartInvGramMatrix {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) : Matrix (Fin (Module.finrank ℝ E)) (Fin (Module.finrank ℝ E)) ℝ

The inverse coordinate-metric matrix from do Carmo, Riemannian Geometry, Chapter 2. On the tangent-trivialization base set this is the inverse of a positive-definite matrix.

Equations

• Riemannian.Tensor.chartInvGramMatrix α x = (Riemannian.Tensor.chartGramMatrix α x)⁻¹

@[simp]

theorem Riemannian.Tensor.chartInvGramMatrix_mul_chartGramMatrix {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] (α : M) {x : M} (hx : x ∈ (chartAt H α).source) : chartInvGramMatrix α x * chartGramMatrix α x = 1

On the chart source, the inverse Gram matrix is a left inverse.

@[simp]

theorem Riemannian.Tensor.chartGramMatrix_mul_chartInvGramMatrix {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] (α : M) {x : M} (hx : x ∈ (chartAt H α).source) : chartGramMatrix α x * chartInvGramMatrix α x = 1

On the chart source, the inverse Gram matrix is a right inverse.

theorem Riemannian.Tensor.contMDiffOn_chartInvGramMatrix_entry {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] (α : M) (i j : Fin (Module.finrank ℝ E)) : ContMDiffOn I (modelWithCornersSelf ℝ ℝ) n (fun (x : M) => chartInvGramMatrix α x i j) (trivializationAt E (TangentSpace I) α).baseSet

Every entry of the inverse chart Gram matrix is C^n on the tangent-trivialization base set.