diff --git a/Physlib.lean b/Physlib.lean index 580bb2490..7f8c14f8d 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -57,6 +57,7 @@ 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.Defs public import Physlib.Mathematics.Geometry.Metric.Riemannian.Defs public import Physlib.Mathematics.InnerProductSpace.Adjoint diff --git a/Physlib/Mathematics/Geometry/Metric/Lorentzian/Defs.lean b/Physlib/Mathematics/Geometry/Metric/Lorentzian/Defs.lean new file mode 100644 index 000000000..c28ce855a --- /dev/null +++ b/Physlib/Mathematics/Geometry/Metric/Lorentzian/Defs.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2026 Matteo Cipollina. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Matteo Cipollina +-/ +module + +import all Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs +import Mathlib.Geometry.Manifold.VectorBundle.Tangent +import Mathlib.LinearAlgebra.QuadraticForm.Signature + +/-! +# Lorentzian metrics + +This file records the Lorentzian condition (index `1`) for a pseudo-Riemannian metric. + +## Main definitions + +p0* `PseudoRiemannianMetric.IsLorentzianMetric`: the Prop-valued predicate asserting that a + pseudo-Riemannian metric has index `1` at every point. + +## Tags + +Lorentzian, pseudo-Riemannian, index +-/ + +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, sigNeg (g.toQuadraticForm x) = 1 + +attribute [simp] IsLorentzianMetric.index_eq_one + +end + +end PseudoRiemannianMetric diff --git a/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean index 1c9a266a6..d12d1acfd 100644 --- a/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean +++ b/Physlib/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean @@ -5,192 +5,282 @@ 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 +import Mathlib.Geometry.Manifold.VectorBundle.Riemannian +import Mathlib.Geometry.Manifold.VectorBundle.Tangent +import Mathlib.LinearAlgebra.BilinearForm.Properties +import Mathlib.LinearAlgebra.QuadraticForm.Signature +import Mathlib.Topology.LocallyConstant.Basic /-! -# Pseudo-Riemannian Metrics on Smooth Manifolds +# Pseudo-Riemannian metrics -This file formalizes pseudo-Riemannian metrics on smooth manifolds and establishes their basic -properties. +This file defines pseudo-Riemannian metrics on smooth manifolds, in a way that mirrors Mathlib's +bundle-first Riemannian metric API. -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 -* `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. +* `Bundle.PseudoRiemannianBundle`: fiberwise data of a symmetric nondegenerate bilinear form. +* `Bundle.ContMDiffPseudoRiemannianMetric`: a `C^n` pseudo-Riemannian metric along a vector bundle, + expressed as a smooth section into the bundle of bilinear forms. +* `Bundle.IsContMDiffPseudoRiemannianBundle`: the corresponding Prop-valued existence predicate. +* `MetricTensor E H M n I`: the common core data of a smooth symmetric nondegenerate bilinear form + on each tangent space. +* `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. +## Implementation notes -* `PseudoRiemannianMetric.sharpEquiv g x`: The inverse of the flat isomorphism, mapping from - the dual space back to the tangent space. +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. -* `PseudoRiemannianMetric.toQuadraticForm g x`: The quadratic form `v ↦ gₓ(v, v)` associated - with the metric at point `x`. +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`. -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[ℝ] ℝ`. +## Tags -## Reference +pseudo-Riemannian, metric tensor, musical isomorphisms, index -* 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 --/ +## References -@[expose] public section +* Barrett O'Neill, *Semi-Riemannian Geometry with Applications to Relativity*, Academic +Press (1983). +-/ 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 +/-! ## 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 + +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 w} [TopologicalSpace M] [ChartedSpace H M] + {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) @@ -210,397 +300,350 @@ def pseudoRiemannianMetricValToQuadraticForm 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`. -/ +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 PseudoRiemannianMetric - (E : Type v) (H : Type w) (M : Type w) (n : WithTop ℕ∞) +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] - [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 + [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[ℝ] ℝ) - /-- The metric is symmetric: `gₓ(v, w) = gₓ(w, v)`. -/ + /-- Symmetry: `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`. -/ + /-- 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 - /-- 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 : - IsLocallyConstant (fun x : M => - have : FiniteDimensional ℝ (TangentSpace I x) := inferInstance - (pseudoRiemannianMetricValToQuadraticForm val symm x).negDim) - -namespace PseudoRiemannianMetric - -variable {E : Type v} {H : Type w} {M : Type w} {n : WithTop ℕ∞} + /-- 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] [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) : +/-- 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 := λ 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 + 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' := λ c v => by + 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] -/-- 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) : +/-- 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) := - pseudoRiemannianMetricValToQuadraticForm g.val g.symm 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 - coe g := g.val + PseudoRiemannianMetric.valToQuadraticForm g.val g.symm x @[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 +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 : PseudoRiemannianMetric E H M n I) (x : M) - (v : TangentSpace I x) : - toQuadraticForm g x v = g.val x v v := rfl +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 : PseudoRiemannianMetric E H M n I) (x : M) : +lemma toBilinForm_isSymm (g : MetricTensor 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 + intro v w + simp [toBilinForm_apply, g.symm x v w] @[simp] -lemma toBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) : +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; rw [symm]; simp [hv] + · 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 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) : ℝ := +/-- 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 : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : +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 -/-! ## Flat -/ - -section Flat - -/-- 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) : +/-! ### 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.val (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 + exact this.2 + +end PairingSmoothness + +/-! ## 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[ℝ] ℝ) := - { 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 } + (g.flatL x).toLinearMap @[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 - -/-- 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 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 : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : +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 -@[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 +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 -@[simp] -lemma flatL_inj (g : PseudoRiemannianMetric E H M n I) (x : M) : - Function.Injective (flatL g x) := +lemma flatL_inj (g : MetricTensor E H M n I) (x : M) : Function.Injective (flatL g x) := flat_inj g x -@[simp] -lemma flatL_surj - (g : PseudoRiemannianMetric E H M n I) (x : M) : - Function.Surjective (g.flatL x) := by +section FiniteDimensional + +variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] + +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 + 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 + 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 } + { 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) + 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 - (g : PseudoRiemannianMetric E H M n I) - (x : M) : +/-- `flatEquiv` as a continuous linear equivalence. -/ +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⟩) - -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 + LinearEquiv.toContinuousLinearEquiv <| + LinearEquiv.ofBijective (g.flatL x).toLinearMap ⟨g.flatL_inj x, g.flatL_surj x⟩ @[simp] -lemma flatEquiv_apply - (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : +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 -end Flat - -/-! ## Sharp -/ - -section Sharp - -/-- 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) : +/-- Index raising equivalence as the inverse of `flatEquiv`. -/ +noncomputable def sharpEquiv (g : MetricTensor E H M n I) (x : M) : (TangentSpace I x →L[ℝ] ℝ) ≃L[ℝ] TangentSpace I x := (g.flatEquiv x).symm -/-- 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 def sharpL (g : MetricTensor E H M n I) (x : M) : + (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x := + (g.sharpEquiv x).toContinuousLinearMap -lemma sharpL_eq_toContinuousLinearMap - (g : PseudoRiemannianMetric E H M n I) (x : M) : - g.sharpL x = (g.sharpEquiv x).toContinuousLinearMap := rfl - -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 - -/-- 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 +/-- 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 @[simp] -lemma sharpL_apply_flatL - (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) : +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 : PseudoRiemannianMetric E H M n I) (x : M) (ω : TangentSpace I x →L[ℝ] ℝ) : - g.flatL x (g.sharpL x ω) = ω := (g.flatEquiv x).right_inv ω +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 ω -/-- 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[ℝ] ℝ) : - 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 +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 -@[simp] -lemma sharp_flat_apply - (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) : +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 := sharpL_apply_flatL g x v - simp only [sharp, flat]; simp only [LinearEquiv.coe_coe] at this ⊢ - exact this + have h := sharpL_apply_flatL (g := g) x v + simpa [sharp, sharpL, flat, flatL] using h -/-- 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[ℝ] ℝ) : +/-- 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 x (g.sharpL x ω₁)] - rw [flatL_apply_sharpL g x ω₁] + rw [← flatL_apply (g := g) x (g.sharpL x ω₁)] + rw [flatL_apply_sharpL (g := g) x ω₁] -/-- The metric evaluated at `v` and `sharp ω`. -/ -lemma apply_vec_sharp - (g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I 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 x (g.sharpL x ω)] - rw [flatL_apply_sharpL g x ω] - -end Sharp - -/-! ## Cotangent -/ -section Cotangent + rw [← flatL_apply (g := g) x (g.sharpL x ω)] + rw [flatL_apply_sharpL (g := g) x ω] -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)] +/-! ## Cotangent metric induced by `g` -/ -/-- 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 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 : PseudoRiemannianMetric E H M n I) (x : M) +@[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 - rw [cotangentMetricVal, apply_sharp_sharp] + cotangentMetricVal g x ω₁ ω₂ = ω₁ (g.sharpL x ω₂) := by + simp [cotangentMetricVal] -lemma cotangentMetricVal_symm (g : PseudoRiemannianMetric E H M n I) (x : M) +lemma cotangentMetricVal_symm (g : MetricTensor E H M n I) (x : M) (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : - cotangentMetricVal g x ω₁ ω₂ = cotangentMetricVal g x ω₂ ω₁ := by + 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) : +/-- 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 := λ ω₂ => 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 + 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 only [cotangentMetricVal, - ContinuousLinearMap.map_add, - ContinuousLinearMap.add_apply, + simp [cotangentMetricVal, ContinuousLinearMap.map_add, ContinuousLinearMap.add_apply, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply] - map_smul' := λ c ω₁ => by + map_smul' := fun c ω₁ => by ext ω₂ - simp only [cotangentMetricVal, - ContinuousLinearMap.map_smul, - ContinuousLinearMap.smul_apply, - LinearMap.coe_mk, AddHom.coe_mk, - RingHom.id_apply, LinearMap.smul_apply] + simp [cotangentMetricVal, 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) : +/-- 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 only [cotangentMetricVal, - ContinuousLinearMap.map_smul, - ContinuousLinearMap.smul_apply, - smul_smul] + simp [cotangentMetricVal, ContinuousLinearMap.smul_apply] + ring 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⟩ + ⟨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 : PseudoRiemannianMetric E H M n I) (x : M) +lemma cotangentToBilinForm_apply (g : MetricTensor E H M n I) (x : M) (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : - cotangentToBilinForm g x ω₁ ω₂ = cotangentMetricVal g x ω₁ ω₂ := rfl + cotangentToBilinForm g x ω₁ ω₂ = cotangentMetricVal g x ω₁ ω₂ := rfl @[simp] -lemma cotangentToQuadraticForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M) +lemma cotangentToQuadraticForm_apply (g : MetricTensor E H M n I) (x : M) (ω : TangentSpace I x →L[ℝ] ℝ) : - cotangentToQuadraticForm g x ω = cotangentMetricVal g x ω ω := rfl + cotangentToQuadraticForm g x ω = cotangentMetricVal g x ω ω := rfl @[simp] -lemma cotangentToBilinForm_isSymm (g : PseudoRiemannianMetric E H M n I) (x : M) : +lemma cotangentToBilinForm_isSymm (g : MetricTensor E H M n I) (x : M) : (cotangentToBilinForm g x).IsSymm := by refine { eq := ?_ } - intro ω₁ ω₂; simp only [cotangentToBilinForm_apply]; exact cotangentMetricVal_symm g x ω₁ ω₂ + intro ω₁ ω₂ + simpa [cotangentToBilinForm_apply] using (cotangentMetricVal_symm (g := 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) : +/-- 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 @@ -608,32 +651,288 @@ lemma cotangentMetricVal_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x intro w let ω' : TangentSpace I x →L[ℝ] ℝ := g.flatL x w have this : g.sharpL x ω' = w := by - simp only [ω', sharpL_apply_flatL] + simp [ω'] 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 + simp [cotangentMetricVal_eq_apply_sharp] at h_apply + simpa [this] using h_apply exact h_forall v @[simp] -lemma cotangentToBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) : +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 x ω + apply cotangentMetricVal_nondegenerate (g := g) x ω intro v exact hω v · intro ω hω - apply cotangentMetricVal_nondegenerate g x ω + 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 x)]; simp [hω] + 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 -end Cotangent +/-- 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 + +/-- 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*) (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] + [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] : + 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. -/ + sigNeg_isLocallyConstant : + IsLocallyConstant (fun x : M => + have : FiniteDimensional ℝ (TangentSpace I x) := inferInstance + sigNeg (PseudoRiemannianMetric.valToQuadraticForm val symm x)) + +namespace PseudoRiemannianMetric + +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] +variable [inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)] + +/-- 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)` -/ +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)`. -/ +noncomputable abbrev toQuadraticForm (g : PseudoRiemannianMetric E H M n I) (x : M) : + QuadraticForm ℝ (TangentSpace I 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 + 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 + +@[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 + +/-! ## 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 + simp [toBilinForm] + +lemma toBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) : + (toBilinForm g x).Nondegenerate := by + simp [toBilinForm] + +/-- 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 + +/-! ### 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'} + +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) + +end PairingSmoothness + +/-! ## Flat / sharp / cotangent API (delegated to `MetricTensor`) -/ + +/-- 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) + +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) + +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 `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 := + MetricTensor.sharpEquiv (g := (g.toMetricTensor : MetricTensor E H M n I)) x + + /-- 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 + + /-- 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 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] + +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 + simp [flat, sharp] + +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 + simpa [flat, sharp] using + (MetricTensor.sharp_flat_apply (g := (g.toMetricTensor : MetricTensor E H M n I)) x v) + +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 + simp [sharpL] + +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 + simpa [sharpL] using + (MetricTensor.apply_vec_sharp (g := (g.toMetricTensor : MetricTensor E H M n I)) x v ω) + + /-- The induced cotangent metric value `g⁻¹(ω₁, ω₂)`. -/ +noncomputable abbrev cotangentMetricVal (g : PseudoRiemannianMetric E H M n I) (x : M) + (ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) : ℝ := + MetricTensor.cotangentMetricVal (g := (g.toMetricTensor : MetricTensor E H M n I)) x ω₁ ω₂ + + /-- 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 + + /-- 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 + +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) + +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/Riemannian/Defs.lean b/Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean index ef407c697..375f0768f 100644 --- a/Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean +++ b/Physlib/Mathematics/Geometry/Metric/Riemannian/Defs.lean @@ -5,220 +5,114 @@ Authors: Matteo Cipollina -/ module -public import Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs -public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic +import all Physlib.Mathematics.Geometry.Metric.PseudoRiemannian.Defs +import Mathlib.Geometry.Manifold.VectorBundle.Riemannian +import Mathlib.Geometry.Manifold.VectorBundle.Tangent +import Mathlib.LinearAlgebra.QuadraticForm.Signature + /-! -# Riemannian Metric Definitions +# Riemannian metrics (tangent bundle) -This module defines the Riemannian metric, building on pseudo-Riemannian metrics. --/ +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.RiemannianMetric.toPseudoRiemannianMetric`: forget positivity to obtain a + pseudo-Riemannian metric (index `0`). -@[expose] public section +## Tags + +Riemannian, pseudo-Riemannian +-/ 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 -namespace RiemannianMetric +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 {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)] +namespace RiemannianMetric -/-- Coercion from RiemannianMetric to its underlying PseudoRiemannianMetric. -/ -instance : Coe (RiemannianMetric I n M) (PseudoRiemannianMetric E H M (n) I) where - coe g := g.toPseudoRiemannianMetric +variable [∀ 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] @[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 +lemma index_toPseudoRiemannianMetric (g : RiemannianMetric I n M) (x : M) : + sigNeg (g.toPseudoRiemannianMetric.toQuadraticForm 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.toQuadraticForm, toPseudoRiemannianMetric, + MetricTensor.toQuadraticForm] using hx -/-- 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 +instance : Coe (RiemannianMetric I n M) (_root_.PseudoRiemannianMetric E H M n I) := + ⟨toPseudoRiemannianMetric⟩ end RiemannianMetric + +/-! ## Existence helper -/ + +/-- Existence of a Riemannian metric implies existence of a pseudo-Riemannian metric (of index `0`), +by forgetting positivity. -/ +theorem nonempty_pseudoRiemannianMetric_of_nonempty_riemannianMetric + [∀ x : M, FiniteDimensional ℝ (TangentSpace I x)] + (h : Nonempty (RiemannianMetric I n M)) : + Nonempty (_root_.PseudoRiemannianMetric E H M n I) := + h.map RiemannianMetric.toPseudoRiemannianMetric + end -end RiemannianMetric + end PseudoRiemannianMetric