diff --git a/Physlib.lean b/Physlib.lean index 580bb2490..48f3f665b 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -57,7 +57,10 @@ public import Physlib.Mathematics.Distribution.PowMul public import Physlib.Mathematics.FDerivCurry public import Physlib.Mathematics.Fin public import Physlib.Mathematics.Fin.Involutions +public import Physlib.Mathematics.Geometry.Metric.Lorentzian.Defs +public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Basic public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs +public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.MetricTensorCotangent public import Physlib.Mathematics.Geometry.Metric.Riemannian.Defs public import Physlib.Mathematics.InnerProductSpace.Adjoint public import Physlib.Mathematics.InnerProductSpace.Basic diff --git a/Physlib/Mathematics/Geometry/Metric/Lorentzian/Defs.lean b/Physlib/Mathematics/Geometry/Metric/Lorentzian/Defs.lean new file mode 100644 index 000000000..b00adb054 --- /dev/null +++ b/Physlib/Mathematics/Geometry/Metric/Lorentzian/Defs.lean @@ -0,0 +1,58 @@ +/- +Copyright (c) 2026 Matteo Cipollina. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Matteo Cipollina +-/ +module + +public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs +public import Mathlib.Geometry.Manifold.VectorBundle.Tangent +public import Mathlib.LinearAlgebra.QuadraticForm.Signature + +/-! +# Lorentzian metrics + +This file records the Lorentzian condition (index `1`) for a pseudo-Riemannian metric. + +We adopt the mathematical, or "mostly plus", convention: a Lorentzian metric has exactly one +negative direction, corresponding to signature `(-, +, ..., +)`. Users working with the physics +"mostly minus" convention should keep in mind that such a metric has negative index `dim - 1` +instead. + +## Main definitions + +* `PseudoRiemannianMetric.IsLorentzianMetric`: the Prop-valued predicate asserting that a + pseudo-Riemannian metric has index `1` at every point. + +## Tags + +Lorentzian, pseudo-Riemannian, index +-/ + +@[expose] public section + +namespace PseudoRiemannianMetric + +noncomputable section + +variable {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] +variable {H : Type w} [TopologicalSpace H] +variable {M : Type*} [TopologicalSpace M] [ChartedSpace H M] +variable {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} +variable [IsManifold I (n + 1) M] +variable [∀ x : M, FiniteDimensional ℝ (TangentSpace I x)] + +/-- Predicate asserting that a pseudo-Riemannian metric has index `1` at every point. -/ +class IsLorentzianMetric (g : _root_.PseudoRiemannianMetric E H M n I) : Prop where + /-- A Lorentzian metric has index `1` at every point. -/ + index_eq_one : ∀ x : M, g.index x = 1 + +@[simp] +lemma sigNeg_toQuadraticForm_eq_one (g : _root_.PseudoRiemannianMetric E H M n I) + [IsLorentzianMetric (g := g)] (x : M) : + sigNeg (g.toQuadraticForm x) = 1 := by + simpa [_root_.PseudoRiemannianMetric.index] using IsLorentzianMetric.index_eq_one (g := g) x + +end + +end PseudoRiemannianMetric diff --git a/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Basic.lean b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Basic.lean new file mode 100644 index 000000000..b021d1c25 --- /dev/null +++ b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Basic.lean @@ -0,0 +1,887 @@ +/- +Copyright (c) 2025 Matteo Cipollina. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Matteo Cipollina +-/ +module + +public import Mathlib.Geometry.Manifold.VectorBundle.Riemannian +public import Mathlib.Geometry.Manifold.VectorBundle.Tangent +public import Mathlib.LinearAlgebra.BilinearForm.Properties +public import Mathlib.LinearAlgebra.QuadraticForm.Signature +public import Mathlib.Topology.LocallyConstant.Basic + +/-! +# Pseudo-Riemannian metrics (basic) + +`Bundle` API, the `MetricTensor` structure, and musical isomorphisms through `apply_vec_sharp`. +Cotangent metric and `MetricTensor.index` are in `MetricTensorCotangent.lean`; the +`PseudoRiemannianMetric` structure is in `Defs.lean`. +-/ + +@[expose] public section + +section PseudoRiemannianMetric + +open Bundle Set Finset Function Filter Module Topology ContinuousLinearMap +open scoped Manifold Bundle LinearMap Dual + +/-! ## Bundle-level infrastructure -/ + +namespace Bundle + +/-! ### Fiberwise pseudo-Riemannian structures -/ + +section PseudoRiemannianBundle + +variable + {B : Type*} [TopologicalSpace B] + {E : B → Type*} [∀ x, SeminormedAddCommGroup (E x)] [∀ x, NormedSpace ℝ (E x)] + +/-- A pseudo-Riemannian structure on a family of fibers `E x`: a symmetric, nondegenerate bilinear +form on each fiber, expressed as a continuous bilinear map. -/ +class PseudoRiemannianBundle : Type _ where + /-- The fiberwise pseudo-inner product as a continuous bilinear map. -/ + metric : ∀ x : B, E x →L[ℝ] E x →L[ℝ] ℝ + /-- Symmetry: `gₓ(v,w) = gₓ(w,v)`. -/ + symm : ∀ (x : B) (v w : E x), metric x v w = metric x w v + /-- Nondegeneracy: if `gₓ(v,w)=0` for all `w`, then `v=0`. -/ + nondegenerate : ∀ (x : B) (v : E x), (∀ w : E x, metric x v w = 0) → v = 0 + +variable [PseudoRiemannianBundle (B := B) (E := E)] + +/-- The metric as a family of continuous bilinear maps. -/ +abbrev metric (x : B) : E x →L[ℝ] E x →L[ℝ] ℝ := + PseudoRiemannianBundle.metric (B := B) (E := E) x + +/-- The fiberwise pseudo-inner-product \(g_x(v,w)\). -/ +noncomputable abbrev pseudoInner (x : B) (v w : E x) : ℝ := + (PseudoRiemannianBundle.metric (B := B) (E := E) x) v w + +omit [TopologicalSpace B] in +@[simp] +lemma pseudoInner_def (x : B) (v w : E x) : + pseudoInner (B := B) (E := E) x v w = metric (B := B) (E := E) x v w := + rfl + +omit [TopologicalSpace B] in +lemma pseudoInner_symm (x : B) (v w : E x) : + pseudoInner (B := B) (E := E) x v w = pseudoInner (B := B) (E := E) x w v := by + simpa [pseudoInner] using (PseudoRiemannianBundle.symm (B := B) (E := E) x v w) + +omit [TopologicalSpace B] in +lemma pseudoInner_nondegenerate (x : B) (v : E x) (hv : ∀ w : E x, + pseudoInner (B := B) (E := E) x v w = 0) : + v = 0 := + PseudoRiemannianBundle.nondegenerate (B := B) (E := E) x v hv + +end PseudoRiemannianBundle + +/-! ### Smoothness of pseudo-Riemannian structures on vector bundles -/ + +section ContMDiff + +open scoped ENat + +variable + {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] + {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n n' : WithTop ℕ∞} + {B : Type*} [TopologicalSpace B] [ChartedSpace HB B] + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] + {E : B → Type*} [TopologicalSpace (TotalSpace F E)] [∀ x, SeminormedAddCommGroup (E x)] + [∀ x, NormedSpace ℝ (E x)] + [FiberBundle F E] [VectorBundle ℝ F E] + [PseudoRiemannianBundle (B := B) (E := E)] + +variable (IB n F E) in +/-- A `C^n` pseudo-Riemannian metric along a vector bundle `E → B`, packaged bundle-first. + +This mirrors Mathlib's `Bundle.ContMDiffRiemannianMetric`, but replaces positivity by fiberwise +nondegeneracy. -/ +structure ContMDiffPseudoRiemannianMetric : Type _ where + /-- The fiberwise bilinear form. -/ + metric (b : B) : E b →L[ℝ] E b →L[ℝ] ℝ + /-- Symmetry: `g_b(v,w) = g_b(w,v)`. -/ + symm (b : B) (v w : E b) : metric b v w = metric b w v + /-- Nondegeneracy: if `g_b(v, w) = 0` for all `w`, then `v = 0`. -/ + nondegenerate (b : B) (v : E b) (hv : ∀ w : E b, metric b v w = 0) : v = 0 + /-- Smoothness as a section of the bundle of bilinear forms. -/ + contMDiff : + ContMDiff IB (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) n + (fun b ↦ TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) b (metric b)) + +variable (IB n F E) in +/-- Prop-valued smoothness predicate for a pseudo-Riemannian bundle. + +This is stated as an existence statement (as in Mathlib's `IsContinuousRiemannianBundle`), so it is +Prop-valued in terms of existing bundle data. -/ +class IsContMDiffPseudoRiemannianBundle : Prop where + exists_contMDiff : + ∃ g : ContMDiffPseudoRiemannianMetric (IB := IB) (n := n) (F := F) (E := E), + ∀ (b : B) (v w : E b), pseudoInner (B := B) (E := E) b v w = g.metric b v w + +lemma IsContMDiffPseudoRiemannianBundle.of_le + [h : IsContMDiffPseudoRiemannianBundle (IB := IB) (n := n) (F := F) (E := E)] (h' : n' ≤ n) : + IsContMDiffPseudoRiemannianBundle (IB := IB) (n := n') (F := F) (E := E) := by + rcases h.exists_contMDiff with ⟨g, hg⟩ + refine ⟨⟨?_, ?_⟩⟩ + · refine + { metric := g.metric + symm := g.symm + nondegenerate := g.nondegenerate + contMDiff := g.contMDiff.of_le h' } + · intro b v w + simpa using hg b v w + +instance [IsContMDiffPseudoRiemannianBundle (IB := IB) (n := (1 : WithTop ℕ∞)) (F := F) (E := E)] : + IsContMDiffPseudoRiemannianBundle (IB := IB) (n := (0 : WithTop ℕ∞)) (F := F) (E := E) := + IsContMDiffPseudoRiemannianBundle.of_le (IB := IB) (F := F) (E := E) zero_le_one + +instance [IsContMDiffPseudoRiemannianBundle (IB := IB) (n := (2 : WithTop ℕ∞)) (F := F) (E := E)] : + IsContMDiffPseudoRiemannianBundle (IB := IB) (n := (1 : WithTop ℕ∞)) (F := F) (E := E) := + IsContMDiffPseudoRiemannianBundle.of_le (IB := IB) (F := F) (E := E) one_le_two + +instance [IsContMDiffPseudoRiemannianBundle (IB := IB) (n := (3 : WithTop ℕ∞)) (F := F) (E := E)] : + IsContMDiffPseudoRiemannianBundle (IB := IB) (n := (2 : WithTop ℕ∞)) (F := F) (E := E) := + IsContMDiffPseudoRiemannianBundle.of_le (IB := IB) (n := (3 : WithTop ℕ∞)) (F := F) (E := E) + (by norm_cast) + +namespace ContMDiffPseudoRiemannianMetric + +/-- A smooth pseudo-Riemannian metric along a bundle induces the corresponding fiberwise +structure. -/ +@[reducible] def toPseudoRiemannianBundle + (g : ContMDiffPseudoRiemannianMetric (IB := IB) (n := n) (F := F) (E := E)) : + PseudoRiemannianBundle (B := B) (E := E) where + metric := g.metric + symm := g.symm + nondegenerate := g.nondegenerate + +instance (g : ContMDiffPseudoRiemannianMetric (IB := IB) (n := n) (F := F) (E := E)) : + letI : PseudoRiemannianBundle (B := B) (E := E) := toPseudoRiemannianBundle (IB := IB) (n := n) + (F := F) (E := E) g + IsContMDiffPseudoRiemannianBundle (IB := IB) (n := n) (F := F) (E := E) := + letI : PseudoRiemannianBundle (B := B) (E := E) := toPseudoRiemannianBundle (IB := IB) (n := n) + (F := F) (E := E) g + ⟨⟨g, fun _ _ _ => rfl⟩⟩ + +end ContMDiffPseudoRiemannianMetric + +section ContMDiffPairing + +variable + {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] + {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} + {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] + [h : IsContMDiffPseudoRiemannianBundle (IB := IB) (n := n) (F := F) (E := E)] + {b : M → B} {v w : ∀ x, E (b x)} {s : Set M} {x : M} + +omit [PseudoRiemannianBundle (B := B) (E := E)] h in +/-- Given two smooth maps into the same fibers, their pairing under a smooth pseudo-Riemannian +bundle metric is smooth. -/ +lemma ContMDiffWithinAt.metric_bundle + (g : ContMDiffPseudoRiemannianMetric (IB := IB) (n := n) (F := F) (E := E)) + (hv : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (v m : TotalSpace F E)) s x) + (hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (w m : TotalSpace F E)) s x) : + ContMDiffWithinAt IM 𝓘(ℝ) n (fun m ↦ g.metric (b m) (v m) (w m)) s x := by + have hb : ContMDiffWithinAt IM IB n b s x := by + simp only [contMDiffWithinAt_totalSpace] at hv + exact hv.1 + have : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ)) n + (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) + (g.metric (b m) (v m) (w m))) s x := by + apply ContMDiffWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F) + · exact ContMDiffAt.comp_contMDiffWithinAt x g.contMDiff.contMDiffAt hb + · exact hv + · exact hw + simp only [contMDiffWithinAt_totalSpace] at this + exact this.2 + +/-- Given two smooth maps into the same fibers of a pseudo-Riemannian bundle, their pairing is +smooth. -/ +lemma ContMDiffWithinAt.pseudoInner_bundle + (hv : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (v m : TotalSpace F E)) s x) + (hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (w m : TotalSpace F E)) s x) : + ContMDiffWithinAt IM 𝓘(ℝ) n (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) s x := by + rcases h.exists_contMDiff with ⟨g, hg⟩ + have hpair := ContMDiffWithinAt.metric_bundle (IB := IB) (n := n) (F := F) (E := E) + (b := b) (v := v) (w := w) (s := s) (x := x) g hv hw + have hrewrite : + (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) = + (fun m ↦ g.metric (b m) (v m) (w m)) := by + funext m + simpa [Bundle.pseudoInner] using (hg (b m) (v m) (w m)) + simpa [hrewrite] using hpair + +lemma ContMDiffAt.pseudoInner_bundle + (hv : ContMDiffAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (v m : TotalSpace F E)) x) + (hw : ContMDiffAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (w m : TotalSpace F E)) x) : + ContMDiffAt IM 𝓘(ℝ) n (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) x := + ContMDiffWithinAt.pseudoInner_bundle (IB := IB) (n := n) (F := F) (E := E) hv hw + +lemma ContMDiffOn.pseudoInner_bundle + (hv : ContMDiffOn IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (v m : TotalSpace F E)) s) + (hw : ContMDiffOn IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (w m : TotalSpace F E)) s) : + ContMDiffOn IM 𝓘(ℝ) n (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) s := + fun x hx ↦ (hv x hx).pseudoInner_bundle (IB := IB) (n := n) (F := F) (E := E) (hw x hx) + +lemma ContMDiff.pseudoInner_bundle + (hv : ContMDiff IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (v m : TotalSpace F E))) + (hw : ContMDiff IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ (w m : TotalSpace F E))) : + ContMDiff IM 𝓘(ℝ) n (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) := + fun x ↦ (hv x).pseudoInner_bundle (IB := IB) (n := n) (F := F) (E := E) (hw x) + +end ContMDiffPairing + +section MDifferentiablePairing + +variable + {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] + {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} + {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] + [h : IsContMDiffPseudoRiemannianBundle (IB := IB) (n := (1 : WithTop ℕ∞)) (F := F) (E := E)] + {b : M → B} {v w : ∀ x, E (b x)} {s : Set M} {x : M} + +/-- Given two differentiable maps into the same fibers of a pseudo-Riemannian bundle, their +pairing is differentiable. -/ +lemma MDifferentiableWithinAt.pseudoInner_bundle + (hv : MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (v m : TotalSpace F E)) s x) + (hw : MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (w m : TotalSpace F E)) s x) : + MDifferentiableWithinAt IM 𝓘(ℝ) + (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) s x := by + rcases h.exists_contMDiff with ⟨g, hg⟩ + have hb : MDifferentiableWithinAt IM IB b s x := by + simp only [mdifferentiableWithinAt_totalSpace] at hv + exact hv.1 + have hpair : MDifferentiableWithinAt IM (IB.prod 𝓘(ℝ)) + (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) + (g.metric (b m) (v m) (w m))) s x := by + apply MDifferentiableWithinAt.clm_bundle_apply₂ (F₁ := F) (F₂ := F) + · exact MDifferentiableAt.comp_mdifferentiableWithinAt x + (g.contMDiff.mdifferentiableAt one_ne_zero) hb + · exact hv + · exact hw + have hrewrite : + (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) = + (fun m ↦ g.metric (b m) (v m) (w m)) := by + funext m + simpa [Bundle.pseudoInner] using (hg (b m) (v m) (w m)) + simp only [mdifferentiableWithinAt_totalSpace] at hpair + simpa [hrewrite] using hpair.2 + +lemma MDifferentiableAt.pseudoInner_bundle + (hv : MDifferentiableAt IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (v m : TotalSpace F E)) x) + (hw : MDifferentiableAt IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (w m : TotalSpace F E)) x) : + MDifferentiableAt IM 𝓘(ℝ) + (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) x := + MDifferentiableWithinAt.pseudoInner_bundle (IB := IB) (F := F) (E := E) hv hw + +lemma MDifferentiableOn.pseudoInner_bundle + (hv : MDifferentiableOn IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (v m : TotalSpace F E)) s) + (hw : MDifferentiableOn IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (w m : TotalSpace F E)) s) : + MDifferentiableOn IM 𝓘(ℝ) + (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) s := + fun x hx ↦ (hv x hx).pseudoInner_bundle (IB := IB) (F := F) (E := E) (hw x hx) + +lemma MDifferentiable.pseudoInner_bundle + (hv : MDifferentiable IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (v m : TotalSpace F E))) + (hw : MDifferentiable IM (IB.prod 𝓘(ℝ, F)) (fun m ↦ (w m : TotalSpace F E))) : + MDifferentiable IM 𝓘(ℝ) + (fun m ↦ pseudoInner (B := B) (E := E) (b m) (v m) (w m)) := + fun x ↦ (hv x).pseudoInner_bundle (IB := IB) (F := F) (E := E) (hw x) + +end MDifferentiablePairing + +end ContMDiff + +end Bundle + +/-! ## Quadratic-form helper -/ + +namespace PseudoRiemannianMetric + +/-- Turn a (curried) symmetric bilinear map on a tangent space into the associated quadratic form +`v ↦ val x v v`. + +This is the entry point to quadratic-form invariants (e.g. `QuadraticForm.sigNeg`) from bundled +metric data; compare O'Neill, *Semi-Riemannian Geometry* (1983), p. 47. -/ +noncomputable def valToQuadraticForm + {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] + {H : Type w} [TopologicalSpace H] + {M : Type*} [TopologicalSpace M] [ChartedSpace H M] + {I : ModelWithCorners ℝ E H} + (val : ∀ (x : M), TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ)) + (symm : ∀ (x : M) (v w : TangentSpace I x), (val x v) w = (val x w) v) + (x : M) : QuadraticForm ℝ (TangentSpace I x) where + toFun v := val x v v + toFun_smul a v := by + simp only [ContinuousLinearMap.map_smul, ContinuousLinearMap.smul_apply, smul_smul] + exists_companion' := + ⟨LinearMap.mk₂ ℝ (fun v y => val x v y + val x y v) + (fun v₁ v₂ y => by simp only [map_add, add_apply]; ring) + (fun a v y => by simp only [map_smul, smul_apply]; ring_nf; exact Eq.symm (smul_add ..)) + (fun v y₁ y₂ => by simp only [map_add, add_apply]; ring) + (fun a v y => by simp only [map_smul, smul_apply]; ring_nf; exact Eq.symm (smul_add ..)), + by + intro v y + simp only [LinearMap.mk₂_apply, ContinuousLinearMap.map_add, + ContinuousLinearMap.add_apply, symm x] + ring⟩ + +end PseudoRiemannianMetric + +/-- A general (pseudo-)metric tensor of smoothness class `C^n` on a manifold `M`. + +This is the common core shared by Riemannian and pseudo-Riemannian metrics: +a smoothly varying symmetric, nondegenerate bilinear form on each tangent space. + +The pseudo-Riemannian notion will extend this with an index/signature constancy condition. -/ +@[ext] +structure MetricTensor + (E : Type v) (H : Type w) (M : Type*) (n : WithTop ℕ∞) + [inst_norm_grp_E : NormedAddCommGroup E] + [inst_norm_sp_E : NormedSpace ℝ E] + [inst_top_H : TopologicalSpace H] + [inst_top_M : TopologicalSpace M] + [inst_chart_M : ChartedSpace H M] + (I : ModelWithCorners ℝ E H) + [inst_mani : IsManifold I (n + 1) M] : + Type _ where + /-- The metric tensor at each point `x : M`, represented as a continuous linear map + `TₓM →L[ℝ] (TₓM →L[ℝ] ℝ)`. Applying it twice, `(val x v) w`, yields `gₓ(v, w)`. -/ + val : ∀ (x : M), TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) + /-- Symmetry: `gₓ(v, w) = gₓ(w, v)`. -/ + symm : ∀ (x : M) (v w : TangentSpace I x), (val x v) w = (val x w) v + /-- Non-degeneracy: if `gₓ(v, w) = 0` for all `w`, then `v = 0`. -/ + nondegenerate : ∀ (x : M) (v : TangentSpace I x), (∀ w : TangentSpace I x, + (val x v) w = 0) → v = 0 + /-- Smoothness of the metric tensor as a smooth section of the bundle of bilinear forms. + We follow the same pattern as Mathlib's Riemannian metric API, using `TotalSpace.mk'` + for the bundled map. -/ + contMDiff : + letI : IsManifold I 1 M := + IsManifold.of_le (I := I) (M := M) (m := (1 : WithTop ℕ∞)) (n := n + 1) + (by simp) + ContMDiff I (I.prod 𝓘(ℝ, E →L[ℝ] E →L[ℝ] ℝ)) n + (fun x ↦ TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ) x (val x)) + +namespace MetricTensor + +variable {E : Type v} {H : Type w} {M : Type*} {n : WithTop ℕ∞} +variable [NormedAddCommGroup E] [NormedSpace ℝ E] +variable [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] +variable {I : ModelWithCorners ℝ E H} +variable [IsManifold I (n + 1) M] + +/-- Coercion from `MetricTensor` to its `val` function. -/ +instance coeFunInst : CoeFun (MetricTensor E H M n I) + (fun _ => ∀ x : M, TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ)) where + coe g := g.val + +/-- The bilinear form on `TₓM` associated to a metric tensor. -/ +noncomputable def toBilinForm (g : MetricTensor E H M n I) (x : M) : + LinearMap.BilinForm ℝ (TangentSpace I x) where + toFun := fun v => + { toFun := fun w => g.val x v w + map_add' := fun w₁ w₂ => by simp only [ContinuousLinearMap.map_add] + map_smul' := fun c w => by simp only [map_smul, smul_eq_mul, RingHom.id_apply] } + map_add' := fun v₁ v₂ => by + ext w + simp only [map_add, add_apply, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply] + map_smul' := fun c v => by + ext w + simp only [map_smul, coe_smul', Pi.smul_apply, smul_eq_mul, LinearMap.coe_mk, AddHom.coe_mk, + RingHom.id_apply, LinearMap.smul_apply] + +/-- The quadratic form `v ↦ gₓ(v,v)` associated to a metric tensor. -/ +noncomputable abbrev toQuadraticForm (g : MetricTensor E H M n I) (x : M) : + QuadraticForm ℝ (TangentSpace I x) := + PseudoRiemannianMetric.valToQuadraticForm g.val g.symm x + +@[simp] +lemma toBilinForm_apply (g : MetricTensor E H M n I) (x : M) (v w : TangentSpace I x) : + toBilinForm g x v w = g.val x v w := rfl + +@[simp] +lemma toQuadraticForm_apply (g : MetricTensor E H M n I) (x : M) (v : TangentSpace I x) : + toQuadraticForm g x v = g.val x v v := rfl + +@[simp] +lemma toBilinForm_isSymm (g : MetricTensor E H M n I) (x : M) : + (toBilinForm g x).IsSymm := by + refine { eq := ?_ } + intro v w + simp [toBilinForm_apply, g.symm x v w] + +@[simp] +lemma toBilinForm_nondegenerate (g : MetricTensor E H M n I) (x : M) : + (toBilinForm g x).Nondegenerate := by + unfold LinearMap.BilinForm.Nondegenerate LinearMap.Nondegenerate + LinearMap.SeparatingLeft LinearMap.SeparatingRight + constructor + · intro v hv + simp_rw [toBilinForm_apply] at hv + exact g.nondegenerate x v hv + · intro v hv + simp_rw [toBilinForm_apply] at hv + have hw : ∀ w : TangentSpace I x, (g.val x v) w = 0 := by + intro w + simpa [g.symm x v w] using hv w + exact g.nondegenerate x v hw + +/-- The value `gₓ(v,w)` of a metric tensor. -/ +noncomputable def inner (g : MetricTensor E H M n I) (x : M) (v w : TangentSpace I x) : ℝ := + g.val x v w + +@[simp] +lemma inner_apply (g : MetricTensor E H M n I) (x : M) (v w : TangentSpace I x) : + inner g x v w = g.val x v w := rfl + +/-! ### Smoothness of the pairing `g(v,w)` -/ + +section PairingSmoothness + +variable [IsManifold I 1 M] + +variable + {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] + {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} + {M' : Type*} [TopologicalSpace M'] [ChartedSpace HM M'] + {b : M' → M} {v w : ∀ x, TangentSpace I (b x)} {s : Set M'} {x : M'} + +/-- Smoothness of the metric pairing along a smooth base map, for smooth fields into the fibers. -/ +lemma ContMDiffWithinAt.inner + (g : MetricTensor E H M n I) + (hv : ContMDiffWithinAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) + (hw : ContMDiffWithinAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) : + ContMDiffWithinAt IM 𝓘(ℝ) n (fun m ↦ g.inner (b m) (v m) (w m)) s x := by + have hb : ContMDiffWithinAt IM I n b s x := by + simp only [contMDiffWithinAt_totalSpace] at hv + exact hv.1 + have : ContMDiffWithinAt IM (I.prod 𝓘(ℝ)) n + (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial M ℝ) (b m) + ((g.val (b m)) (v m) (w m))) s x := by + apply ContMDiffWithinAt.clm_bundle_apply₂ (F₁ := E) (F₂ := E) + · exact ContMDiffAt.comp_contMDiffWithinAt x g.contMDiff.contMDiffAt hb + · exact hv + · exact hw + simp only [contMDiffWithinAt_totalSpace] at this + simpa [MetricTensor.inner] using this.2 + +lemma ContMDiffAt.inner + (g : MetricTensor E H M n I) + (hv : ContMDiffAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) + (hw : ContMDiffAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) : + ContMDiffAt IM 𝓘(ℝ) n (fun m ↦ g.inner (b m) (v m) (w m)) x := + ContMDiffWithinAt.inner (g := g) hv hw + +lemma ContMDiffOn.inner + (g : MetricTensor E H M n I) + (hv : ContMDiffOn IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) + (hw : ContMDiffOn IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) : + ContMDiffOn IM 𝓘(ℝ) n (fun m ↦ g.inner (b m) (v m) (w m)) s := + fun x hx ↦ ContMDiffWithinAt.inner (g := g) (x := x) (hv x hx) (hw x hx) + +lemma ContMDiff.inner + (g : MetricTensor E H M n I) + (hv : ContMDiff IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y))) + (hw : ContMDiff IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y))) : + ContMDiff IM 𝓘(ℝ) n (fun m ↦ g.inner (b m) (v m) (w m)) := + fun x ↦ ContMDiffAt.inner (g := g) (x := x) (hv x) (hw x) + +end PairingSmoothness + +section MDifferentiablePairing + +variable + {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] + {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} + {M' : Type*} [TopologicalSpace M'] [ChartedSpace HM M'] + {b : M' → M} {v w : ∀ x, TangentSpace I (b x)} {s : Set M'} {x : M'} + +lemma MDifferentiableWithinAt.inner + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableWithinAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) + (hw : MDifferentiableWithinAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) : + MDifferentiableWithinAt IM 𝓘(ℝ) (fun m ↦ g.inner (b m) (v m) (w m)) s x := by + have hb : MDifferentiableWithinAt IM I b s x := by + simp only [mdifferentiableWithinAt_totalSpace] at hv + exact hv.1 + have hpair : MDifferentiableWithinAt IM (I.prod 𝓘(ℝ)) + (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial M ℝ) (b m) + ((g.val (b m)) (v m) (w m))) s x := by + apply MDifferentiableWithinAt.clm_bundle_apply₂ (F₁ := E) (F₂ := E) + · exact MDifferentiableAt.comp_mdifferentiableWithinAt x + ((g.contMDiff.of_le hn).mdifferentiableAt one_ne_zero) hb + · exact hv + · exact hw + simp only [mdifferentiableWithinAt_totalSpace] at hpair + simpa [MetricTensor.inner] using hpair.2 + +lemma MDifferentiableAt.inner + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) + (hw : MDifferentiableAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) : + MDifferentiableAt IM 𝓘(ℝ) (fun m ↦ g.inner (b m) (v m) (w m)) x := + MDifferentiableWithinAt.inner (g := g) hn hv hw + +lemma MDifferentiableOn.inner + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableOn IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) + (hw : MDifferentiableOn IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) : + MDifferentiableOn IM 𝓘(ℝ) (fun m ↦ g.inner (b m) (v m) (w m)) s := + fun x hx ↦ MDifferentiableWithinAt.inner (g := g) (x := x) hn (hv x hx) (hw x hx) + +lemma MDifferentiable.inner + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiable IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y))) + (hw : MDifferentiable IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y))) : + MDifferentiable IM 𝓘(ℝ) (fun m ↦ g.inner (b m) (v m) (w m)) := + fun x ↦ MDifferentiableAt.inner (g := g) (x := x) hn (hv x) (hw x) + +end MDifferentiablePairing + +/-! ## Flat / sharp (musical isomorphisms) -/ + +/-- Index lowering map `v ↦ gₓ(v, -)` as a continuous linear map. -/ +abbrev flatL (g : MetricTensor E H M n I) (x : M) : + TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) := + g.val x + +/-- Index lowering map `v ↦ gₓ(v, -)` as a linear map. -/ +abbrev flat (g : MetricTensor E H M n I) (x : M) : + TangentSpace I x →ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ) := + (g.flatL x).toLinearMap + +@[simp] +lemma flat_apply (g : MetricTensor E H M n I) (x : M) (v w : TangentSpace I x) : + (flat g x v) w = g.val x v w := rfl + +@[simp] +lemma flatL_apply (g : MetricTensor E H M n I) (x : M) (v w : TangentSpace I x) : + (flatL g x v) w = g.val x v w := rfl + +lemma flat_inj (g : MetricTensor E H M n I) (x : M) : Function.Injective (flat g x) := by + rw [← LinearMap.ker_eq_bot] + apply LinearMap.ker_eq_bot'.mpr + intro v hv + apply g.nondegenerate x v + intro w + exact DFunLike.congr_fun hv w + +lemma flatL_inj (g : MetricTensor E H M n I) (x : M) : Function.Injective (flatL g x) := + flat_inj g x + +/-- Index lowering on the total space of the tangent bundle. -/ +noncomputable abbrev flatBundleMap (g : MetricTensor E H M n I) : + Bundle.TotalSpace E (fun y : M ↦ TangentSpace I y) → + Bundle.TotalSpace (E →L[ℝ] ℝ) (fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + | ⟨x, v⟩ => ⟨x, g.flatL x v⟩ + +lemma flatBundleMap_apply (g : MetricTensor E H M n I) (x : M) (v : TangentSpace I x) : + g.flatBundleMap ⟨x, v⟩ = ⟨x, g.flatL x v⟩ := rfl + +/-! ### Smoothness of index lowering -/ + +/-- The family `x ↦ g.flatL x` is a smooth section of the bundle of continuous linear maps from the +tangent bundle to the cotangent bundle. -/ +lemma contMDiff_flatL [IsManifold I 1 M] (g : MetricTensor E H M n I) : + ContMDiff I (I.prod 𝓘(ℝ, E →L[ℝ] E →L[ℝ] ℝ)) n + (fun x ↦ TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] (TangentSpace I y →L[ℝ] ℝ)) + x (g.flatL x)) := by + simpa [flatL] using g.contMDiff + +section FlatSmoothness + +variable + {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] + {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} + {M' : Type*} [TopologicalSpace M'] [ChartedSpace HM M'] + {b : M' → M} {v : ∀ x, TangentSpace I (b x)} {s : Set M'} {x : M'} + +/-- Lowering an index with a smooth metric tensor sends smooth vector fields to smooth covector +fields. -/ +lemma ContMDiffWithinAt.flatL + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hv : ContMDiffWithinAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) : + ContMDiffWithinAt IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) s x := by + have hv' := hv + simp only [contMDiffWithinAt_totalSpace] at hv' + have hflat : ContMDiffWithinAt IM (I.prod 𝓘(ℝ, E →L[ℝ] E →L[ℝ] ℝ)) n + (fun m ↦ TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] (TangentSpace I y →L[ℝ] ℝ)) + (b m) (g.flatL (b m))) s x := by + exact ContMDiffAt.comp_contMDiffWithinAt x (contMDiff_flatL (g := g)).contMDiffAt hv'.1 + exact ContMDiffWithinAt.clm_bundle_apply (F₁ := E) (F₂ := E →L[ℝ] ℝ) hflat hv + +lemma ContMDiffAt.flatL + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hv : ContMDiffAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) : + ContMDiffAt IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) x := + ContMDiffWithinAt.flatL (g := g) hv + +lemma ContMDiffOn.flatL + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hv : ContMDiffOn IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) : + ContMDiffOn IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) s := + fun x hx ↦ ContMDiffWithinAt.flatL (g := g) (hv x hx) + +lemma ContMDiff.flatL + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hv : ContMDiff IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y))) : + ContMDiff IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) := + fun x ↦ ContMDiffAt.flatL (g := g) (hv x) + +section MDifferentiableFlat + +lemma MDifferentiableWithinAt.flatL + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableWithinAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) : + MDifferentiableWithinAt IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) s x := by + have hv' := hv + simp only [mdifferentiableWithinAt_totalSpace] at hv' + have hflat : MDifferentiableWithinAt IM (I.prod 𝓘(ℝ, E →L[ℝ] E →L[ℝ] ℝ)) + (fun m ↦ TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] (TangentSpace I y →L[ℝ] ℝ)) + (b m) (g.flatL (b m))) s x := by + exact MDifferentiableAt.comp_mdifferentiableWithinAt x + (((contMDiff_flatL (g := g)).of_le hn).mdifferentiableAt one_ne_zero) hv'.1 + exact MDifferentiableWithinAt.clm_bundle_apply (F₁ := E) (F₂ := E →L[ℝ] ℝ) hflat hv + +lemma MDifferentiableAt.flatL + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) : + MDifferentiableAt IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) x := + MDifferentiableWithinAt.flatL (g := g) hn hv + +lemma MDifferentiableOn.flatL + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableOn IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) : + MDifferentiableOn IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) s := + fun x hx ↦ MDifferentiableWithinAt.flatL (g := g) hn (hv x hx) + +lemma MDifferentiable.flatL + [IsManifold I 1 M] + (g : MetricTensor E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiable IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y))) : + MDifferentiable IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) := + fun x ↦ MDifferentiableAt.flatL (g := g) hn (hv x) + +end MDifferentiableFlat +end FlatSmoothness + +/-- Index lowering is smooth on the total space of the tangent bundle. -/ +lemma contMDiff_flatBundleMap [IsManifold I 1 M] (g : MetricTensor E H M n I) : + ContMDiff (I.prod 𝓘(ℝ, E)) (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n g.flatBundleMap := by + simpa [flatBundleMap] using + (ContMDiff.flatL (g := g) + (b := fun p : Bundle.TotalSpace E (fun y : M ↦ TangentSpace I y) => p.1) + (v := fun p => p.2) contMDiff_id) + +/-- Index lowering is differentiable on the total space of the tangent bundle. -/ +lemma mdifferentiable_flatBundleMap [IsManifold I 1 M] + (g : MetricTensor E H M n I) (hn : (1 : WithTop ℕ∞) ≤ n) : + MDifferentiable (I.prod 𝓘(ℝ, E)) (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) g.flatBundleMap := by + simpa [flatBundleMap] using + (MDifferentiable.flatL (g := g) + (b := fun p : Bundle.TotalSpace E (fun y : M ↦ TangentSpace I y) => p.1) + (v := fun p => p.2) hn mdifferentiable_id) + +section FiniteDimensional + +variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] + +/-! In finite dimensions, nondegeneracy implies that `flatL` is automatically surjective, so the +musical isomorphisms can be packaged as inverse continuous linear equivalences. In infinite +dimensions, one would need a stronger nondegeneracy hypothesis to obtain such equivalences. -/ + +lemma flatL_surj (g : MetricTensor E H M n I) (x : M) : Function.Surjective (g.flatL x) := by + haveI : FiniteDimensional ℝ (TangentSpace I x) := inst_tangent_findim x + have h_finrank_eq : + finrank ℝ (TangentSpace I x) = finrank ℝ (TangentSpace I x →L[ℝ] ℝ) := by + have h_dual_eq : finrank ℝ (TangentSpace I x →L[ℝ] ℝ) = + finrank ℝ (Module.Dual ℝ (TangentSpace I x)) := by + let to_dual : (TangentSpace I x →L[ℝ] ℝ) → Module.Dual ℝ (TangentSpace I x) := + fun f => f.toLinearMap + let from_dual : Module.Dual ℝ (TangentSpace I x) → (TangentSpace I x →L[ℝ] ℝ) := + fun f => ContinuousLinearMap.mk f (by + apply LinearMap.continuous_of_finiteDimensional) + let equiv : (TangentSpace I x →L[ℝ] ℝ) ≃ₗ[ℝ] Module.Dual ℝ (TangentSpace I x) := + { toFun := to_dual + invFun := from_dual + map_add' := fun f g => by ext v; rfl + map_smul' := fun c f => by ext v; rfl + left_inv := fun f => by ext v; rfl + right_inv := fun f => by ext v; rfl } + exact LinearEquiv.finrank_eq equiv + rw [h_dual_eq, ← Subspace.dual_finrank_eq] + exact + (LinearMap.injective_iff_surjective_of_finrank_eq_finrank h_finrank_eq).mp (flatL_inj g x) + +/-- `flatEquiv` as a continuous linear equivalence. + +In finite dimensions, nondegeneracy of the metric implies surjectivity of `flatL`, so no extra +data are required. -/ +noncomputable def flatEquiv (g : MetricTensor E H M n I) (x : M) : + TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) := + LinearEquiv.toContinuousLinearEquiv <| + LinearEquiv.ofBijective (g.flatL x).toLinearMap ⟨g.flatL_inj x, g.flatL_surj x⟩ + +@[simp] +lemma flatEquiv_apply (g : MetricTensor E H M n I) (x : M) (v w : TangentSpace I x) : + (g.flatEquiv x v) w = g.val x v w := rfl + +/-- Index raising equivalence as the inverse of `flatEquiv`. + +This is the finite-dimensional `sharp` isomorphism; in infinite dimensions one would need a +stronger hypothesis to package index-raising in this form. -/ +noncomputable def sharpEquiv (g : MetricTensor E H M n I) (x : M) : + (TangentSpace I x →L[ℝ] ℝ) ≃L[ℝ] TangentSpace I x := + (g.flatEquiv x).symm + +/-- Index raising map `ω ↦ sharp ω` as a continuous linear map. -/ +noncomputable def sharpL (g : MetricTensor E H M n I) (x : M) : + (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x := + (g.sharpEquiv x).toContinuousLinearMap + +/-- Index raising map `sharp` as a linear map. -/ +noncomputable def sharp (g : MetricTensor E H M n I) (x : M) : + (TangentSpace I x →L[ℝ] ℝ) →ₗ[ℝ] TangentSpace I x := + (g.sharpEquiv x).toLinearEquiv.toLinearMap + +/-- Index raising on the total space of the cotangent bundle. -/ +noncomputable abbrev sharpBundleMap (g : MetricTensor E H M n I) : + Bundle.TotalSpace (E →L[ℝ] ℝ) (fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) → + Bundle.TotalSpace E (fun y : M ↦ TangentSpace I y) + | ⟨x, ω⟩ => ⟨x, g.sharpL x ω⟩ + +lemma sharpBundleMap_apply (g : MetricTensor E H M n I) (x : M) (ω : TangentSpace I x →L[ℝ] ℝ) : + g.sharpBundleMap ⟨x, ω⟩ = ⟨x, g.sharpL x ω⟩ := rfl + +/-- Fiberwise musical isomorphism between the total spaces of the tangent and cotangent bundles. -/ +noncomputable def flatBundleEquiv (g : MetricTensor E H M n I) : + Bundle.TotalSpace E (fun y : M ↦ TangentSpace I y) ≃ + Bundle.TotalSpace (E →L[ℝ] ℝ) (fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) where + toFun := g.flatBundleMap + invFun := g.sharpBundleMap + left_inv := by + rintro ⟨x, v⟩ + change Bundle.TotalSpace.mk x (g.sharpL x (g.flatL x v)) = Bundle.TotalSpace.mk x v + exact congrArg (Bundle.TotalSpace.mk x) ((g.flatEquiv x).left_inv v) + right_inv := by + rintro ⟨x, ω⟩ + change + (Bundle.TotalSpace.mk x (g.flatL x (g.sharpL x ω)) : + Bundle.TotalSpace (E →L[ℝ] ℝ) (fun y : M ↦ TangentSpace I y →L[ℝ] ℝ)) = + Bundle.TotalSpace.mk x ω + exact congrArg (Bundle.TotalSpace.mk x) ((g.flatEquiv x).right_inv ω) + +@[simp] +lemma sharpL_apply_flatL (g : MetricTensor E H M n I) (x : M) (v : TangentSpace I x) : + g.sharpL x (g.flatL x v) = v := + (g.flatEquiv x).left_inv v + +@[simp] +lemma flatL_apply_sharpL (g : MetricTensor E H M n I) (x : M) + (ω : TangentSpace I x →L[ℝ] ℝ) : g.flatL x (g.sharpL x ω) = ω := + (g.flatEquiv x).right_inv ω + +@[simp] +lemma flat_sharp_apply (g : MetricTensor E H M n I) (x : M) + (ω : TangentSpace I x →L[ℝ] ℝ) : g.flat x (g.sharp x ω) = ω := by + ext v + have h := congrArg (fun f : TangentSpace I x →L[ℝ] ℝ => f v) (flatL_apply_sharpL (g := g) x ω) + simpa [flat, flatL, sharp, sharpL] using h + +lemma sharp_flat_apply (g : MetricTensor E H M n I) (x : M) (v : TangentSpace I x) : + g.sharp x (g.flat x v) = v := by + have h := sharpL_apply_flatL (g := g) x v + simpa [sharp, sharpL, flat, flatL] using h + +/-- Metric evaluated at `sharp ω₁` and `sharp ω₂`. -/ +lemma apply_sharp_sharp (g : MetricTensor E H M n I) (x : M) + (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : + g.val x (g.sharpL x ω₁) (g.sharpL x ω₂) = ω₁ (g.sharpL x ω₂) := by + rw [← flatL_apply (g := g) x (g.sharpL x ω₁)] + rw [flatL_apply_sharpL (g := g) x ω₁] + +/-- Metric evaluated at `v` and `sharp ω`. -/ +lemma apply_vec_sharp (g : MetricTensor E H M n I) (x : M) (v : TangentSpace I x) + (ω : TangentSpace I x →L[ℝ] ℝ) : + g.val x v (g.sharpL x ω) = ω v := by + rw [g.symm x v (g.sharpL x ω)] + rw [← flatL_apply (g := g) x (g.sharpL x ω)] + rw [flatL_apply_sharpL (g := g) x ω] + + +end FiniteDimensional + +end MetricTensor diff --git a/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean index 1c9a266a6..1b17b1c34 100644 --- a/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean +++ b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean @@ -5,635 +5,541 @@ Authors: Matteo Cipollina -/ module -public import Mathlib.Analysis.InnerProductSpace.Basic -public import Mathlib.Geometry.Manifold.MFDeriv.Defs -public import Mathlib.LinearAlgebra.BilinearForm.Properties -public import Mathlib.LinearAlgebra.QuadraticForm.Real -public import Mathlib.Topology.LocallyConstant.Basic +public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Basic +public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.MetricTensorCotangent /-! -# Pseudo-Riemannian Metrics on Smooth Manifolds +# Pseudo-Riemannian metrics (manifold structure) -This file formalizes pseudo-Riemannian metrics on smooth manifolds and establishes their basic -properties. +This file defines the `PseudoRiemannianMetric` structure and its API, building on +`Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Basic.lean` (bundle-level setup and +`MetricTensor` through the musical isomorphisms) and +`Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/MetricTensorCotangent.lean` (induced cotangent +metric and `MetricTensor.index`). -A pseudo-Riemannian metric equips a manifold with a smoothly varying, non-degenerate, symmetric -bilinear form of *constant index* on each tangent space, generalizing the concept of an inner -product space to curved spaces. The index here refers to `QuadraticForm.negDim`, the dimension -of a maximal negative definite subspace. +A pseudo-Riemannian metric is a smoothly varying symmetric nondegenerate bilinear form on each +tangent space, whose index (negative inertia) is locally constant. The index is formalized using +`QuadraticForm.sigNeg`. In finite dimension, a metric induces the usual musical isomorphisms +(`flat`/`sharp`) and an induced metric on the cotangent spaces. -## Main Definitions +## Main definitions (this file) -* `PseudoRiemannianMetric E H M n I`: A structure representing a `C^n` pseudo-Riemannian metric - on a manifold `M` modelled on `(E, H)` with model with corners `I`. It consists of a family - of non-degenerate, symmetric, continuous bilinear forms `gₓ` on each tangent space `TₓM`, - varying `C^n`-smoothly with `x` and having a locally constant negative dimension (`negDim`). - The model space `E` must be finite-dimensional, and the manifold `M` must be `C^{n+1}` smooth. +* `PseudoRiemannianMetric E H M n I`: a `MetricTensor` whose pointwise index is locally constant. -* `PseudoRiemannianMetric.flatEquiv g x`: The "musical isomorphism" from the tangent space at `x` - to its dual space, representing the canonical isomorphism induced by the metric. +Earlier files in the same folder provide `Bundle` pseudo-Riemannian infrastructure, the +`MetricTensor` core, and cotangent/index material for `MetricTensor`. -* `PseudoRiemannianMetric.sharpEquiv g x`: The inverse of the flat isomorphism, mapping from - the dual space back to the tangent space. +## Implementation notes -* `PseudoRiemannianMetric.toQuadraticForm g x`: The quadratic form `v ↦ gₓ(v, v)` associated - with the metric at point `x`. +Smoothness is stated as a `ContMDiff` assumption for a bundled map `x ↦ TotalSpace.mk' … x (gₓ)` as +in Mathlib. Index-type constructions use `QuadraticForm.sigNeg` and therefore require +finite-dimensional tangent spaces. For now, local constancy of the index is packaged as part of the +definition of `PseudoRiemannianMetric`; deriving it from smooth nondegenerate variation would +require additional topological linear algebra about continuous families of symmetric bilinear forms. -This formalization adopts a direct approach, defining the metric as a family of bilinear forms -on tangent spaces, varying smoothly over the manifold. This pragmatic choice allows for foundational -development while acknowledging that a more abstract ideal would involve defining metrics as -sections of a tensor bundle (e.g., `Hom(TM ⊗ TM, ℝ)` or `TM →L[ℝ] TM →L[ℝ] ℝ`. +If the fibers already carry a topology (e.g. the tangent bundle), we register the fiberwise metric +through `Bundle.PseudoRiemannianBundle` to avoid introducing diamonds in typeclass inference, in the +same spirit as Mathlib's `Bundle.RiemannianBundle`. -## Reference +## Tags -* Barrett O'Neill, "Semi-Riemannian Geometry With Applications to Relativity" (Academic Press, 1983) -* [Discussion on Zulip about (Pseudo) Riemannian metrics] https. -leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.28Pseudo.29.20Riemannian.20metric +pseudo-Riemannian, metric tensor, musical isomorphisms, index + +## References + +* Barrett O'Neill, *Semi-Riemannian Geometry with Applications to Relativity*, Academic +Press (1983). -/ @[expose] public section section PseudoRiemannianMetric -noncomputable section - open Bundle Set Finset Function Filter Module Topology ContinuousLinearMap open scoped Manifold Bundle LinearMap Dual -namespace QuadraticForm - -variable {K : Type*} [Field K] - -/-! ## Negative Index -/ - -/-- The negative dimension (often called the index or negative index of inertia) of a -quadratic form `q` on a finite-dimensional real vector space. - -This value is defined by diagonalizing the quadratic form into an equivalent -`QuadraticMap.weightedSumSquares ℝ s`, where `s : Fin (finrank ℝ E) → SignType` -assigns `1`, `0`, or `-1` to each component. The `negDim` is the count of -components `i` for which `s i = SignType.neg`. - -By Sylvester's Law of Inertia, this count is an invariant of the quadratic form. -Geometrically, `negDim q` represents the dimension of any maximal vector subspace -on which `q` is negative definite. This corresponds to O'Neill's Definition 18 (p. 47) -of the index `ν` of a symmetric bilinear form `b` on `V`, which is "the largest integer -that is the dimension of a subspace `W ⊂ V` on which `b|W` is negative -definite." -/ -noncomputable def negDim {E : Type*} [AddCommGroup E] - [Module ℝ E] [FiniteDimensional ℝ E] - (q : QuadraticForm ℝ E) : ℕ := by classical - let P : (Fin (finrank ℝ E) → SignType) → Prop := fun w => - QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => (w i : ℝ)) - let h_exists : ∃ w, P w := QuadraticForm.equivalent_signType_weighted_sum_squared q - let w := Classical.choose h_exists - exact Finset.card (Finset.filter (fun i => w i = SignType.neg) Finset.univ) - -/-- For a standard basis vector in a weighted sum of squares, only one term in the sum - is nonzero. -/ -lemma QuadraticMap.weightedSumSquares_basis_vector {E : Type*} [AddCommGroup E] - [Module ℝ E] {weights : Fin (finrank ℝ E) → ℝ} - {i : Fin (finrank ℝ E)} (v : Fin (finrank ℝ E) → ℝ) - (hv : ∀ j, v j = if j = i then 1 else 0) : - QuadraticMap.weightedSumSquares ℝ weights v = weights i := by - simp only [QuadraticMap.weightedSumSquares_apply] - rw [Finset.sum_eq_single i] - · simp only [hv i, ↓reduceIte, mul_one, smul_eq_mul] - · intro j _ hj - simp only [hv j, if_neg hj, mul_zero, smul_eq_mul] - · simp only [Finset.mem_univ, not_true_eq_false, smul_eq_mul, mul_eq_zero, or_self, - IsEmpty.forall_iff] - -set_option backward.isDefEq.respectTransparency false in -/-- When a quadratic form is equivalent to a weighted sum of squares, - negative weights correspond to vectors where the form takes negative values. - This is a concrete realization of a 1-dimensional negative definite subspace, - contributing to O'Neill's index `ν` (Definition 18, p. 47). -/ -lemma neg_weight_implies_neg_value {E : Type*} [AddCommGroup E] [Module ℝ E] - {q : QuadraticForm ℝ E} {w : Fin (finrank ℝ E) → SignType} - (h_equiv : QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => (w i : ℝ))) - {i : Fin (finrank ℝ E)} (hi : w i = SignType.neg) : - ∃ v : E, v ≠ 0 ∧ q v < 0 := by - let f := Classical.choice h_equiv - let v_std : Fin (finrank ℝ E) → ℝ := fun j => if j = i then 1 else 0 - let v := f.symm v_std - have hv_ne_zero : v ≠ 0 := by - intro h - have : f v = f 0 := by rw [h] - have : f (f.symm v_std) = f 0 := by rw [← this] - have : v_std = 0 := by - rw [← f.apply_symm_apply v_std] - exact Eq.trans this (map_zero f) - have : v_std i = 0 := by rw [this]; rfl - simp only [↓reduceIte, one_ne_zero, v_std] at this - have hq_neg : q v < 0 := by - have heq : q v = QuadraticMap.weightedSumSquares ℝ (fun j => (w j : ℝ)) v_std := - QuadraticMap.IsometryEquiv.map_app f.symm v_std - have hw : QuadraticMap.weightedSumSquares ℝ (fun j => (w j : ℝ)) v_std = (w i : ℝ) := by - apply QuadraticMap.weightedSumSquares_basis_vector v_std - intro j; simp only [v_std] - rw [heq, hw] - have : (w i : ℝ) = -1 := by simp only [hi, SignType.neg_eq_neg_one, SignType.coe_neg, - SignType.coe_one] - rw [this] - exact neg_one_lt_zero - exact ⟨v, hv_ne_zero, hq_neg⟩ - -/-- A positive definite quadratic form cannot have any negative weights - in its diagonal representation. A quadratic form `q` derived from a bilinear form `b` - is positive definite if `b(v,v) > 0` for `v ≠ 0` (O'Neill, Definition 17 (1), p. 46). - The existence of a negative weight would imply `q(v) < 0` for some `v ≠ 0`, a contradiction. -/ -lemma posDef_no_neg_weights {E : Type*} [AddCommGroup E] [Module ℝ E] - {q : QuadraticForm ℝ E} (hq : q.PosDef) - {w : Fin (finrank ℝ E) → SignType} - (h_equiv : QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => (w i : ℝ))) : - ∀ i, w i ≠ SignType.neg := by - intro i hi - obtain ⟨v, hv_ne_zero, hq_neg⟩ := QuadraticForm.neg_weight_implies_neg_value h_equiv hi - have hq_pos : 0 < q v := hq v hv_ne_zero - exact lt_asymm hq_neg hq_pos - -/-- For a positive definite quadratic form, the negative dimension (index) is zero. - O'Neill states (p. 47) that "ν = 0 if and only if b is positive semidefinite." - Since positive definite implies positive semidefinite (Definitions 17 (1) and (2), p. 46), - a positive definite form must have index `ν = 0`. -/ -theorem rankNeg_eq_zero {E : Type*} [AddCommGroup E] - [Module ℝ E] [FiniteDimensional ℝ E] {q : QuadraticForm ℝ E} (hq : q.PosDef) : - q.negDim = 0 := by - haveI : Invertible (2 : ℝ) := inferInstance - unfold QuadraticForm.negDim - have h_exists := equivalent_signType_weighted_sum_squared q - let w := Classical.choose h_exists - have h_equiv : QuadraticMap.Equivalent q - (QuadraticMap.weightedSumSquares ℝ fun i => (w i : ℝ)) := - Classical.choose_spec h_exists - have h_no_neg : ∀ i, w i ≠ SignType.neg := - QuadraticForm.posDef_no_neg_weights hq h_equiv - simp [Finset.card_eq_zero, Finset.filter_eq_empty_iff] - exact fun ⦃x⦄ => h_no_neg x - -end QuadraticForm - -/-! ## Pseudo-Riemannian Metric -/ - -/-- -Constructs a `QuadraticForm` on the tangent space `TₓM` at a point `x` from the -value of a pseudo-Riemannian metric at that point. -(O'Neill, p. 47, "The function q: V → R given by q(v) = b(v,v) is the associated quadratic -form of b.") -The pseudo-Riemannian metric is given by `val`, a family of continuous bilinear forms -`gₓ: TₓM × TₓM → ℝ` for each `x : M`. -The quadratic form `Qₓ` at `x` is defined as `Qₓ(v) = gₓ(v,v)`. -The associated symmetric bilinear form required by `QuadraticForm.exists_companion'` -is `Bₓ(v,w) = gₓ(v,w) + gₓ(w,v)`. Given the symmetry `symm`, this is `2 * gₓ(v,w)`. --/ -def pseudoRiemannianMetricValToQuadraticForm - {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] - {H : Type w} [TopologicalSpace H] - {M : Type w} [TopologicalSpace M] [ChartedSpace H M] - {I : ModelWithCorners ℝ E H} - (val : ∀ (x : M), TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ)) - (symm : ∀ (x : M) (v w : TangentSpace I x), (val x v) w = (val x w) v) - (x : M) : QuadraticForm ℝ (TangentSpace I x) where - toFun v := val x v v - toFun_smul a v := by - simp only [ContinuousLinearMap.map_smul, ContinuousLinearMap.smul_apply, smul_smul] - exists_companion' := - ⟨LinearMap.mk₂ ℝ (fun v y => val x v y + val x y v) - (fun v₁ v₂ y => by simp only [map_add, add_apply]; ring) - (fun a v y => by simp only [map_smul, smul_apply]; ring_nf; exact Eq.symm (smul_add ..)) - (fun v y₁ y₂ => by simp only [map_add, add_apply]; ring) - (fun a v y => by simp only [map_smul, smul_apply]; ring_nf; exact Eq.symm (smul_add ..)), - by - intro v y - simp only [LinearMap.mk₂_apply, ContinuousLinearMap.map_add, - ContinuousLinearMap.add_apply, symm x] - ring⟩ - -/-- A pseudo-Riemannian metric of smoothness class `C^n` on a manifold `M` modelled on `(E, H)` -with model `I`. This structure defines a smoothly varying, non-degenerate, symmetric, -continuous bilinear form `gₓ` of constant negative dimension on the tangent space `TₓM` -at each point `x`. Requires `M` to be `C^{n+1}` smooth. -This structure formalizes O'Neill's Definition 3.1 (p. 54) of a metric tensor `g` on `M` -as a "symmetric non-degenerate (0,2) tensor field on M of constant index." -Each `gₓ` is a scalar product (O'Neill, Definition 20, p. 47) on `TₓM`. -/ +/-- A `C^n` pseudo-Riemannian metric on a manifold. + +This is a smooth symmetric nondegenerate bilinear form on each tangent space whose index +(`QuadraticForm.sigNeg`) is locally constant (O'Neill, *Semi-Riemannian Geometry* (1983), +Definition 3.1). -/ @[ext] structure PseudoRiemannianMetric - (E : Type v) (H : Type w) (M : Type w) (n : WithTop ℕ∞) + (E : Type v) (H : Type w) (M : Type*) (n : WithTop ℕ∞) [inst_norm_grp_E : NormedAddCommGroup E] [inst_norm_sp_E : NormedSpace ℝ E] [inst_top_H : TopologicalSpace H] [inst_top_M : TopologicalSpace M] [inst_chart_M : ChartedSpace H M] - [inst_chart_E : ChartedSpace H E] (I : ModelWithCorners ℝ E H) [inst_mani : IsManifold I (n + 1) M] [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] : - Type (max u v w) where - /-- The metric tensor at each point `x : M`, represented as a continuous linear map - `TₓM →L[ℝ] (TₓM →L[ℝ] ℝ)`. Applying it twice, `(val x v) w`, yields `gₓ(v, w)`. -/ - val : ∀ (x : M), TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) - /-- The metric is symmetric: `gₓ(v, w) = gₓ(w, v)`. -/ - symm : ∀ (x : M) (v w : TangentSpace I x), (val x v) w = (val x w) v - /-- The metric is non-degenerate: if `gₓ(v, w) = 0` for all `w`, then `v = 0`. -/ - nondegenerate : ∀ (x : M) (v : TangentSpace I x), (∀ w : TangentSpace I x, - (val x v) w = 0) → v = 0 - /-- The metric varies smoothly: Expressed in local coordinates via the chart - `e := extChartAt I x₀`, the function - `y ↦ g_{e.symm y}(mfderiv I I e.symm y v, mfderiv I I e.symm y w)` is `C^n` smooth on the - chart's target `e.target` for any constant vectors `v, w` in the model space `E`. -/ - smooth_in_charts' : ∀ (x₀ : M) (v w : E), - let e := extChartAt I x₀ - ContDiffWithinAt ℝ n - (fun y => val (e.symm y) (mfderiv I I e.symm y v) (mfderiv I I e.symm y w)) - (e.target) (e x₀) - /-- The negative dimension (`QuadraticForm.negDim`) of the metric's quadratic form is - locally constant. On a connected manifold, this implies it is constant globally. -/ - negDim_isLocallyConstant : + Type _ extends toMetricTensor : MetricTensor E H M n I where + /-- The negative index (`QuadraticForm.sigNeg`) of the metric's quadratic form is + locally constant. On a connected manifold, this implies it is constant globally. + + TODO: mathematically, this should be derivable from smooth nondegenerate variation of the + metric tensor. We currently keep it as data until the requisite topological linear algebra + lemmas are available. -/ + sigNeg_isLocallyConstant : IsLocallyConstant (fun x : M => have : FiniteDimensional ℝ (TangentSpace I x) := inferInstance - (pseudoRiemannianMetricValToQuadraticForm val symm x).negDim) + sigNeg (PseudoRiemannianMetric.valToQuadraticForm val symm x)) namespace PseudoRiemannianMetric -variable {E : Type v} {H : Type w} {M : Type w} {n : WithTop ℕ∞} +variable {E : Type v} {H : Type w} {M : Type*} {n : WithTop ℕ∞} variable [NormedAddCommGroup E] [NormedSpace ℝ E] -variable [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [ChartedSpace H E] +variable [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] variable {I : ModelWithCorners ℝ E H} variable [IsManifold I (n + 1) M] variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] -variable {g : PseudoRiemannianMetric E H M n I} /-- Given a pseudo-Riemannian metric `g` on manifold `M` and a point `x : M`, this function constructs a bilinear form on the tangent space at `x`. For tangent vectors `u v : T_x M`, the bilinear form is given by: `g_x(u, v) = g(x)(u, v)` -/ -def toBilinForm (g : PseudoRiemannianMetric E H M n I) (x : M) : - LinearMap.BilinForm ℝ (TangentSpace I x) where - toFun := λ v => { toFun := λ w => g.val x v w, - map_add' := λ w₁ w₂ => by - simp only [ContinuousLinearMap.map_add], - map_smul' := λ c w => by - simp only [map_smul, smul_eq_mul, RingHom.id_apply] } - map_add' := λ v₁ v₂ => by - ext w - simp only [map_add, add_apply, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply] - map_smul' := λ c v => by - ext w - simp only [map_smul, coe_smul', Pi.smul_apply, smul_eq_mul, LinearMap.coe_mk, AddHom.coe_mk, - RingHom.id_apply, LinearMap.smul_apply] +noncomputable abbrev toBilinForm (g : PseudoRiemannianMetric E H M n I) (x : M) : + LinearMap.BilinForm ℝ (TangentSpace I x) := + MetricTensor.toBilinForm (g := g.toMetricTensor) x /-- Convert a pseudo-Riemannian metric at a point `x` to a quadratic form `v ↦ gₓ(v, v)`. -/ -abbrev toQuadraticForm (g : PseudoRiemannianMetric E H M n I) (x : M) : +noncomputable abbrev toQuadraticForm (g : PseudoRiemannianMetric E H M n I) (x : M) : QuadraticForm ℝ (TangentSpace I x) := - pseudoRiemannianMetricValToQuadraticForm g.val g.symm x + MetricTensor.toQuadraticForm (g := g.toMetricTensor) x /-- Coercion from PseudoRiemannianMetric to its function representation. -/ instance coeFunInst : CoeFun (PseudoRiemannianMetric E H M n I) - (fun _ => ∀ x : M, TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ)) where + (fun _ => ∀ x : M, TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ)) where coe g := g.val @[simp] lemma toBilinForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M) - (v w : TangentSpace I x) : - toBilinForm g x v w = g.val x v w := rfl + (v w : TangentSpace I x) : toBilinForm g x v w = g.val x v w := + rfl @[simp] lemma toQuadraticForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M) - (v : TangentSpace I x) : - toQuadraticForm g x v = g.val x v v := rfl + (v : TangentSpace I x) : toQuadraticForm g x v = g.val x v v := + rfl + +/-! ## Index (negative inertia) -/ + +/-- The (negative) index of a pseudo-Riemannian metric at a point, defined as the negative index of +the associated quadratic form `v ↦ gₓ(v,v)`. -/ +noncomputable def index (g : PseudoRiemannianMetric E H M n I) (x : M) : ℕ := + sigNeg (g.toQuadraticForm x) @[simp] +lemma index_def (g : PseudoRiemannianMetric E H M n I) (x : M) : + g.index x = sigNeg (g.toQuadraticForm x) := + rfl + +lemma index_isLocallyConstant (g : PseudoRiemannianMetric E H M n I) : + IsLocallyConstant (fun x : M => g.index x) := + g.sigNeg_isLocallyConstant + +lemma index_eq_of_isPreconnected (g : PseudoRiemannianMetric E H M n I) {s : Set M} + (hs : IsPreconnected s) {x y : M} (hx : x ∈ s) (hy : y ∈ s) : g.index x = g.index y := + (index_isLocallyConstant (g := g)).apply_eq_of_isPreconnected hs hx hy + +lemma index_eq_of_preconnectedSpace [PreconnectedSpace M] (g : PseudoRiemannianMetric E H M n I) + (x y : M) : g.index x = g.index y := + (index_isLocallyConstant (g := g)).apply_eq_of_preconnectedSpace x y + +lemma index_eq_of_mem_connectedComponent (g : PseudoRiemannianMetric E H M n I) (x y : M) + (hy : y ∈ connectedComponent x) : g.index y = g.index x := + (index_isLocallyConstant (g := g)).apply_eq_of_isPreconnected + (isConnected_connectedComponent.isPreconnected) + hy (mem_connectedComponent : x ∈ connectedComponent x) + lemma toBilinForm_isSymm (g : PseudoRiemannianMetric E H M n I) (x : M) : (toBilinForm g x).IsSymm := by - refine { eq := ?_ } - intro v w; simp only [toBilinForm_apply]; exact g.symm x v w + simp [toBilinForm] -@[simp] lemma toBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) : (toBilinForm g x).Nondegenerate := by - unfold LinearMap.BilinForm.Nondegenerate LinearMap.Nondegenerate - LinearMap.SeparatingLeft LinearMap.SeparatingRight - constructor - · intro v hv; simp_rw [toBilinForm_apply] at hv; exact g.nondegenerate x v hv - · intro v hv; simp_rw [toBilinForm_apply] at hv; - have hw : ∀ (w : TangentSpace I x), ((g.val x) v) w = 0 := by - intro w; rw [symm]; simp [hv] - exact g.nondegenerate x v hw - -/-- The inner product (or scalar product) on the tangent space at point `x` - induced by the pseudo-Riemannian metric `g`. This is `gₓ(v, w)`. -/ -def inner (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : ℝ := - g.val x v w + simp [toBilinForm] -@[simp] -lemma inner_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : +/-- The fiberwise pairing \(g_x(v,w)\) of a pseudo-Riemannian metric. -/ +noncomputable abbrev inner (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : + ℝ := + MetricTensor.inner (g := g.toMetricTensor) x v w + +@[simp] lemma inner_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : inner g x v w = g.val x v w := rfl -/-! ## Flat -/ +/-! ### Smoothness of the pairing `g(v,w)` -/ -section Flat +section PairingSmoothness -/-- The "musical" isomorphism (index lowering) `v ↦ gₓ(v, -)`. -The non-degeneracy of `gₓ` (O'Neill, Def 17 (3), p. 46) means its matrix representation -is invertible (O'Neill, Lemma 19, p. 47), and that this map is an isomorphism from `TₓM` -to its dual. -/ -def flat (g : PseudoRiemannianMetric E H M n I) (x : M) : - TangentSpace I x →ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ) := - { toFun := λ v => g.val x v, - map_add' := λ v w => by simp only [ContinuousLinearMap.map_add], - map_smul' := λ a v => by simp only [ContinuousLinearMap.map_smul]; rfl } +variable [IsManifold I 1 M] -@[simp] -lemma flat_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : - (flat g x v) w = g.val x v w := by rfl +variable + {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] + {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} + {M' : Type*} [TopologicalSpace M'] [ChartedSpace HM M'] + {b : M' → M} {v w : ∀ x, TangentSpace I (b x)} {s : Set M'} {x : M'} -/-- The musical isomorphism as a continuous linear map. -/ -def flatL (g : PseudoRiemannianMetric E H M n I) (x : M) : - TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) where - toFun := λ v => g.val x v - map_add' := λ v w => by simp only [ContinuousLinearMap.map_add] - map_smul' := λ a v => by simp only [ContinuousLinearMap.map_smul]; rfl - cont := ContinuousLinearMap.continuous (g.val x) +lemma ContMDiffWithinAt.inner + (g : PseudoRiemannianMetric E H M n I) + (hv : ContMDiffWithinAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) + (hw : ContMDiffWithinAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) : + ContMDiffWithinAt IM 𝓘(ℝ) n (fun m ↦ g.inner (b m) (v m) (w m)) s x := by + simpa [PseudoRiemannianMetric.inner] using + (MetricTensor.ContMDiffWithinAt.inner (g := g.toMetricTensor) (b := b) (v := v) (w := w) + (s := s) (x := x) hv hw) + +lemma ContMDiffAt.inner + (g : PseudoRiemannianMetric E H M n I) + (hv : ContMDiffAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) + (hw : ContMDiffAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) : + ContMDiffAt IM 𝓘(ℝ) n (fun m ↦ g.inner (b m) (v m) (w m)) x := + ContMDiffWithinAt.inner (g := g) hv hw + +lemma ContMDiffOn.inner + (g : PseudoRiemannianMetric E H M n I) + (hv : ContMDiffOn IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) + (hw : ContMDiffOn IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) : + ContMDiffOn IM 𝓘(ℝ) n (fun m ↦ g.inner (b m) (v m) (w m)) s := + fun x hx ↦ ContMDiffWithinAt.inner (g := g) (x := x) (hv x hx) (hw x hx) + +lemma ContMDiff.inner + (g : PseudoRiemannianMetric E H M n I) + (hv : ContMDiff IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y))) + (hw : ContMDiff IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y))) : + ContMDiff IM 𝓘(ℝ) n (fun m ↦ g.inner (b m) (v m) (w m)) := + fun x ↦ ContMDiffAt.inner (g := g) (x := x) (hv x) (hw x) -@[simp] -lemma flatL_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : - (flatL g x v) w = g.val x v w := rfl +end PairingSmoothness -@[simp] -lemma flat_inj (g : PseudoRiemannianMetric E H M n I) (x : M) : - Function.Injective (flat g x) := by - rw [← LinearMap.ker_eq_bot]; apply LinearMap.ker_eq_bot'.mpr - intro v hv; apply g.nondegenerate x v; intro w; exact DFunLike.congr_fun hv w +section MDifferentiablePairing -@[simp] -lemma flatL_inj (g : PseudoRiemannianMetric E H M n I) (x : M) : - Function.Injective (flatL g x) := - flat_inj g x +variable + {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] + {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} + {M' : Type*} [TopologicalSpace M'] [ChartedSpace HM M'] + {b : M' → M} {v w : ∀ x, TangentSpace I (b x)} {s : Set M'} {x : M'} -@[simp] -lemma flatL_surj - (g : PseudoRiemannianMetric E H M n I) (x : M) : - Function.Surjective (g.flatL x) := by - haveI : FiniteDimensional ℝ (TangentSpace I x) := inst_tangent_findim x - have h_finrank_eq : finrank ℝ (TangentSpace I x) = finrank ℝ (TangentSpace I x →L[ℝ] ℝ) := by - have h_dual_eq : finrank ℝ (TangentSpace I x →L[ℝ] ℝ) = finrank ℝ (Module.Dual ℝ - (TangentSpace I x)) := by - let to_dual : (TangentSpace I x →L[ℝ] ℝ) → Module.Dual ℝ (TangentSpace I x) := - fun f => f.toLinearMap - let from_dual : Module.Dual ℝ (TangentSpace I x) → (TangentSpace I x →L[ℝ] ℝ) := fun f => - ContinuousLinearMap.mk f (by - apply LinearMap.continuous_of_finiteDimensional) - let equiv : (TangentSpace I x →L[ℝ] ℝ) ≃ₗ[ℝ] Module.Dual ℝ (TangentSpace I x) := - { toFun := to_dual, - invFun := from_dual, - map_add' := fun f g => by - ext v; unfold to_dual; simp only [LinearMap.add_apply]; rfl, - map_smul' := fun c f => by - ext v; unfold to_dual; simp only [LinearMap.smul_apply]; rfl, - left_inv := fun f => by - ext v; unfold to_dual from_dual; simp, - right_inv := fun f => by - ext v; unfold to_dual from_dual; simp } - exact LinearEquiv.finrank_eq equiv - rw [h_dual_eq, ← Subspace.dual_finrank_eq] - exact (LinearMap.injective_iff_surjective_of_finrank_eq_finrank h_finrank_eq).mp (flatL_inj g x) - -/-- The "musical" isomorphism (index lowering) from `TₓM` to its dual, -as a continuous linear equivalence. This equivalence is a direct result of `gₓ` being -a non-degenerate bilinear form (O'Neill, Def 17(3), p. 46; Lemma 19, p. 47). -/ -def flatEquiv +lemma MDifferentiableWithinAt.inner + [IsManifold I 1 M] (g : PseudoRiemannianMetric E H M n I) - (x : M) : - TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) := - LinearEquiv.toContinuousLinearEquiv - (LinearEquiv.ofBijective - ((g.flatL x).toLinearMap) - ⟨g.flatL_inj x, g.flatL_surj x⟩) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableWithinAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) + (hw : MDifferentiableWithinAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) : + MDifferentiableWithinAt IM 𝓘(ℝ) (fun m ↦ g.inner (b m) (v m) (w m)) s x := by + simpa [PseudoRiemannianMetric.inner] using + (MetricTensor.MDifferentiableWithinAt.inner (g.toMetricTensor) (b := b) (v := v) (w := w) + (s := s) (x := x) hn hv hw) + +lemma MDifferentiableAt.inner + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) + (hw : MDifferentiableAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) : + MDifferentiableAt IM 𝓘(ℝ) (fun m ↦ g.inner (b m) (v m) (w m)) x := + MDifferentiableWithinAt.inner (g := g) hn hv hw + +lemma MDifferentiableOn.inner + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableOn IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) + (hw : MDifferentiableOn IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) : + MDifferentiableOn IM 𝓘(ℝ) (fun m ↦ g.inner (b m) (v m) (w m)) s := + fun x hx ↦ MDifferentiableWithinAt.inner (g := g) (x := x) hn (hv x hx) (hw x hx) + +lemma MDifferentiable.inner + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiable IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y))) + (hw : MDifferentiable IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (w m : TotalSpace E fun y : M ↦ TangentSpace I y))) : + MDifferentiable IM 𝓘(ℝ) (fun m ↦ g.inner (b m) (v m) (w m)) := + fun x ↦ MDifferentiableAt.inner (g := g) (x := x) hn (hv x) (hw x) -lemma coe_flatEquiv - (g : PseudoRiemannianMetric E H M n I) (x : M) : - (g.flatEquiv x : TangentSpace I x →ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ)) = g.flatL x := rfl +end MDifferentiablePairing -@[simp] -lemma flatEquiv_apply - (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : - (g.flatEquiv x v) w = g.val x v w := rfl +/-! ## Flat / sharp / cotangent API (delegated to `MetricTensor`) -end Flat +TODO: upgrade the fiberwise bundle equivalence below to a smooth equivalence by proving that +`sharpBundleMap` is smooth. The `flatL` family and the total-space `flatBundleMap` are already +smooth, but the inverse direction still needs a smooth-inverse argument. -/ -/-! ## Sharp -/ +/-- Index lowering map `v ↦ gₓ(v, -)` as a linear map. -/ +abbrev flat (g : PseudoRiemannianMetric E H M n I) (x : M) : + TangentSpace I x →ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ) := + MetricTensor.flat (g := (g.toMetricTensor : MetricTensor E H M n I)) x + +/-- Index lowering map `v ↦ gₓ(v, -)` as a continuous linear map. -/ +abbrev flatL (g : PseudoRiemannianMetric E H M n I) (x : M) : + TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) := + MetricTensor.flatL (g := (g.toMetricTensor : MetricTensor E H M n I)) x + +lemma flat_inj (g : PseudoRiemannianMetric E H M n I) (x : M) : + Function.Injective (flat g x) := by + simpa [flat] using (MetricTensor.flat_inj (g := (g.toMetricTensor : MetricTensor E H M n I)) x) -section Sharp +lemma flatL_inj (g : PseudoRiemannianMetric E H M n I) (x : M) : + Function.Injective (flatL g x) := by + simpa [flatL] using (MetricTensor.flatL_inj (g := (g.toMetricTensor : MetricTensor E H M n I)) x) + +/-- Index lowering on the total space of the tangent bundle. -/ +noncomputable abbrev flatBundleMap (g : PseudoRiemannianMetric E H M n I) : + Bundle.TotalSpace E (fun y : M ↦ TangentSpace I y) → + Bundle.TotalSpace (E →L[ℝ] ℝ) (fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) := + MetricTensor.flatBundleMap (g := (g.toMetricTensor : MetricTensor E H M n I)) + +lemma flatBundleMap_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) : + g.flatBundleMap ⟨x, v⟩ = ⟨x, g.flatL x v⟩ := rfl + +/-- The family `x ↦ g.flatL x` is a smooth section of the bundle of continuous linear maps from the +tangent bundle to the cotangent bundle. -/ +lemma contMDiff_flatL [IsManifold I 1 M] (g : PseudoRiemannianMetric E H M n I) : + ContMDiff I (I.prod 𝓘(ℝ, E →L[ℝ] E →L[ℝ] ℝ)) n + (fun x ↦ TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] (TangentSpace I y →L[ℝ] ℝ)) + x (g.flatL x)) := by + simpa [flatL] using + (MetricTensor.contMDiff_flatL (g := (g.toMetricTensor : MetricTensor E H M n I))) + +section FlatSmoothness + +variable + {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] + {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} + {M' : Type*} [TopologicalSpace M'] [ChartedSpace HM M'] + {b : M' → M} {v : ∀ x, TangentSpace I (b x)} {s : Set M'} {x : M'} + +lemma ContMDiffWithinAt.flatL + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hv : ContMDiffWithinAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) : + ContMDiffWithinAt IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) s x := by + simpa [PseudoRiemannianMetric.flatL] using + (MetricTensor.ContMDiffWithinAt.flatL (g := g.toMetricTensor) (b := b) (v := v) + (s := s) (x := x) hv) + +lemma ContMDiffAt.flatL + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hv : ContMDiffAt IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) : + ContMDiffAt IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) x := + ContMDiffWithinAt.flatL (g := g) hv + +lemma ContMDiffOn.flatL + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hv : ContMDiffOn IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) : + ContMDiffOn IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) s := + fun x hx ↦ ContMDiffWithinAt.flatL (g := g) (hv x hx) + +lemma ContMDiff.flatL + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hv : ContMDiff IM (I.prod 𝓘(ℝ, E)) n + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y))) : + ContMDiff IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) := + fun x ↦ ContMDiffAt.flatL (g := g) (hv x) + +section MDifferentiableFlat + +lemma MDifferentiableWithinAt.flatL + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableWithinAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s x) : + MDifferentiableWithinAt IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) s x := by + simpa [PseudoRiemannianMetric.flatL] using + (MetricTensor.MDifferentiableWithinAt.flatL (g := g.toMetricTensor) (b := b) (v := v) + (s := s) (x := x) hn hv) + +lemma MDifferentiableAt.flatL + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableAt IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) x) : + MDifferentiableAt IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) x := + MDifferentiableWithinAt.flatL (g := g) hn hv + +lemma MDifferentiableOn.flatL + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiableOn IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y)) s) : + MDifferentiableOn IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) s := + fun x hx ↦ MDifferentiableWithinAt.flatL (g := g) hn (hv x hx) + +lemma MDifferentiable.flatL + [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) + (hn : (1 : WithTop ℕ∞) ≤ n) + (hv : MDifferentiable IM (I.prod 𝓘(ℝ, E)) + (fun m ↦ (v m : TotalSpace E fun y : M ↦ TangentSpace I y))) : + MDifferentiable IM (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) + (fun m ↦ TotalSpace.mk' (E →L[ℝ] ℝ) + (E := fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) + (b m) (g.flatL (b m) (v m))) := + fun x ↦ MDifferentiableAt.flatL (g := g) hn (hv x) + +end MDifferentiableFlat +end FlatSmoothness + +/-- Index lowering is smooth on the total space of the tangent bundle. -/ +lemma contMDiff_flatBundleMap [IsManifold I 1 M] (g : PseudoRiemannianMetric E H M n I) : + ContMDiff (I.prod 𝓘(ℝ, E)) (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) n g.flatBundleMap := by + simpa [PseudoRiemannianMetric.flatBundleMap] using + (MetricTensor.contMDiff_flatBundleMap + (g := (g.toMetricTensor : MetricTensor E H M n I))) + +/-- Index lowering is differentiable on the total space of the tangent bundle. -/ +lemma mdifferentiable_flatBundleMap [IsManifold I 1 M] + (g : PseudoRiemannianMetric E H M n I) (hn : (1 : WithTop ℕ∞) ≤ n) : + MDifferentiable (I.prod 𝓘(ℝ, E)) (I.prod 𝓘(ℝ, E →L[ℝ] ℝ)) g.flatBundleMap := by + simpa [PseudoRiemannianMetric.flatBundleMap] using + (MetricTensor.mdifferentiable_flatBundleMap + (g := (g.toMetricTensor : MetricTensor E H M n I)) hn) + +lemma flatL_surj (g : PseudoRiemannianMetric E H M n I) (x : M) : + Function.Surjective (flatL g x) := by + simpa [flatL] using (MetricTensor.flatL_surj (g := (g.toMetricTensor : MetricTensor E H M n I)) x) + + /-- The `flat` musical equivalence `TₓM ≃ (TₓM)⋆`. -/ +noncomputable abbrev flatEquiv (g : PseudoRiemannianMetric E H M n I) (x : M) : + TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) := + MetricTensor.flatEquiv (g := (g.toMetricTensor : MetricTensor E H M n I)) x -/-- The "musical" isomorphism (index raising) from the dual of `TₓM` to `TₓM`. -This is the inverse of `flatEquiv g x`, and its existence as an isomorphism is -guaranteed by the non-degeneracy of `gₓ` (O'Neill, Lemma 19, p. 47). -/ -def sharpEquiv - (g : PseudoRiemannianMetric E H M n I) (x : M) : + /-- The `sharp` musical equivalence `(TₓM)⋆ ≃ TₓM`. -/ +noncomputable abbrev sharpEquiv (g : PseudoRiemannianMetric E H M n I) (x : M) : (TangentSpace I x →L[ℝ] ℝ) ≃L[ℝ] TangentSpace I x := - (g.flatEquiv x).symm + MetricTensor.sharpEquiv (g := (g.toMetricTensor : MetricTensor E H M n I)) x -/-- The index raising map `sharp` as a continuous linear map. -/ -def sharpL - (g : PseudoRiemannianMetric E H M n I) (x : M) : - (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x := (g.sharpEquiv x).toContinuousLinearMap + /-- Index raising map `ω ↦ sharp ω` as a continuous linear map. -/ +noncomputable abbrev sharpL (g : PseudoRiemannianMetric E H M n I) (x : M) : + (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x := + MetricTensor.sharpL (g := (g.toMetricTensor : MetricTensor E H M n I)) x -lemma sharpL_eq_toContinuousLinearMap - (g : PseudoRiemannianMetric E H M n I) (x : M) : - g.sharpL x = (g.sharpEquiv x).toContinuousLinearMap := rfl + /-- Index raising map `ω ↦ sharp ω` as a linear map. -/ +noncomputable abbrev sharp (g : PseudoRiemannianMetric E H M n I) (x : M) : + (TangentSpace I x →L[ℝ] ℝ) →ₗ[ℝ] TangentSpace I x := + MetricTensor.sharp (g := (g.toMetricTensor : MetricTensor E H M n I)) x -lemma coe_sharpEquiv - (g : PseudoRiemannianMetric E H M n I) (x : M) : - (g.sharpEquiv x : (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x) = g.sharpL x := rfl +/-- Index raising on the total space of the cotangent bundle. -/ +noncomputable abbrev sharpBundleMap (g : PseudoRiemannianMetric E H M n I) : + Bundle.TotalSpace (E →L[ℝ] ℝ) (fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) → + Bundle.TotalSpace E (fun y : M ↦ TangentSpace I y) := + MetricTensor.sharpBundleMap (g := (g.toMetricTensor : MetricTensor E H M n I)) -/-- The index raising map `sharp` as a linear map. -/ -noncomputable def sharp - (g : PseudoRiemannianMetric E H M n I) (x : M) : - (TangentSpace I x →L[ℝ] ℝ) →ₗ[ℝ] TangentSpace I x := (g.sharpEquiv x).toLinearEquiv.toLinearMap +lemma sharpBundleMap_apply (g : PseudoRiemannianMetric E H M n I) (x : M) + (ω : TangentSpace I x →L[ℝ] ℝ) : + g.sharpBundleMap ⟨x, ω⟩ = ⟨x, g.sharpL x ω⟩ := rfl -@[simp] -lemma sharpL_apply_flatL - (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) : - g.sharpL x (g.flatL x v) = v := - (g.flatEquiv x).left_inv v +/-- Fiberwise musical isomorphism between the total spaces of the tangent and cotangent bundles. -/ +noncomputable def flatBundleEquiv (g : PseudoRiemannianMetric E H M n I) : + Bundle.TotalSpace E (fun y : M ↦ TangentSpace I y) ≃ + Bundle.TotalSpace (E →L[ℝ] ℝ) (fun y : M ↦ TangentSpace I y →L[ℝ] ℝ) := + MetricTensor.flatBundleEquiv (g := (g.toMetricTensor : MetricTensor E H M n I)) -@[simp] -lemma flatL_apply_sharpL - (g : PseudoRiemannianMetric E H M n I) (x : M) (ω : TangentSpace I x →L[ℝ] ℝ) : - g.flatL x (g.sharpL x ω) = ω := (g.flatEquiv x).right_inv ω +lemma sharpL_apply_flatL (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) : + g.sharpL x (g.flatL x v) = v := by + simp [sharpL, flatL] -/-- Applying `sharp` then `flat` recovers the original covector. -/ -@[simp] -lemma flat_sharp_apply - (g : PseudoRiemannianMetric E H M n I) (x : M) (ω : TangentSpace I x →L[ℝ] ℝ) : +lemma flatL_apply_sharpL (g : PseudoRiemannianMetric E H M n I) (x : M) + (ω : TangentSpace I x →L[ℝ] ℝ) : + g.flatL x (g.sharpL x ω) = ω := by + simp [sharpL, flatL] + +lemma flat_sharp_apply (g : PseudoRiemannianMetric E H M n I) (x : M) + (ω : TangentSpace I x →L[ℝ] ℝ) : g.flat x (g.sharp x ω) = ω := by - have := flatL_apply_sharpL g x ω - simp only [flat, sharp]; simp only [LinearEquiv.coe_coe] at this ⊢ - exact this + simp [flat, sharp] -@[simp] -lemma sharp_flat_apply - (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) : +lemma sharp_flat_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) : g.sharp x (g.flat x v) = v := by - have := sharpL_apply_flatL g x v - simp only [sharp, flat]; simp only [LinearEquiv.coe_coe] at this ⊢ - exact this + simpa [flat, sharp] using + (MetricTensor.sharp_flat_apply (g := (g.toMetricTensor : MetricTensor E H M n I)) x v) -/-- The metric evaluated at `sharp ω₁` and `sharp ω₂`. -/ -@[simp] -lemma apply_sharp_sharp - (g : PseudoRiemannianMetric E H M n I) (x : M) (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : +lemma apply_sharp_sharp (g : PseudoRiemannianMetric E H M n I) (x : M) + (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : g.val x (g.sharpL x ω₁) (g.sharpL x ω₂) = ω₁ (g.sharpL x ω₂) := by - rw [← flatL_apply g x (g.sharpL x ω₁)] - rw [flatL_apply_sharpL g x ω₁] + simp [sharpL] -/-- The metric evaluated at `v` and `sharp ω`. -/ -lemma apply_vec_sharp - (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) +lemma apply_vec_sharp (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) (ω : TangentSpace I x →L[ℝ] ℝ) : g.val x v (g.sharpL x ω) = ω v := by - rw [g.symm x v (g.sharpL x ω)] - rw [← flatL_apply g x (g.sharpL x ω)] - rw [flatL_apply_sharpL g x ω] + simpa [sharpL] using + (MetricTensor.apply_vec_sharp (g := (g.toMetricTensor : MetricTensor E H M n I)) x v ω) -end Sharp - -/-! ## Cotangent -/ -section Cotangent - -variable {E : Type v} {H : Type w} {M : Type w} {n : WithTop ℕ∞} -variable [NormedAddCommGroup E] [NormedSpace ℝ E] -variable [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [ChartedSpace H E] -variable {I : ModelWithCorners ℝ E H} -variable [IsManifold I (n + 1) M] -variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] - -/-- The value of the induced metric on the cotangent space at point `x`. -/ -noncomputable def cotangentMetricVal (g : PseudoRiemannianMetric E H M n I) (x : M) + /-- The induced cotangent metric value `g⁻¹(ω₁, ω₂)`. -/ +noncomputable abbrev cotangentMetricVal (g : PseudoRiemannianMetric E H M n I) (x : M) (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : ℝ := - g.val x (g.sharpL x ω₁) (g.sharpL x ω₂) + MetricTensor.cotangentMetricVal (g := (g.toMetricTensor : MetricTensor E H M n I)) x ω₁ ω₂ -@[simp] -lemma cotangentMetricVal_eq_apply_sharp (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : - cotangentMetricVal g x ω₁ ω₂ = ω₁ (g.sharpL x ω₂) := by - rw [cotangentMetricVal, apply_sharp_sharp] + /-- The induced cotangent metric as a bilinear form. -/ +noncomputable abbrev cotangentToBilinForm (g : PseudoRiemannianMetric E H M n I) (x : M) : + LinearMap.BilinForm ℝ (TangentSpace I x →L[ℝ] ℝ) := + MetricTensor.cotangentToBilinForm (g := (g.toMetricTensor : MetricTensor E H M n I)) x -lemma cotangentMetricVal_symm (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : - cotangentMetricVal g x ω₁ ω₂ = cotangentMetricVal g x ω₂ ω₁ := by - unfold cotangentMetricVal - rw [g.symm x (g.sharpL x ω₁) (g.sharpL x ω₂)] - -/-- The induced metric on the cotangent space at point `x` as a bilinear form. -For covectors `ω₁` and `ω₂`, this gives `g(ω₁^#, ω₂^#)`, where `ω^#` is -the "sharp" musical isomorphism raising indices. -/ -noncomputable def cotangentToBilinForm (g : PseudoRiemannianMetric E H M n I) (x : M) : - LinearMap.BilinForm ℝ (TangentSpace I x →L[ℝ] ℝ) where - toFun ω₁ := { toFun := λ ω₂ => cotangentMetricVal g x ω₁ ω₂, - map_add' := λ ω₂ ω₃ => by - simp only [cotangentMetricVal, - ContinuousLinearMap.map_add], - map_smul' := λ c ω₂ => by - simp only [cotangentMetricVal, - map_smul, smul_eq_mul, RingHom.id_apply] } - map_add' := λ ω₁ ω₂ => by - ext ω₃ - simp only [cotangentMetricVal, - ContinuousLinearMap.map_add, - ContinuousLinearMap.add_apply, - LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply] - map_smul' := λ c ω₁ => by - ext ω₂ - simp only [cotangentMetricVal, - ContinuousLinearMap.map_smul, - ContinuousLinearMap.smul_apply, - LinearMap.coe_mk, AddHom.coe_mk, - RingHom.id_apply, LinearMap.smul_apply] - -/-- The cometric on the cotangent space T_x*M at `x`, expressed as a quadratic form. -It is induced by the pseudo-Riemannian metric on the tangent space T_xM. -/ -noncomputable def cotangentToQuadraticForm (g : PseudoRiemannianMetric E H M n I) (x : M) : - QuadraticForm ℝ (TangentSpace I x →L[ℝ] ℝ) where - toFun ω := cotangentMetricVal g x ω ω - toFun_smul a ω := by - simp only [cotangentMetricVal, - ContinuousLinearMap.map_smul, - ContinuousLinearMap.smul_apply, - smul_smul] - exists_companion' := - ⟨LinearMap.mk₂ ℝ (fun ω₁ ω₂ => - cotangentMetricVal g x ω₁ ω₂ + cotangentMetricVal g x ω₂ ω₁) - (fun ω₁ ω₂ ω₃ => by simp only [cotangentMetricVal, map_add, add_apply]; ring) - (fun a ω₁ ω₂ => by - simp only [cotangentMetricVal, map_smul, smul_apply]; - ring_nf; exact Eq.symm (smul_add ..)) - (fun ω₁ ω₂ ω₃ => by - simp only [cotangentMetricVal, map_add, add_apply]; ring) - (fun a ω₁ ω₂ => by - simp only [cotangentMetricVal, map_smul, smul_apply]; ring_nf; - exact Eq.symm (smul_add ..)), - by - intro ω₁ ω₂ - simp only [LinearMap.mk₂_apply, cotangentMetricVal] - simp only [ContinuousLinearMap.map_add, ContinuousLinearMap.add_apply] - ring⟩ + /-- The induced cotangent metric as a quadratic form. -/ +noncomputable abbrev cotangentToQuadraticForm (g : PseudoRiemannianMetric E H M n I) (x : M) : + QuadraticForm ℝ (TangentSpace I x →L[ℝ] ℝ) := + MetricTensor.cotangentToQuadraticForm (g := (g.toMetricTensor : MetricTensor E H M n I)) x -@[simp] -lemma cotangentToBilinForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : - cotangentToBilinForm g x ω₁ ω₂ = cotangentMetricVal g x ω₁ ω₂ := rfl - -@[simp] -lemma cotangentToQuadraticForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω : TangentSpace I x →L[ℝ] ℝ) : - cotangentToQuadraticForm g x ω = cotangentMetricVal g x ω ω := rfl - -@[simp] -lemma cotangentToBilinForm_isSymm (g : PseudoRiemannianMetric E H M n I) (x : M) : - (cotangentToBilinForm g x).IsSymm := by - refine { eq := ?_ } - intro ω₁ ω₂; simp only [cotangentToBilinForm_apply]; exact cotangentMetricVal_symm g x ω₁ ω₂ - -/-- The cotangent metric is non-degenerate: if `cotangentMetricVal g x ω v = 0` for all `v`, - then `ω = 0`. -/ -lemma cotangentMetricVal_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) - (ω : TangentSpace I x →L[ℝ] ℝ) (h : ∀ v : TangentSpace I x →L[ℝ] ℝ, - cotangentMetricVal g x ω v = 0) : - ω = 0 := by - apply ContinuousLinearMap.ext - intro v - have h_forall : ∀ w : TangentSpace I x, ω w = 0 := by - intro w - let ω' : TangentSpace I x →L[ℝ] ℝ := g.flatL x w - have this : g.sharpL x ω' = w := by - simp only [ω', sharpL_apply_flatL] - have h_apply : cotangentMetricVal g x ω ω' = 0 := h ω' - simp only [cotangentMetricVal_eq_apply_sharp] at h_apply - rw [this] at h_apply - exact h_apply - exact h_forall v +theorem cotangentToQuadraticForm_equivalent_toQuadraticForm (g : PseudoRiemannianMetric E H M n I) + (x : M) : + (g.cotangentToQuadraticForm x).Equivalent (g.toQuadraticForm x) := by + simpa [cotangentToQuadraticForm, toQuadraticForm] using + (MetricTensor.cotangentToQuadraticForm_equivalent_toQuadraticForm + (g := (g.toMetricTensor : MetricTensor E H M n I)) x) -@[simp] -lemma cotangentToBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) : - (cotangentToBilinForm g x).Nondegenerate := by - unfold LinearMap.BilinForm.Nondegenerate LinearMap.Nondegenerate - LinearMap.SeparatingLeft LinearMap.SeparatingRight - constructor - · intro ω hω - apply cotangentMetricVal_nondegenerate g x ω - intro v - exact hω v - · intro ω hω - apply cotangentMetricVal_nondegenerate g x ω - intro v - have hv : ∀ (y : TangentSpace I x →L[ℝ] ℝ), ((g.cotangentToBilinForm x) ω) y = 0 := by - intro y; rw [LinearMap.BilinForm.isSymm_def.mp (cotangentToBilinForm_isSymm g x)]; simp [hω] - exact hv v - -end Cotangent +theorem cotangent_sigNeg_eq (g : PseudoRiemannianMetric E H M n I) (x : M) : + sigNeg (g.cotangentToQuadraticForm x) = + sigNeg (g.toQuadraticForm x) := by + simpa using (cotangentToQuadraticForm_equivalent_toQuadraticForm (g := g) x).sigNeg_eq end PseudoRiemannianMetric -end end PseudoRiemannianMetric diff --git a/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/MetricTensorCotangent.lean b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/MetricTensorCotangent.lean new file mode 100644 index 000000000..82a4d98c2 --- /dev/null +++ b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/MetricTensorCotangent.lean @@ -0,0 +1,174 @@ +/- +Copyright (c) 2025 Matteo Cipollina. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Matteo Cipollina +-/ +module + +public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Basic + +/-! +# Metric tensor: cotangent metric and index + +Induced cotangent-space metric (via the musical isomorphism) and the pointwise index +(`QuadraticForm.sigNeg`) for `MetricTensor`, continuing +`Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Basic.lean`. +-/ + +@[expose] public section + +section PseudoRiemannianMetric + +open Bundle Set Finset Function Filter Module Topology ContinuousLinearMap +open scoped Manifold Bundle LinearMap Dual + +namespace MetricTensor + +variable {E : Type v} {H : Type w} {M : Type*} {n : WithTop ℕ∞} +variable [NormedAddCommGroup E] [NormedSpace ℝ E] +variable [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] +variable {I : ModelWithCorners ℝ E H} +variable [IsManifold I (n + 1) M] + +section FiniteDimensional + +variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] + +/-! ## Cotangent metric induced by `g` -/ + +/-- The induced metric value on the cotangent space at `x`. -/ +noncomputable def cotangentMetricVal (g : MetricTensor E H M n I) (x : M) + (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : ℝ := + g.val x (g.sharpL x ω₁) (g.sharpL x ω₂) + +@[simp] lemma cotangentMetricVal_eq_apply_sharp (g : MetricTensor E H M n I) (x : M) + (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : + cotangentMetricVal g x ω₁ ω₂ = ω₁ (g.sharpL x ω₂) := by + simp [cotangentMetricVal] + +lemma cotangentMetricVal_symm (g : MetricTensor E H M n I) (x : M) + (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : + cotangentMetricVal g x ω₁ ω₂ = cotangentMetricVal g x ω₂ ω₁ := by + unfold cotangentMetricVal + rw [g.symm x (g.sharpL x ω₁) (g.sharpL x ω₂)] + +/-- The induced cotangent metric as a bilinear form. -/ +noncomputable def cotangentToBilinForm (g : MetricTensor E H M n I) (x : M) : + LinearMap.BilinForm ℝ (TangentSpace I x →L[ℝ] ℝ) where + toFun ω₁ := + { toFun := fun ω₂ => cotangentMetricVal g x ω₁ ω₂ + map_add' := fun ω₂ ω₃ => by simp [cotangentMetricVal, ContinuousLinearMap.map_add] + map_smul' := fun c ω₂ => by simp [cotangentMetricVal, map_smul, smul_eq_mul, RingHom.id_apply] + } + map_add' := fun ω₁ ω₂ => by + ext ω₃ + simp [cotangentMetricVal, ContinuousLinearMap.map_add, ContinuousLinearMap.add_apply, + LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply] + map_smul' := fun c ω₁ => by + ext ω₂ + simp [cotangentMetricVal, ContinuousLinearMap.smul_apply, + LinearMap.coe_mk, AddHom.coe_mk, RingHom.id_apply, LinearMap.smul_apply] + +/-- The induced cotangent metric as a quadratic form. -/ +noncomputable def cotangentToQuadraticForm (g : MetricTensor E H M n I) (x : M) : + QuadraticForm ℝ (TangentSpace I x →L[ℝ] ℝ) where + toFun ω := cotangentMetricVal g x ω ω + toFun_smul a ω := by + simp [cotangentMetricVal, ContinuousLinearMap.smul_apply] + ring + exists_companion' := + ⟨LinearMap.mk₂ ℝ (fun ω₁ ω₂ => + cotangentMetricVal g x ω₁ ω₂ + cotangentMetricVal g x ω₂ ω₁) + (fun ω₁ ω₂ ω₃ => by simp [cotangentMetricVal, map_add, add_apply]; ring) + (fun a ω₁ ω₂ => by + simp [cotangentMetricVal, map_smul, smul_apply] + ring_nf) + (fun ω₁ ω₂ ω₃ => by simp [cotangentMetricVal, map_add, add_apply]; ring) + (fun a ω₁ ω₂ => by + simp [cotangentMetricVal, map_smul, smul_apply] + ring_nf), + by + intro ω₁ ω₂ + simp [LinearMap.mk₂_apply, cotangentMetricVal, ContinuousLinearMap.map_add, + ContinuousLinearMap.add_apply] + ring⟩ + +@[simp] +lemma cotangentToBilinForm_apply (g : MetricTensor E H M n I) (x : M) + (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : + cotangentToBilinForm g x ω₁ ω₂ = cotangentMetricVal g x ω₁ ω₂ := rfl + +@[simp] +lemma cotangentToQuadraticForm_apply (g : MetricTensor E H M n I) (x : M) + (ω : TangentSpace I x →L[ℝ] ℝ) : + cotangentToQuadraticForm g x ω = cotangentMetricVal g x ω ω := rfl + +@[simp] +lemma cotangentToBilinForm_isSymm (g : MetricTensor E H M n I) (x : M) : + (cotangentToBilinForm g x).IsSymm := by + refine { eq := ?_ } + intro ω₁ ω₂ + simpa [cotangentToBilinForm_apply] using (cotangentMetricVal_symm (g := g) x ω₁ ω₂) + +/-- Nondegeneracy of the cotangent metric. -/ +lemma cotangentMetricVal_nondegenerate (g : MetricTensor E H M n I) (x : M) + (ω : TangentSpace I x →L[ℝ] ℝ) + (h : ∀ v : TangentSpace I x →L[ℝ] ℝ, cotangentMetricVal g x ω v = 0) : + ω = 0 := by + apply ContinuousLinearMap.ext + intro v + have h_forall : ∀ w : TangentSpace I x, ω w = 0 := by + intro w + let ω' : TangentSpace I x →L[ℝ] ℝ := g.flatL x w + have this : g.sharpL x ω' = w := by + simp [ω'] + have h_apply : cotangentMetricVal g x ω ω' = 0 := h ω' + simp [cotangentMetricVal_eq_apply_sharp] at h_apply + simpa [this] using h_apply + exact h_forall v + +@[simp] +lemma cotangentToBilinForm_nondegenerate (g : MetricTensor E H M n I) (x : M) : + (cotangentToBilinForm g x).Nondegenerate := by + unfold LinearMap.BilinForm.Nondegenerate LinearMap.Nondegenerate + LinearMap.SeparatingLeft LinearMap.SeparatingRight + constructor + · intro ω hω + apply cotangentMetricVal_nondegenerate (g := g) x ω + intro v + exact hω v + · intro ω hω + apply cotangentMetricVal_nondegenerate (g := g) x ω + intro v + have hv : ∀ y : TangentSpace I x →L[ℝ] ℝ, ((g.cotangentToBilinForm x) ω) y = 0 := by + intro y + rw [LinearMap.BilinForm.isSymm_def.mp (cotangentToBilinForm_isSymm (g := g) x)] + simp [hω] + exact hv v + +/-- The cotangent quadratic form is equivalent to the tangent quadratic form via `sharp`. -/ +theorem cotangentToQuadraticForm_equivalent_toQuadraticForm (g : MetricTensor E H M n I) (x : M) : + (g.cotangentToQuadraticForm x).Equivalent (g.toQuadraticForm x) := by + refine ⟨?_⟩ + refine + { toLinearEquiv := (g.sharpEquiv x).toLinearEquiv + map_app' := fun ω => ?_ } + simp [cotangentToQuadraticForm_apply, cotangentMetricVal, toQuadraticForm, sharpEquiv, sharpL] + +end FiniteDimensional + +/-- The (negative) index of a metric tensor at a point, defined as the negative index of the +associated quadratic form `v ↦ gₓ(v,v)`. + +This is a pointwise invariant; it need not be locally constant. -/ +noncomputable def index (g : MetricTensor E H M n I) (x : M) : ℕ := + sigNeg (g.toQuadraticForm x) + +@[simp] +lemma index_def (g : MetricTensor E H M n I) (x : M) : + g.index x = sigNeg (g.toQuadraticForm x) := + rfl + +end MetricTensor + +end PseudoRiemannianMetric diff --git a/Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean b/Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean index ef407c697..a462bf18b 100644 --- a/Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean +++ b/Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean @@ -6,219 +6,132 @@ Authors: Matteo Cipollina module public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs -public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic +public import Mathlib.Geometry.Manifold.VectorBundle.Riemannian +public import Mathlib.Geometry.Manifold.VectorBundle.Tangent +public import Mathlib.LinearAlgebra.QuadraticForm.Signature + /-! -# Riemannian Metric Definitions +# Riemannian metrics (tangent bundle) + +This file defines `RiemannianMetric` as the specialization of Mathlib's bundle-level +`Bundle.ContMDiffRiemannianMetric` to the tangent bundle, and provides a coercion to +`PseudoRiemannianMetric` by forgetting positivity. + +## Main definitions + +* `PseudoRiemannianMetric.RiemannianMetric`: a `C^n` Riemannian metric on `M`. +* `PseudoRiemannianMetric.IsRiemannianMetric`: the Prop-valued predicate on a generic + pseudo-Riemannian metric asserting index `0`. +* `PseudoRiemannianMetric.RiemannianMetric.toPseudoRiemannianMetric`: forget positivity to obtain a + pseudo-Riemannian metric (index `0`). -This module defines the Riemannian metric, building on pseudo-Riemannian metrics. +## Tags + +Riemannian, pseudo-Riemannian -/ @[expose] public section namespace PseudoRiemannianMetric -section RiemannianMetric -open Bundle Set Finset Function Filter Module Topology ContinuousLinearMap -open scoped Manifold Bundle LinearMap Dual -open PseudoRiemannianMetric InnerProductSpace +open Bundle ContinuousLinearMap +open scoped Manifold Bundle noncomputable section variable {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] variable {H : Type w} [TopologicalSpace H] -variable {M : Type w} [TopologicalSpace M] [ChartedSpace H M] [ChartedSpace H E] -variable {I : ModelWithCorners ℝ E H} {n : ℕ∞} - -/-- A `RiemannianMetric` on a manifold `M` modeled on `H` with corners `I` (over the model space `E` -, typically `ℝ^m`) is a family of inner products on the tangent spaces `TangentSpace I x` -for each `x : M`. This family is required to vary smoothly with `x`, specifically with smoothness -`C^n`. - -This structure `extends` `PseudoRiemannianMetric`, inheriting the core properties of a -pseudo-Riemannian metric, such as being a symmetric, non-degenerate, `C^n`-smooth tensor field -of type `(0,2)`. The key distinguishing feature of a Riemannian metric is its positive-definiteness. - -The `pos_def'` field ensures that for any point `x` on the manifold and any non-zero tangent -vector `v` at `x`, the inner product `gₓ(v, v)` (denoted `val x v v`) is strictly positive. -This condition makes each `val x` (the metric at point `x`) a positive-definite symmetric -bilinear form, effectively an inner product, on the tangent space `TangentSpace I x`. - -Parameters: -- `I`: The `ModelWithCorners` for the manifold `M`. This defines the model space `E` (e.g., `ℝ^d`) - and the model space for the boundary `H`. -- `n`: The smoothness class of the metric, an `ℕ∞` value. The metric tensor components are `C^n` - functions. -- `M`: The type of the manifold. -- `[TopologicalSpace M]`: Assumes `M` has a topological structure. -- `[ChartedSpace H M]`: Assumes `M` is equipped with an atlas of charts to `H`. -- `[IsManifold I (n + 1) M]`: Assumes `M` is a manifold of smoothness `C^(n+1)`. - The manifold needs to be slightly smoother than the metric itself for certain constructions. -- `[inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)]`: - Ensures that each tangent space is a finite-dimensional real vector space. - -Fields: -- `toPseudoRiemannianMetric`: The underlying pseudo-Riemannian metric. This provides the - smooth family of symmetric bilinear forms `val : M → SymBilinForm ℝ (TangentSpace I ·)`. -- `pos_def'`: The positive-definiteness condition: `∀ x v, v ≠ 0 → val x v v > 0`. This asserts - that for any point `x` and any non-zero tangent vector `v` at `x`, the metric evaluated - on `(v, v)` is strictly positive. -/ -@[ext] -structure RiemannianMetric - (I : ModelWithCorners ℝ E H) (n : ℕ∞) (M : Type w) - [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (n + 1) M] - [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] - extends PseudoRiemannianMetric E H M n I where - /-- `gₓ(v, v) > 0` for all nonzero `v`. `val` is inherited from `PseudoRiemannianMetric`. -/ - pos_def' : ∀ x v, v ≠ 0 → val x v v > 0 +variable {M : Type*} [TopologicalSpace M] [ChartedSpace H M] +variable {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} +variable [IsManifold I (n + 1) M] [IsManifold I 1 M] + +private lemma sigNeg_eq_zero_of_posDef + {F : Type*} [AddCommGroup F] [Module ℝ F] [FiniteDimensional ℝ F] + {Q : QuadraticForm ℝ F} (hQ : Q.PosDef) : sigNeg Q = 0 := by + obtain ⟨W, hW, hWneg⟩ := exists_finrank_eq_sigNeg_and_negDef (Q := Q) + have hWbot : W = ⊥ := by + rw [Submodule.eq_bot_iff] + intro x hx + by_contra hx0 + have hxW : (⟨x, hx⟩ : W) ≠ 0 := fun h => hx0 (congrArg Subtype.val h) + have hneg : Q x < 0 := by + have := hWneg _ hxW + simpa using neg_pos.mp (by simpa using this) + exact (not_lt_of_gt (hQ x hx0)) hneg + have hfin0 : Module.finrank ℝ W = 0 := by simp [hWbot] + exact hW.symm.trans hfin0 + +/-- A `C^n` Riemannian metric on `M`. -/ +abbrev RiemannianMetric + (I : ModelWithCorners ℝ E H) (n : WithTop ℕ∞) (M : Type*) + [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] := + Bundle.ContMDiffRiemannianMetric (IB := I) (n := n) (F := E) (E := fun x : M ↦ TangentSpace I x) + +variable [∀ x : M, FiniteDimensional ℝ (TangentSpace I x)] + +omit [IsManifold I 1 M] in +/-- Predicate asserting that a pseudo-Riemannian metric has index `0` at every point. -/ +class IsRiemannianMetric (g : _root_.PseudoRiemannianMetric E H M n I) : Prop where + /-- A Riemannian metric has index `0` at every point. -/ + index_eq_zero : ∀ x : M, g.index x = 0 + +omit [IsManifold I 1 M] in +@[simp] +lemma sigNeg_toQuadraticForm_eq_zero (g : _root_.PseudoRiemannianMetric E H M n I) + [IsRiemannianMetric (g := g)] (x : M) : + sigNeg (g.toQuadraticForm x) = 0 := by + simpa [_root_.PseudoRiemannianMetric.index] using IsRiemannianMetric.index_eq_zero (g := g) x + namespace RiemannianMetric -variable {I : ModelWithCorners ℝ E H} {n : ℕ∞} {M : Type w} -variable [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (n + 1) M] -variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] +/-- Forget the positivity to get a pseudo-Riemannian metric. The index is (locally constantly) `0`. +It makes pseudo-Riemannian API (musical isomorphisms, etc.) usable for a Riemannian metric. -/ +def toPseudoRiemannianMetric (g : RiemannianMetric I n M) : + _root_.PseudoRiemannianMetric E H M n I where + val := g.inner + symm := g.symm + nondegenerate x v hv := by + by_contra h + exact (g.pos x v h).ne' (hv v) + contMDiff := g.contMDiff + sigNeg_isLocallyConstant := + IsLocallyConstant.of_constant _ fun x y => by + have hx : + sigNeg (_root_.PseudoRiemannianMetric.valToQuadraticForm g.inner g.symm x) = 0 := + sigNeg_eq_zero_of_posDef fun v hv => by + simpa [_root_.PseudoRiemannianMetric.valToQuadraticForm] using g.pos x v hv + have hy : + sigNeg (_root_.PseudoRiemannianMetric.valToQuadraticForm g.inner g.symm y) = 0 := + sigNeg_eq_zero_of_posDef fun v hv => by + simpa [_root_.PseudoRiemannianMetric.valToQuadraticForm] using g.pos y v hv + rw [hx, hy] + +lemma index_toPseudoRiemannianMetric (g : RiemannianMetric I n M) (x : M) : + g.toPseudoRiemannianMetric.index x = 0 := by + have hx : sigNeg (_root_.PseudoRiemannianMetric.valToQuadraticForm g.inner g.symm x) = 0 := + sigNeg_eq_zero_of_posDef fun v hv => by + simpa [_root_.PseudoRiemannianMetric.valToQuadraticForm] using g.pos x v hv + simpa [_root_.PseudoRiemannianMetric.index, _root_.PseudoRiemannianMetric.toQuadraticForm, + toPseudoRiemannianMetric] using hx + +instance : Coe (RiemannianMetric I n M) (_root_.PseudoRiemannianMetric E H M n I) := + ⟨toPseudoRiemannianMetric⟩ + +instance (g : RiemannianMetric I n M) : + IsRiemannianMetric (g := (g : _root_.PseudoRiemannianMetric E H M n I)) where + index_eq_zero := index_toPseudoRiemannianMetric (g := g) -/-- Coercion from RiemannianMetric to its underlying PseudoRiemannianMetric. -/ -instance : Coe (RiemannianMetric I n M) (PseudoRiemannianMetric E H M (n) I) where - coe g := g.toPseudoRiemannianMetric +end RiemannianMetric -@[simp] -lemma pos_def (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) - (hv : v ≠ 0) : - (g.toPseudoRiemannianMetric.val x v) v > 0 := g.pos_def' x v hv +/-! ## Existence helper -/ -/-- The quadratic form associated with a Riemannian metric is positive definite. -/ -@[simp] -lemma toQuadraticForm_posDef (g : RiemannianMetric I n M) (x : M) : - (g.toQuadraticForm x).PosDef := - λ v hv => g.pos_def x v hv - -lemma riemannian_metric_negDim_zero (g : RiemannianMetric I n M) (x : M) : - (g.toQuadraticForm x).negDim = 0 := by - apply QuadraticForm.rankNeg_eq_zero - exact g.toQuadraticForm_posDef x - -/-! ## InnerProductSpace structure from RiemannianMetric -/ - -section InnerProductSpace - -variable (g : RiemannianMetric I n M) (x : M) - -/-- The `InnerProductSpace.Core` structure for `TₓM` induced by a Riemannian metric `g`. - This provides the properties of an inner product: symmetry, - non-negativity, linearity, and definiteness. - Each `gₓ` is an inner product on `TₓM` (O'Neill, p. 55). -/ -@[reducible] -noncomputable def tangentInnerCore (g : RiemannianMetric I n M) (x : M) : - InnerProductSpace.Core ℝ (TangentSpace I x) where - inner := λ v w => g.inner x v w - conj_inner_symm := λ v w => by - simp only [inner_apply, conj_trivial] - exact g.toPseudoRiemannianMetric.symm x w v - re_inner_nonneg := λ v => by - simp only [inner_apply, RCLike.re_to_real] - by_cases hv : v = 0 - · simp [hv, map_zero] - · exact le_of_lt (g.pos_def x v hv) - add_left := λ u v w => by - simp only [inner_apply, map_add, ContinuousLinearMap.add_apply] - smul_left := λ r u v => by - simp only [inner_apply, map_smul, conj_trivial] - rfl - definite := fun v (h_inner_zero : g.inner x v v = 0) => by - by_contra h_v_ne_zero - have h_pos : g.inner x v v > 0 := g.pos_def x v h_v_ne_zero - linarith [h_inner_zero, h_pos] - -/-! ### Local `NormedAddCommGroup` and `InnerProductSpace` Instances - -These instances are defined locally to be used when a specific Riemannian metric `g` -and point `x` are in context. They are not global instances to avoid typeclass conflicts -and to respect the fact that a manifold might not have a canonical Riemannian metric, -or might be studied with an indefinite (pseudo-Riemannian) metric where these -standard norm structures are not appropriate. -/ - -/-- Creates a `NormedAddCommGroup` structure on `TₓM` from a Riemannian metric `g`. -/ -@[reducible] -noncomputable def TangentSpace.metricNormedAddCommGroup (g : RiemannianMetric I n M) (x : M) : - NormedAddCommGroup (TangentSpace I x) := - @InnerProductSpace.Core.toNormedAddCommGroup ℝ (TangentSpace I x) _ _ _ (tangentInnerCore g x) - -/-- Creates an `InnerProductSpace` structure on `TₓM` from a Riemannian metric `g`. - Alternative implementation using `letI`. -/ -@[reducible] -noncomputable def TangentSpace.metricInnerProductSpace' (g : RiemannianMetric I n M) (x : M) : - letI := TangentSpace.metricNormedAddCommGroup g x - InnerProductSpace ℝ (TangentSpace I x) := - InnerProductSpace.ofCore (tangentInnerCore g x).toCore - -/-- Creates an `InnerProductSpace` structure on `TₓM` from a Riemannian metric `g`. -/ -@[reducible] -noncomputable def TangentSpace.metricInnerProductSpace (g : RiemannianMetric I n M) (x : M) : - let _ := TangentSpace.metricNormedAddCommGroup g x - InnerProductSpace ℝ (TangentSpace I x) := - let inner_core := tangentInnerCore g x - let _ := TangentSpace.metricNormedAddCommGroup g x - InnerProductSpace.ofCore inner_core.toCore - -/-- The norm on a tangent space induced by a Riemannian metric, defined as the square root - of the inner product of a vector with itself. -/ -noncomputable def norm (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : ℝ := - Real.sqrt (g.inner x v v) - --- Example using the norm function -example (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : - norm g x v ≥ 0 := Real.sqrt_nonneg _ - --- Example showing how to use the metric inner product space -example (g : RiemannianMetric I n M) (x : M) (v w : TangentSpace I x) : - (TangentSpace.metricInnerProductSpace g x).inner v w = g.inner x v w := by - letI := TangentSpace.metricInnerProductSpace g x - rfl - -/-- Helper function to compute the norm on a tangent space from a Riemannian metric, - using the underlying `NormedAddCommGroup` structure. -/ -noncomputable def norm' (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : ℝ := - let normed_group := TangentSpace.metricNormedAddCommGroup g x - @Norm.norm (TangentSpace I x) (@NormedAddCommGroup.toNorm (TangentSpace I x) normed_group) v - --- Example: Using a custom norm function instead of the notation -example (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : - norm g x v ≥ 0 := by - unfold norm - apply Real.sqrt_nonneg - -example (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : ℝ := - letI := TangentSpace.metricNormedAddCommGroup g x - ‖v‖ - -example (g : RiemannianMetric I n M) (x : M) (v : TangentSpace I x) : ℝ := - let normed_group := TangentSpace.metricNormedAddCommGroup g x - @Norm.norm (TangentSpace I x) (@NormedAddCommGroup.toNorm (TangentSpace I x) normed_group) v - -lemma norm_eq_norm_of_metricNormedAddCommGroup (g : RiemannianMetric I n M) (x : M) - (v : TangentSpace I x) : norm g x v = @Norm.norm (TangentSpace I x) - (@NormedAddCommGroup.toNorm _ (TangentSpace.metricNormedAddCommGroup g x)) v := by - unfold norm - let normed_group := TangentSpace.metricNormedAddCommGroup g x - unfold TangentSpace.metricNormedAddCommGroup - simp only [inner_apply] - rfl - -end InnerProductSpace - -/-! ## Curve -/ - -section Curve - -/-- Calculates the length of a curve `γ` between parameters `t₀` and `t₁` -using the Riemannian metric `g`. This is defined as the integral of the norm of -the tangent vector along the curve. -/ -def curveLength (g : RiemannianMetric I n M) (γ : ℝ → M) (t₀ t₁ : ℝ) - {IDE : ModelWithCorners ℝ ℝ ℝ}[ChartedSpace ℝ ℝ] : ℝ := - ∫ t in t₀..t₁, norm g (γ t) ((mfderiv IDE I γ t) ((1 : ℝ) : TangentSpace IDE t)) - -end Curve +/-- Existence of a Riemannian metric implies existence of a pseudo-Riemannian metric (of index `0`), +by forgetting positivity. -/ +theorem nonempty_pseudoRiemannianMetric_of_nonempty_riemannianMetric + (h : Nonempty (RiemannianMetric I n M)) : + Nonempty (_root_.PseudoRiemannianMetric E H M n I) := + h.map RiemannianMetric.toPseudoRiemannianMetric -end RiemannianMetric end -end RiemannianMetric + end PseudoRiemannianMetric