Smoothness of the musical isomorphisms of a nondegenerate metric

A smooth nondegenerate metric g on a manifold with finite-dimensional model space is, read as a section of Hom(TM, T*M), its own flat musical map, so the flat map is smooth by definition. This file proves that the inverse sharp map is smooth as well: the fibrewise inverses of g form a smooth section of Hom(T*M, TM). In a bundle chart this is the smoothness of the inverse of the metric matrix, obtained from smoothness of inversion of continuous linear maps. No positivity is assumed.

Consequently the sharp of a C^n covector field is a C^n vector field. This is the regularity input needed to turn the Koszul functional of an indefinite metric into a covariant derivative. For a Riemannian metric, the corresponding statement for the Riesz dual is Riemannian.Tensor.contMDiffOn_rieszDual.

Main results

• TauCeti.Manifold.ContMDiffNondegenerateMetric.isInvertible: each fibre map g x is invertible.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.inverse_apply: its inverse is the sharp map.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.contMDiff_inverse: the fibrewise inverses form a smooth section of Hom(T*M, TM).
• TauCeti.Manifold.ContMDiffNondegenerateMetric.contMDiffWithinAt_sharp and its variants: the sharp of a C^n covector field is a C^n vector field, for n ≤ ∞.

References

• B. O'Neill, Semi-Riemannian Geometry, Academic Press, 1983, Chapter 3.
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isInvertible {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 (↑⊤) M] (g : ContMDiffNondegenerateMetric) (x : M) : (g.toContMDiffSection x).IsInvertible

The flat map g x : T_x M →L[ℝ] T_x^* M of a nondegenerate metric is invertible.

@[simp]

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.inverse_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 (↑⊤) M] (g : ContMDiffNondegenerateMetric) (x : M) (φ : TangentSpace I x →L[ℝ] ℝ) : (g.toContMDiffSection x).inverse φ = (g.sharp x) ↑φ

The inverse of the flat map g x is the sharp musical isomorphism.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.contMDiff_inverse {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 (↑⊤) M] (g : ContMDiffNondegenerateMetric) : ContMDiff I (I.prod (modelWithCornersSelf ℝ ((E →L[ℝ] ℝ) →L[ℝ] E))) ↑⊤ fun (x : M) => ⟨x, (g.toContMDiffSection x).inverse⟩

The fibrewise inverses of a smooth nondegenerate metric form a smooth section of the bundle Hom(T*M, TM). Equivalently, the sharp musical isomorphism is smooth in bundle charts.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.contMDiffWithinAt_sharp {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 (↑⊤) M] (g : ContMDiffNondegenerateMetric) {n : WithTop ℕ∞} {Φ : (x : M) → TangentSpace I x →L[ℝ] ℝ} {s : Set M} {x : M} (hn : n ≤ ↑⊤) (hΦ : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) n (fun (y : M) => ⟨y, Φ y⟩) s x) : ContMDiffWithinAt I (I.prod (modelWithCornersSelf ℝ E)) n (fun (y : M) => ⟨y, (g.sharp y) ↑(Φ y)⟩) s x

The sharp of a C^n covector field is a C^n vector field, for n ≤ ∞.

We give here a version of this statement within a set at a point.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.contMDiffAt_sharp {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 (↑⊤) M] (g : ContMDiffNondegenerateMetric) {n : WithTop ℕ∞} {Φ : (x : M) → TangentSpace I x →L[ℝ] ℝ} {x : M} (hn : n ≤ ↑⊤) (hΦ : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) n (fun (y : M) => ⟨y, Φ y⟩) x) : ContMDiffAt I (I.prod (modelWithCornersSelf ℝ E)) n (fun (y : M) => ⟨y, (g.sharp y) ↑(Φ y)⟩) x

The sharp of a C^n covector field is a C^n vector field, for n ≤ ∞.

We give here a version of this statement at a point.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.contMDiffOn_sharp {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 (↑⊤) M] (g : ContMDiffNondegenerateMetric) {n : WithTop ℕ∞} {Φ : (x : M) → TangentSpace I x →L[ℝ] ℝ} {s : Set M} (hn : n ≤ ↑⊤) (hΦ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) n (fun (y : M) => ⟨y, Φ y⟩) s) : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ E)) n (fun (y : M) => ⟨y, (g.sharp y) ↑(Φ y)⟩) s

The sharp of a C^n covector field is a C^n vector field, for n ≤ ∞.

We give here a version of this statement on a set.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.contMDiff_sharp {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 (↑⊤) M] (g : ContMDiffNondegenerateMetric) {n : WithTop ℕ∞} {Φ : (x : M) → TangentSpace I x →L[ℝ] ℝ} (hn : n ≤ ↑⊤) (hΦ : ContMDiff I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) n fun (y : M) => ⟨y, Φ y⟩) : ContMDiff I (I.prod (modelWithCornersSelf ℝ E)) n fun (y : M) => ⟨y, (g.sharp y) ↑(Φ y)⟩

The sharp of a C^n covector field is a C^n vector field, for n ≤ ∞.