diff --git a/PhysLean.lean b/PhysLean.lean index b45cee7ae..72176fc53 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -52,7 +52,9 @@ import PhysLean.Mathematics.Distribution.PowMul import PhysLean.Mathematics.FDerivCurry import PhysLean.Mathematics.Fin import PhysLean.Mathematics.Fin.Involutions +import PhysLean.Mathematics.Geometry.Metric.Lorentzian.Defs import PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs +import PhysLean.Mathematics.Geometry.Metric.QuadraticForm.NegDim import PhysLean.Mathematics.Geometry.Metric.Riemannian.Defs import PhysLean.Mathematics.InnerProductSpace.Adjoint import PhysLean.Mathematics.InnerProductSpace.Basic diff --git a/PhysLean/Mathematics/Geometry/Metric/Lorentzian/Defs.lean b/PhysLean/Mathematics/Geometry/Metric/Lorentzian/Defs.lean new file mode 100644 index 000000000..50311ed38 --- /dev/null +++ b/PhysLean/Mathematics/Geometry/Metric/Lorentzian/Defs.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2026 Matteo Cipollina. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Matteo Cipollina +-/ + +import PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs + +/-! +# Lorentzian metrics + +This file records the Lorentzian condition (index `1`) for a pseudo-Riemannian metric. + +## Main definitions + +* `PseudoRiemannianMetric.IsLorentzianMetric`: the Prop-valued predicate asserting + `(g.toQuadraticForm x).negDim = 1` for all `x`. + +## Tags + +Lorentzian, pseudo-Riemannian, index +-/ + +namespace PseudoRiemannianMetric + +noncomputable section + +open scoped Manifold + +section + +variable {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] +variable {H : Type w} [TopologicalSpace H] +variable {M : Type w} [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 : PseudoRiemannianMetric E H M n I) : Prop where + negDim_eq_one : ∀ x : M, (g.toQuadraticForm x).negDim = 1 + +namespace IsLorentzianMetric + +variable (g : PseudoRiemannianMetric E H M n I) + +/-- For a Lorentzian metric, the index is `1` at every point. -/ +lemma index_eq_one (x : M) [IsLorentzianMetric (g := g)] : + g.index x = 1 := by + simpa [PseudoRiemannianMetric.index] using + (IsLorentzianMetric.negDim_eq_one (g := g) x) + +end IsLorentzianMetric + +end + +end + +end PseudoRiemannianMetric + +#lint diff --git a/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean b/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean index c5a120a0d..0f7fc1bb8 100644 --- a/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean +++ b/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean @@ -3,191 +3,282 @@ Copyright (c) 2025 Matteo Cipollina. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Matteo Cipollina -/ - -import Mathlib.Analysis.InnerProductSpace.Basic -import Mathlib.Analysis.RCLike.Lemmas -import Mathlib.Geometry.Manifold.MFDeriv.Defs +import Mathlib.Geometry.Manifold.VectorBundle.Riemannian +import Mathlib.Geometry.Manifold.VectorBundle.Tangent import Mathlib.LinearAlgebra.BilinearForm.Properties -import Mathlib.LinearAlgebra.QuadraticForm.Real import Mathlib.Topology.LocallyConstant.Basic +import PhysLean.Mathematics.Geometry.Metric.QuadraticForm.NegDim /-! -# Pseudo-Riemannian Metrics on Smooth Manifolds +# Pseudo-Riemannian metrics + +This file defines pseudo-Riemannian metrics on smooth manifolds, in a way that mirrors Mathlib's +bundle-first Riemannian metric API. -This file formalizes pseudo-Riemannian metrics on smooth manifolds and establishes their basic -properties. +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.negDim`. In finite dimension, a metric induces the usual musical isomorphisms +(`flat`/`sharp`) and an induced metric on the cotangent spaces. -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. +## Main definitions -## Main Definitions +* `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 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. +## Implementation notes -* `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. +Smoothness is stated as a `ContMDiff` assumption for a bundled map `x ↦ TotalSpace.mk' … x (gₓ)` as +in Mathlib. Index-type constructions use `QuadraticForm.negDim` and therefore require +finite-dimensional tangent spaces. -* `PseudoRiemannianMetric.sharpEquiv g x`: The inverse of the flat isomorphism, mapping from - the dual space back to the tangent space. +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`. -* `PseudoRiemannianMetric.toQuadraticForm g x`: The quadratic form `v ↦ gₓ(v, v)` associated - with the metric at point `x`. +## Tags -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[ℝ] ℝ`. +pseudo-Riemannian, metric tensor, musical isomorphisms, index -## Reference +## References -* 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 +* 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] - -/-- 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)`. --/ -private def pseudoRiemannianMetricValToQuadraticForm +/-! ## Bundle-level infrastructure (Mathlib-style) -/ + +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)\). -/ +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. -/ +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.negDim`) from bundled +metric data; compare O'Neill, *Semi-Riemannian Geometry* (1983), p. 47. -/ +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) @@ -207,397 +298,350 @@ private 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. -/ +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. -/ +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. -/ +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 - -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 +/-- 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 -/-- 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 @@ -605,32 +649,292 @@ 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) : ℕ := + (g.toQuadraticForm x).negDim + +@[simp] +lemma index_def (g : MetricTensor E H M n I) (x : M) : + g.index x = (g.toQuadraticForm x).negDim := + 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.negDim`) 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 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 + (PseudoRiemannianMetric.valToQuadraticForm val symm x).negDim) + +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)` -/ +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) : + 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) : ℕ := + (g.toQuadraticForm x).negDim + +@[simp] +lemma index_def (g : PseudoRiemannianMetric E H M n I) (x : M) : + g.index x = (g.toQuadraticForm x).negDim := + rfl + +lemma index_isLocallyConstant (g : PseudoRiemannianMetric E H M n I) : + IsLocallyConstant (fun x : M => g.index x) := by + simpa [index, toQuadraticForm] using g.negDim_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. -/ +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_signature_eq (g : PseudoRiemannianMetric E H M n I) (x : M) : + (g.cotangentToQuadraticForm x).signature = (g.toQuadraticForm x).signature := by + exact + QuadraticForm.signature_eq_of_equivalent (E := (TangentSpace I x →L[ℝ] ℝ)) + (E₂ := TangentSpace I x) (cotangentToQuadraticForm_equivalent_toQuadraticForm (g := g) x) + +theorem cotangent_negDim_eq (g : PseudoRiemannianMetric E H M n I) (x : M) : + (g.cotangentToQuadraticForm x).negDim = (g.toQuadraticForm x).negDim := by + exact congrArg QuadraticForm.Signature.neg (cotangent_signature_eq (g := g) x) end PseudoRiemannianMetric -end end PseudoRiemannianMetric diff --git a/PhysLean/Mathematics/Geometry/Metric/QuadraticForm/NegDim.lean b/PhysLean/Mathematics/Geometry/Metric/QuadraticForm/NegDim.lean new file mode 100644 index 000000000..7a7355e9e --- /dev/null +++ b/PhysLean/Mathematics/Geometry/Metric/QuadraticForm/NegDim.lean @@ -0,0 +1,830 @@ +/- +Copyright (c) 2026 Matteo Cipollina. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Matteo Cipollina +-/ + +import Mathlib.LinearAlgebra.QuadraticForm.Real +import Mathlib.Algebra.Module.Submodule.Map +import Mathlib.Data.Nat.Lattice +import Mathlib.LinearAlgebra.Dimension.Constructions +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas + +/-! +# Inertia indices for real quadratic forms + +This file defines canonical inertia data for a real quadratic form on a finite-dimensional real +vector space. + +The main construction is `QuadraticForm.posIndex`, the maximal dimension of a submodule on which a +quadratic form is positive definite. From this we define the canonical indices +`QuadraticForm.posDim`, `QuadraticForm.negDim`, `QuadraticForm.zeroDim`, and the canonical +`QuadraticForm.signature`. + +These constructions are invariant under `QuadraticForm.Equivalent` and do not depend on a choice of +diagonalization. + +## Main definitions + +- `QuadraticForm.posIndex`: maximal dimension of a submodule where `Q` is positive definite +- `QuadraticForm.posDim`: positive index of inertia (defined as `posIndex Q`) +- `QuadraticForm.negDim`: negative index of inertia (defined as `posIndex (-Q)`) +- `QuadraticForm.zeroDim`: nullity, defined so `posDim + negDim + zeroDim = finrank` +- `QuadraticForm.signature`: the triple `(posDim, negDim, zeroDim)` + +## Implementation notes + +Noncanonical Sylvester-diagonalization choices (`QuadraticForm.signTypeWeights`, +`QuadraticForm.signatureChoice`, and the bridge lemmas relating them to the canonical indices) are +kept in `PhysLean.Mathematics.Geometry.Metric.QuadraticForm.Sylvester`. + +## Tags + +quadratic form, inertia, signature, Sylvester law, index +-/ + +namespace QuadraticForm + +open Finset Module QuadraticMap SignType +open scoped BigOperators + +/-! ### Signature and indices -/ + +/-- A (finite-dimensional) real quadratic form has a signature `(pos, neg, zero)` given by +Sylvester's law of inertia: the numbers of positive, negative, and zero squares in a diagonal +representation. -/ +@[ext] structure Signature where + /-- The positive index of inertia. -/ + pos : ℕ + /-- The negative index of inertia. -/ + neg : ℕ + /-- The nullity (dimension of the radical). -/ + zero : ℕ + +namespace Signature + +/-- Alias for the `zero` component (common terminology: nullity). -/ +abbrev nullity (s : Signature) : ℕ := s.zero + +end Signature + +/-- For a 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] + +/-- When a quadratic form is equivalent to a weighted sum of squares, negative weights correspond +to vectors where the form takes negative values. -/ +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 diagonalization. -/ +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 + +/-! +### Inertia uniqueness (canonical indices) + +We want the signature counts to be invariants (independent +of the choice of diagonalization). We provide the key intermediate notion of +the **positive index**, defined as the maximum dimension of a subspace on which the form is +positive definite. + +In this file we prove invariance of this index under `QuadraticForm.Equivalent`. In a subsequent +step, one computes this index for diagonal `weightedSumSquares` forms, and deduces uniqueness of +the inertia counts. +-/ + +section InertiaUniqueness + +variable {V : Type*} [AddCommGroup V] [Module ℝ V] + +/-- `IsPosDefOn Q W` means that the restriction of `Q` to the submodule `W` is positive definite. -/ +def IsPosDefOn (Q : QuadraticForm ℝ V) (W : Submodule ℝ V) : Prop := + (Q.comp W.subtype).PosDef + +/-- Predicate asserting that a real quadratic form admits a positive definite submodule of +dimension `k`. -/ +def PosIndexPred (Q : QuadraticForm ℝ V) (k : ℕ) : Prop := + ∃ W : Submodule ℝ V, FiniteDimensional ℝ W ∧ finrank ℝ W = k ∧ IsPosDefOn (V := V) Q W + +private lemma posIndexPred_zero (Q : QuadraticForm ℝ V) : + PosIndexPred (V := V) Q 0 := by + refine ⟨(⊥ : Submodule ℝ V), ?_, by simp, ?_⟩ + · infer_instance + intro x hx + exfalso + exact hx (Subsingleton.elim x 0) + +private lemma posIndexPred_le_finrank [FiniteDimensional ℝ V] {Q : QuadraticForm ℝ V} {k : ℕ} + (hk : PosIndexPred (V := V) Q k) : k ≤ finrank ℝ V := by + rcases hk with ⟨W, hWfd, hW, -⟩ + haveI : FiniteDimensional ℝ W := hWfd + have hk_le : finrank ℝ W ≤ finrank ℝ V := + Submodule.finrank_le (R := ℝ) (M := V) W + simpa [hW] using hk_le + +/-- The positive index of a real quadratic form: the maximal dimension of a subspace on which the +form is positive definite. -/ +noncomputable def posIndex (Q : QuadraticForm ℝ V) : ℕ := + sSup {k : ℕ | PosIndexPred (V := V) Q k} + +private lemma posIndex_nonempty (Q : QuadraticForm ℝ V) : + ({k : ℕ | PosIndexPred (V := V) Q k} : Set ℕ).Nonempty := + ⟨0, posIndexPred_zero (V := V) Q⟩ + +private lemma posIndex_bddAbove [FiniteDimensional ℝ V] (Q : QuadraticForm ℝ V) : + BddAbove ({k : ℕ | PosIndexPred (V := V) Q k} : Set ℕ) := by + refine ⟨finrank ℝ V, ?_⟩ + intro k hk + exact posIndexPred_le_finrank (V := V) (Q := Q) hk + +lemma posIndex_spec [FiniteDimensional ℝ V] (Q : QuadraticForm ℝ V) : + ∃ W : Submodule ℝ V, finrank ℝ W = posIndex (V := V) Q ∧ IsPosDefOn (V := V) Q W := by + have hmem : + posIndex (V := V) Q ∈ ({k : ℕ | PosIndexPred (V := V) Q k} : Set ℕ) := by + simpa [posIndex] using + (Nat.sSup_mem (s := ({k : ℕ | PosIndexPred (V := V) Q k} : Set ℕ)) + (posIndex_nonempty (V := V) Q) (posIndex_bddAbove (V := V) Q)) + rcases hmem with ⟨W, hWfd, hW, hWpos⟩ + haveI : FiniteDimensional ℝ W := hWfd + exact ⟨W, hW, hWpos⟩ + +lemma le_posIndex_of_exists [FiniteDimensional ℝ V] {Q : QuadraticForm ℝ V} {k : ℕ} + (hk : PosIndexPred (V := V) Q k) : + k ≤ posIndex (V := V) Q := by + have hb : BddAbove ({k : ℕ | PosIndexPred (V := V) Q k} : Set ℕ) := + posIndex_bddAbove (V := V) Q + simpa [posIndex] using (le_csSup hb hk) + +/- If `Q` and `Q₂` are equivalent, then `posIndex Q ≤ posIndex Q₂`. -/ +lemma posIndex_le_of_equivalent [FiniteDimensional ℝ V] {V₂ : Type*} [AddCommGroup V₂] [Module ℝ V₂] + [FiniteDimensional ℝ V₂] {Q : QuadraticForm ℝ V} {Q₂ : QuadraticForm ℝ V₂} + (h : Q.Equivalent Q₂) : + posIndex (V := V) Q ≤ posIndex (V := V₂) Q₂ := by + rcases h with ⟨e⟩ + rcases posIndex_spec (Q := Q) with ⟨W, hWfin, hWpos⟩ + let f : V →ₗ[ℝ] V₂ := (e.toLinearEquiv : V ≃ₗ[ℝ] V₂).toLinearMap + have hf_inj : Function.Injective f := e.toLinearEquiv.injective + let W₂ : Submodule ℝ V₂ := W.map f + have hfinrank : finrank ℝ W₂ = finrank ℝ W := by + simpa [W₂] using (LinearEquiv.finrank_eq (Submodule.equivMapOfInjective f hf_inj W)).symm + have hW₂pos : IsPosDefOn (V := V₂) Q₂ W₂ := by + intro x hx + rcases x with ⟨xv, hxv⟩ + have hx0 : (⟨xv, by simpa [W₂] using hxv⟩ : W.map f) ≠ 0 := by + intro h0 + apply hx + ext + simpa using congrArg Subtype.val h0 + let eqv := Submodule.equivMapOfInjective f hf_inj W + set x' : W.map f := ⟨xv, by simpa [W₂] using hxv⟩ + have hx' : (eqv.symm x') ≠ 0 := by + intro h0 + apply hx0 + have := congrArg eqv h0 + simpa using this + have hpos' : 0 < (Q.comp W.subtype) (eqv.symm x') := hWpos _ hx' + have hxmap : f ((eqv.symm x' : W) : V) = (x' : V₂) := + Submodule.map_equivMapOfInjective_symm_apply f hf_inj W x' + have heq : Q₂ (x' : V₂) = Q ((eqv.symm x' : W) : V) := by + have : Q₂ (f ((eqv.symm x' : W) : V)) = Q ((eqv.symm x' : W) : V) := by + simp [f] + simpa [hxmap] using this + simpa [IsPosDefOn, QuadraticMap.comp_apply, heq, x'] using hpos' + have hk : + PosIndexPred (V := V₂) Q₂ (posIndex (V := V) Q) := by + refine ⟨W₂, ?_, ?_, hW₂pos⟩ + · infer_instance + · simp [hWfin, hfinrank] + exact le_posIndex_of_exists (V := V₂) hk + +/-- `posIndex` is invariant under equivalence of quadratic forms. -/ +theorem posIndex_eq_of_equivalent [FiniteDimensional ℝ V] {V₂ : Type*} [AddCommGroup V₂] + [Module ℝ V₂] + [FiniteDimensional ℝ V₂] {Q : QuadraticForm ℝ V} {Q₂ : QuadraticForm ℝ V₂} + (h : Q.Equivalent Q₂) : + posIndex (V := V) Q = posIndex (V := V₂) Q₂ := by + refine le_antisymm (posIndex_le_of_equivalent (V := V) (V₂ := V₂) (Q := Q) (Q₂ := Q₂) h) ?_ + rcases h with ⟨e⟩ + exact posIndex_le_of_equivalent (V := V₂) (V₂ := V) (Q := Q₂) (Q₂ := Q) ⟨e.symm⟩ + +end InertiaUniqueness + +/-! ### Canonical signature and indices -/ + +section Canonical + +variable {E : Type*} [AddCommGroup E] [Module ℝ E] + +lemma posIndex_le_finrank [FiniteDimensional ℝ E] (Q : QuadraticForm ℝ E) : + posIndex (V := E) Q ≤ finrank ℝ E := by + let s : Set ℕ := {k : ℕ | PosIndexPred (V := E) Q k} + have hsne : s.Nonempty := ⟨0, posIndexPred_zero (V := E) Q⟩ + refine (csSup_le hsne) ?_ + intro k hk + exact posIndexPred_le_finrank (V := E) (Q := Q) hk + +/-- The positive index of inertia of a real quadratic form (canonical). -/ +noncomputable def posDim (Q : QuadraticForm ℝ E) : ℕ := + posIndex (V := E) Q + +/-- The negative index of inertia of a real quadratic form (canonical). -/ +noncomputable def negDim (Q : QuadraticForm ℝ E) : ℕ := + posIndex (V := E) (-Q) + +@[simp] +lemma posDim_def (Q : QuadraticForm ℝ E) : + Q.posDim = posIndex (V := E) Q := rfl + +@[simp] +lemma negDim_def (Q : QuadraticForm ℝ E) : + Q.negDim = posIndex (V := E) (-Q) := rfl + +lemma posDim_le_finrank [FiniteDimensional ℝ E] (Q : QuadraticForm ℝ E) : Q.posDim ≤ finrank ℝ E := + posIndex_le_finrank (E := E) Q + +lemma negDim_le_finrank [FiniteDimensional ℝ E] (Q : QuadraticForm ℝ E) : Q.negDim ≤ finrank ℝ E := + posIndex_le_finrank (E := E) (-Q) + +@[simp] +lemma posDim_neg (Q : QuadraticForm ℝ E) : (-Q).posDim = Q.negDim := rfl + +lemma negDim_neg (Q : QuadraticForm ℝ E) : (-Q).negDim = Q.posDim := by + simp [negDim, posDim] + +lemma posDim_add_negDim_le_finrank [FiniteDimensional ℝ E] (Q : QuadraticForm ℝ E) : + Q.posDim + Q.negDim ≤ finrank ℝ E := by + rcases posIndex_spec (Q := Q) with ⟨Wpos, hWpos, hpos⟩ + rcases posIndex_spec (Q := -Q) with ⟨Wneg, hWneg, hneg⟩ + have hdisj : Disjoint Wpos Wneg := by + rw [Submodule.disjoint_def] + intro x hxpos hxneg + by_contra hx0 + have hxpos' : 0 < Q x := by + have : 0 < (Q.comp Wpos.subtype) ⟨x, hxpos⟩ := hpos ⟨x, hxpos⟩ (by simpa using hx0) + simpa [IsPosDefOn, QuadraticMap.comp_apply] using this + have hxneg' : Q x < 0 := by + have : 0 < ((-Q).comp Wneg.subtype) ⟨x, hxneg⟩ := hneg ⟨x, hxneg⟩ (by simpa using hx0) + have : 0 < (-Q) x := by simpa [IsPosDefOn, QuadraticMap.comp_apply] using this + simpa using (neg_pos.mp this) + exact (not_lt_of_gt hxpos') hxneg' + have hdim : finrank ℝ Wpos + finrank ℝ Wneg ≤ finrank ℝ E := + Submodule.finrank_add_finrank_le_of_disjoint hdisj + simpa [posDim, negDim, hWpos, hWneg] using hdim + +/-- The nullity of a real quadratic form, defined so that `pos + neg + zero = finrank`. -/ +noncomputable def zeroDim (Q : QuadraticForm ℝ E) : ℕ := + finrank ℝ E - Q.posDim - Q.negDim + +@[simp] +lemma zeroDim_def (Q : QuadraticForm ℝ E) : + Q.zeroDim = finrank ℝ E - Q.posDim - Q.negDim := rfl + +lemma zeroDim_neg (Q : QuadraticForm ℝ E) : (-Q).zeroDim = Q.zeroDim := by + simp [zeroDim, posDim, negDim, Nat.sub_sub, Nat.add_comm] + +/-- The signature `(pos, neg, zero)` of a real quadratic form (canonical). -/ +noncomputable def signature (Q : QuadraticForm ℝ E) : Signature := + ⟨Q.posDim, Q.negDim, Q.zeroDim⟩ + +@[simp] +lemma signature_pos (Q : QuadraticForm ℝ E) : Q.signature.pos = Q.posDim := + rfl + +@[simp] +lemma signature_neg (Q : QuadraticForm ℝ E) : Q.signature.neg = Q.negDim := + rfl + +@[simp] +lemma signature_zero (Q : QuadraticForm ℝ E) : Q.signature.zero = Q.zeroDim := + rfl + +@[simp] +lemma signature_def (Q : QuadraticForm ℝ E) : + Q.signature = ⟨Q.posDim, Q.negDim, Q.zeroDim⟩ := + rfl + +lemma posDim_add_negDim_add_zeroDim [FiniteDimensional ℝ E] (Q : QuadraticForm ℝ E) : + Q.posDim + Q.negDim + Q.zeroDim = finrank ℝ E := by + set n : ℕ := finrank ℝ E + set p : ℕ := Q.posDim + set m : ℕ := Q.negDim + have hp : p ≤ n := by + simpa [p, n] using (posDim_le_finrank (E := E) Q) + have hpm : p + m ≤ n := by + simpa [p, m, n] using (posDim_add_negDim_le_finrank (E := E) Q) + have hm : m ≤ n - p := by + exact (Nat.le_sub_iff_add_le hp).2 (by simpa [Nat.add_comm, p, m, n] using hpm) + calc + Q.posDim + Q.negDim + Q.zeroDim + = p + m + (n - p - m) := by simp [zeroDim, n, p, m] + _ = p + (m + ((n - p) - m)) := by + simp [Nat.add_assoc] + _ = p + (n - p) := by + simp [Nat.add_sub_of_le hm] + _ = n := by + simp [Nat.add_sub_of_le hp] + +lemma signature_sum [FiniteDimensional ℝ E] (Q : QuadraticForm ℝ E) : + Q.signature.pos + Q.signature.neg + Q.signature.zero = finrank ℝ E := by + simpa using (posDim_add_negDim_add_zeroDim (E := E) Q) + +/-- For a positive definite quadratic form, `posDim = finrank`. -/ +theorem posDim_posDef [FiniteDimensional ℝ E] {Q : QuadraticForm ℝ E} (hQ : Q.PosDef) : + Q.posDim = finrank ℝ E := by + apply le_antisymm (posDim_le_finrank (E := E) Q) + have hk : + PosIndexPred (V := E) Q (finrank ℝ E) := by + refine ⟨(⊤ : Submodule ℝ E), ?_, by simp, ?_⟩ + · infer_instance + intro x hx + have hx' : (x : E) ≠ 0 := by + intro h0 + apply hx + ext + simp [h0] + simpa [IsPosDefOn, QuadraticMap.comp_apply] using (hQ (x : E) hx') + have : finrank ℝ E ≤ posIndex (V := E) Q := + le_posIndex_of_exists (V := E) (k := finrank ℝ E) hk + simpa [posDim] using this + +/-- For a positive definite quadratic form, `negDim = 0`. -/ +theorem negDim_posDef [FiniteDimensional ℝ E] {Q : QuadraticForm ℝ E} (hQ : Q.PosDef) : + Q.negDim = 0 := by + rcases posIndex_spec (Q := -Q) with ⟨W, hW, hWpos⟩ + have hWbot : W = ⊥ := by + ext x + constructor + · intro hx + by_contra hx0 + have hpos' : 0 < ((-Q).comp W.subtype) ⟨x, hx⟩ := hWpos ⟨x, hx⟩ (by + intro h0; apply hx0; simpa using congrArg Subtype.val h0) + have hneg' : Q x < 0 := by + have : 0 < (-Q) x := by simpa [QuadraticMap.comp_apply] using hpos' + simpa using (neg_pos.mp this) + have hposQ : 0 < Q x := hQ x hx0 + exact (not_lt_of_gt hposQ) hneg' + · intro hx + have hx0 : x = 0 := by + simpa [Submodule.mem_bot] using hx + simp [hx0] + have hfin0 : finrank ℝ W = 0 := by simp [hWbot] + have : posIndex (V := E) (-Q) = 0 := by simpa [hW] using hfin0 + simp [negDim, this] + +/-- For a positive definite quadratic form, `zeroDim = 0`. -/ +theorem zeroDim_posDef [FiniteDimensional ℝ E] {Q : QuadraticForm ℝ E} (hQ : Q.PosDef) : + Q.zeroDim = 0 := by + have hpos : Q.posDim = finrank ℝ E := posDim_posDef (E := E) hQ + have hneg : Q.negDim = 0 := negDim_posDef (E := E) hQ + have hpos' : posIndex (V := E) Q = finrank ℝ E := by simpa [posDim] using hpos + have hneg' : posIndex (V := E) (-Q) = 0 := by simpa [negDim] using hneg + simp [zeroDim, posDim, negDim, hpos', hneg'] + +lemma Equivalent.neg {E₂ : Type*} [AddCommGroup E₂] [Module ℝ E₂] + {Q : QuadraticForm ℝ E} {Q₂ : QuadraticForm ℝ E₂} (h : Q.Equivalent Q₂) : + (-Q).Equivalent (-Q₂) := by + rcases h with ⟨e⟩ + refine ⟨?_⟩ + refine + { toLinearEquiv := e.toLinearEquiv + map_app' := fun x => ?_ } + simp + +theorem posDim_eq_of_equivalent [FiniteDimensional ℝ E] {E₂ : Type*} [AddCommGroup E₂] [Module ℝ E₂] + [FiniteDimensional ℝ E₂] + {Q : QuadraticForm ℝ E} {Q₂ : QuadraticForm ℝ E₂} (h : Q.Equivalent Q₂) : + Q.posDim = Q₂.posDim := by + simp [posDim, posIndex_eq_of_equivalent (Q := Q) (Q₂ := Q₂) h] + +theorem negDim_eq_of_equivalent [FiniteDimensional ℝ E] {E₂ : Type*} [AddCommGroup E₂] [Module ℝ E₂] + [FiniteDimensional ℝ E₂] + {Q : QuadraticForm ℝ E} {Q₂ : QuadraticForm ℝ E₂} (h : Q.Equivalent Q₂) : + Q.negDim = Q₂.negDim := by + have h' : (-Q).Equivalent (-Q₂) := Equivalent.neg (E := E) (E₂ := E₂) h + simp [negDim, posIndex_eq_of_equivalent (Q := -Q) (Q₂ := -Q₂) h'] + +theorem zeroDim_eq_of_equivalent [FiniteDimensional ℝ E] {E₂ : Type*} [AddCommGroup E₂] + [Module ℝ E₂] + [FiniteDimensional ℝ E₂] + {Q : QuadraticForm ℝ E} {Q₂ : QuadraticForm ℝ E₂} (h : Q.Equivalent Q₂) : + Q.zeroDim = Q₂.zeroDim := by + rcases h with ⟨e⟩ + have hfin : finrank ℝ E = finrank ℝ E₂ := LinearEquiv.finrank_eq e.toLinearEquiv + have hposI : posIndex (V := E) Q = posIndex (V := E₂) Q₂ := + posIndex_eq_of_equivalent (Q := Q) (Q₂ := Q₂) ⟨e⟩ + have hnegI : posIndex (V := E) (-Q) = posIndex (V := E₂) (-Q₂) := + posIndex_eq_of_equivalent (Q := -Q) (Q₂ := -Q₂) (Equivalent.neg (E := E) (E₂ := E₂) ⟨e⟩) + simp [zeroDim, posDim, negDim, hfin, hposI, hnegI] + +theorem signature_eq_of_equivalent [FiniteDimensional ℝ E] {E₂ : Type*} [AddCommGroup E₂] + [Module ℝ E₂] + [FiniteDimensional ℝ E₂] + {Q : QuadraticForm ℝ E} {Q₂ : QuadraticForm ℝ E₂} (h : Q.Equivalent Q₂) : + Q.signature = Q₂.signature := by + rcases h with ⟨e⟩ + have hfin : finrank ℝ E = finrank ℝ E₂ := LinearEquiv.finrank_eq e.toLinearEquiv + have hposI : posIndex (V := E) Q = posIndex (V := E₂) Q₂ := + posIndex_eq_of_equivalent (Q := Q) (Q₂ := Q₂) ⟨e⟩ + have hnegI : posIndex (V := E) (-Q) = posIndex (V := E₂) (-Q₂) := + posIndex_eq_of_equivalent (Q := -Q) (Q₂ := -Q₂) (Equivalent.neg (E := E) (E₂ := E₂) ⟨e⟩) + ext <;> simp [signature, posDim, negDim, zeroDim, hfin, hposI, hnegI] + +end Canonical + +/-! +### Diagonal computation + +We compute the canonical indices for the diagonal form `weightedSumSquares` with `SignType` weights. +This is the key bridge between the canonical `posIndex`-based definition and Mathlib's Sylvester +diagonalization existence theorem. +-/ + +section Diagonal + +open scoped BigOperators + +noncomputable section + +variable {n : ℕ} + +/-- The diagonal quadratic form with `SignType` weights `w`, i.e. the weighted sum of squares +with weights in `{ -1, 0, 1 }`. -/ +abbrev diagForm (w : Fin n → SignType) : QuadraticForm ℝ (Fin n → ℝ) := + QuadraticMap.weightedSumSquares ℝ fun i => (w i : ℝ) + +/-- The set of indices where `w` takes the value `s`. -/ +def signSet (s : SignType) (w : Fin n → SignType) : Finset (Fin n) := + Finset.univ.filter fun i => w i = s + +/-- The set of indices where `w` is positive. -/ +abbrev posSet (w : Fin n → SignType) : Finset (Fin n) := + signSet (n := n) SignType.pos w + +/-- The set of indices where `w` is negative. -/ +abbrev negSet (w : Fin n → SignType) : Finset (Fin n) := + signSet (n := n) SignType.neg w + +/-- The set of indices where `w` is zero. -/ +abbrev zeroSet (w : Fin n → SignType) : Finset (Fin n) := + signSet (n := n) 0 w + +lemma mem_posSet {w : Fin n → SignType} {i : Fin n} : + i ∈ posSet (n := n) w ↔ w i = SignType.pos := by + simp [posSet, signSet] + +lemma mem_negSet {w : Fin n → SignType} {i : Fin n} : + i ∈ negSet (n := n) w ↔ w i = SignType.neg := by + simp [negSet, signSet] + +lemma mem_zeroSet {w : Fin n → SignType} {i : Fin n} : + i ∈ zeroSet (n := n) w ↔ w i = 0 := by + simp [zeroSet, signSet] + +lemma posSet_neg (w : Fin n → SignType) : + posSet (n := n) (fun i => -w i) = negSet (n := n) w := by + ext i + cases hi : w i <;> simp [posSet, negSet, signSet, hi] + +/-- The submodule of vectors supported on the positive-weight coordinates. -/ +def supportedOnPos (w : Fin n → SignType) : Submodule ℝ (Fin n → ℝ) where + carrier := {v | ∀ i, w i ≠ SignType.pos → v i = 0} + zero_mem' := by intro i hi; simp + add_mem' := by + intro v₁ v₂ hv₁ hv₂ i hi + simp [Pi.add_apply, hv₁ i hi, hv₂ i hi] + smul_mem' := by + intro a v hv i hi + simp [Pi.smul_apply, hv i hi] + +@[simp] +lemma mem_supportedOnPos {w : Fin n → SignType} {v : Fin n → ℝ} : + v ∈ supportedOnPos (n := n) w ↔ ∀ i, w i ≠ SignType.pos → v i = 0 := + Iff.rfl + +/-- Restriction of a vector to the positive-weight coordinates. -/ +def restrictPos (w : Fin n → SignType) : + (Fin n → ℝ) →ₗ[ℝ] ({i // i ∈ posSet (n := n) w} → ℝ) where + toFun v i := v i.1 + map_add' := by intro v₁ v₂; ext i; rfl + map_smul' := by intro a v; ext i; rfl + +@[simp] +lemma restrictPos_apply {w : Fin n → SignType} (v : Fin n → ℝ) + (i : {i // i ∈ posSet (n := n) w}) : restrictPos (n := n) w v i = v i.1 := + rfl + +/-- If a vector has no positive-weight coordinates, then its value under `diagForm w` is +nonpositive. -/ +lemma diagForm_nonpos_of_no_pos {w : Fin n → SignType} {v : Fin n → ℝ} + (hv : ∀ i, w i = SignType.pos → v i = 0) : + diagForm (n := n) w v ≤ 0 := by + simp only [diagForm, QuadraticMap.weightedSumSquares_apply] + refine Finset.sum_nonpos ?_ + intro i _ + cases hwi : w i <;> simp [hwi, hv i, mul_self_nonneg] + +/-- On `supportedOnPos w`, the diagonal form `diagForm w` is positive definite. -/ +lemma isPosDefOn_diagForm_supportedOnPos (w : Fin n → SignType) : + IsPosDefOn (V := Fin n → ℝ) (diagForm (n := n) w) (supportedOnPos (n := n) w) := by + intro v hv0 + -- pick a coordinate where `v` is nonzero + have hv' : ∃ i, (v : Fin n → ℝ) i ≠ 0 := by + by_contra h + apply hv0 + ext i + have : (v : Fin n → ℝ) i = 0 := by + by_contra hi + exact h ⟨i, hi⟩ + simpa using this + rcases hv' with ⟨i, hi⟩ + have hwpos : w i = SignType.pos := by + by_contra hne + have : (v : Fin n → ℝ) i = 0 := by + exact (mem_supportedOnPos (n := n) (w := w) |>.1 v.property) i hne + exact hi this + have hterm_pos : 0 < (v : Fin n → ℝ) i ^ 2 := by + simpa [pow_two] using sq_pos_of_ne_zero hi + have hle : + (v : Fin n → ℝ) i ^ 2 ≤ diagForm (n := n) w (v : Fin n → ℝ) := by + simp only [diagForm, QuadraticMap.weightedSumSquares_apply] + have hnonneg : + ∀ j : Fin n, 0 ≤ ((w j : ℝ) • ((v : Fin n → ℝ) j * (v : Fin n → ℝ) j)) := by + intro j + by_cases hj : w j = SignType.pos + · simp [hj, mul_self_nonneg] + · have : (v : Fin n → ℝ) j = 0 := (mem_supportedOnPos (n := n) (w := w)).1 v.property j hj + simp [this] + have : ((w i : ℝ) • ((v : Fin n → ℝ) i * (v : Fin n → ℝ) i)) + ≤ ∑ j : Fin n, (w j : ℝ) • ((v : Fin n → ℝ) j * (v : Fin n → ℝ) j) := by + refine Finset.single_le_sum (fun j _ => hnonneg j) ?_ + simp + simpa [hwpos, pow_two] using this + exact lt_of_lt_of_le hterm_pos hle + +/-- The submodule `supportedOnPos w` is linearly equivalent to functions on the positive index +set. -/ +noncomputable def supportedOnPosEquiv (w : Fin n → SignType) : + supportedOnPos (n := n) w ≃ₗ[ℝ] ({i // i ∈ posSet (n := n) w} → ℝ) := by + refine + { toLinearMap := + { toFun := fun v i => (v : Fin n → ℝ) i.1 + map_add' := by intro v₁ v₂; ext i; rfl + map_smul' := by intro a v; ext i; rfl } + invFun := fun u => + ⟨fun i => if h : i ∈ posSet (n := n) w then u ⟨i, h⟩ else 0, by + intro i hi + by_cases h : i ∈ posSet (n := n) w + · exfalso + exact hi ((mem_posSet (n := n) (w := w)).1 h) + · simp [h]⟩ + left_inv := by + intro v + ext i + by_cases h : i ∈ posSet (n := n) w + · have : w i = SignType.pos := (mem_posSet (n := n) (w := w)).1 h + simp [h] + · have : w i ≠ SignType.pos := by + intro hpos + exact h ((mem_posSet (n := n) (w := w)).2 hpos) + have : (v : Fin n → ℝ) i = 0 := + (mem_supportedOnPos (n := n) (w := w)).1 v.property i this + simp [h, this] + right_inv := by + intro u + ext i + simp } + +lemma finrank_supportedOnPos (w : Fin n → SignType) : + finrank ℝ (supportedOnPos (n := n) w) = (posSet (n := n) w).card := by + have h : + finrank ℝ ({i // i ∈ posSet (n := n) w} → ℝ) = (posSet (n := n) w).card := by + change finrank ℝ ((posSet (n := n) w) → ℝ) = (posSet (n := n) w).card + calc + finrank ℝ ((posSet (n := n) w) → ℝ) = Fintype.card (posSet (n := n) w) := by + simp [Module.finrank_fintype_fun_eq_card] + _ = (posSet (n := n) w).card := by + simp + simpa [h] using (LinearEquiv.finrank_eq (supportedOnPosEquiv (n := n) w)) + +private theorem posIndex_diag_signType (w : Fin n → SignType) : + posIndex (V := Fin n → ℝ) (diagForm (n := n) w) = (posSet (n := n) w).card := by + have h_lower : + (posSet (n := n) w).card ≤ posIndex (V := Fin n → ℝ) (diagForm (n := n) w) := by + have hk : + PosIndexPred (V := Fin n → ℝ) (diagForm (n := n) w) (posSet (n := n) w).card := by + refine ⟨supportedOnPos (n := n) w, ?_, finrank_supportedOnPos (n := n) w, ?_⟩ + · infer_instance + · exact isPosDefOn_diagForm_supportedOnPos (n := n) w + exact le_posIndex_of_exists (V := Fin n → ℝ) (Q := diagForm (n := n) w) hk + -- upper bound: any positive definite subspace injects into the positive coordinates + have h_upper : + posIndex (V := Fin n → ℝ) (diagForm (n := n) w) ≤ (posSet (n := n) w).card := by + rcases posIndex_spec (Q := diagForm (n := n) w) with ⟨W, hW, hWpos⟩ + let f := restrictPos (n := n) w + let g : W →ₗ[ℝ] ({i // i ∈ posSet (n := n) w} → ℝ) := f.comp W.subtype + have hg_inj : Function.Injective g := by + intro x y hxy + have : g (x - y) = 0 := by + simpa [g, map_sub] using congrArg (fun z => z - g y) hxy + have hvanish : ∀ i, w i = SignType.pos → ((x - y : W) : (Fin n → ℝ)) i = 0 := by + intro i hi + have : (g (x - y)) ⟨i, (mem_posSet (n := n) (w := w)).2 hi⟩ = 0 := by + simp [this] + simpa [g, f, restrictPos_apply] using this + have hnonpos : + diagForm (n := n) w ((x - y : W) : (Fin n → ℝ)) ≤ 0 := + diagForm_nonpos_of_no_pos (n := n) (w := w) hvanish + by_cases hxy0 : x - y = 0 + · have : x = y := sub_eq_zero.mp hxy0 + exact this + · have hpos : 0 < (diagForm (n := n) w).comp W.subtype (x - y) := hWpos _ hxy0 + have : ¬ (0 < (diagForm (n := n) w).comp W.subtype (x - y)) := + not_lt_of_ge (by simpa [QuadraticMap.comp_apply] using hnonpos) + exact (this hpos).elim + have hfin_le : + finrank ℝ W ≤ (posSet (n := n) w).card := by + let eW : W ≃ₗ[ℝ] LinearMap.range g := LinearEquiv.ofInjective g hg_inj + have hWrange : finrank ℝ W = finrank ℝ (LinearMap.range g) := LinearEquiv.finrank_eq eW + have hrange_le : + finrank ℝ (LinearMap.range g) ≤ finrank ℝ ({i // i ∈ posSet (n := n) w} → ℝ) := + Submodule.finrank_le (R := ℝ) (M := ({i // i ∈ posSet (n := n) w} → ℝ)) (LinearMap.range g) + have htarget : + finrank ℝ ({i // i ∈ posSet (n := n) w} → ℝ) = (posSet (n := n) w).card := by + change finrank ℝ ((posSet (n := n) w) → ℝ) = (posSet (n := n) w).card + calc + finrank ℝ ((posSet (n := n) w) → ℝ) = Fintype.card (posSet (n := n) w) := by + simp [Module.finrank_fintype_fun_eq_card] + _ = (posSet (n := n) w).card := by + simp + simpa [hWrange, htarget] using hrange_le + simpa [hW] using hfin_le + exact le_antisymm h_upper h_lower + +theorem posIndex_weightedSumSquares_signType (w : Fin n → SignType) : + posIndex (V := Fin n → ℝ) + (QuadraticMap.weightedSumSquares ℝ fun i : Fin n => (w i : ℝ)) = + (Finset.univ.filter fun i : Fin n => w i = SignType.pos).card := by + simpa [diagForm, posSet, signSet] using (posIndex_diag_signType (n := n) w) + +private theorem posDim_diagForm (w : Fin n → SignType) : + QuadraticForm.posDim (E := Fin n → ℝ) (diagForm (n := n) w) = (posSet (n := n) w).card := by + simp [QuadraticForm.posDim, posIndex_diag_signType (n := n) w] + +theorem posDim_weightedSumSquares_signType (w : Fin n → SignType) : + QuadraticForm.posDim (E := Fin n → ℝ) + ((QuadraticMap.weightedSumSquares ℝ fun i : Fin n => (w i : ℝ)) : + QuadraticForm ℝ (Fin n → ℝ)) = + (Finset.univ.filter fun i : Fin n => w i = SignType.pos).card := by + simpa [diagForm, posSet, signSet] using (posDim_diagForm (n := n) w) + +private theorem negDim_diagForm (w : Fin n → SignType) : + QuadraticForm.negDim (E := Fin n → ℝ) (diagForm (n := n) w) = (negSet (n := n) w).card := by + set Q : QuadraticForm ℝ (Fin n → ℝ) := diagForm (n := n) w + have hneg : -Q = diagForm (n := n) (fun i => -w i) := by + ext v + simp [Q, diagForm, QuadraticMap.weightedSumSquares_apply] + have hpos : posIndex (V := Fin n → ℝ) (-Q) = (posSet (n := n) (fun i => -w i)).card := by + simpa [hneg] using (posIndex_diag_signType (n := n) (w := fun i => -w i)) + simp [Q, QuadraticForm.negDim, hpos, posSet_neg (n := n) w, negSet, signSet] + +theorem negDim_weightedSumSquares_signType (w : Fin n → SignType) : + QuadraticForm.negDim (E := Fin n → ℝ) + ((QuadraticMap.weightedSumSquares ℝ fun i : Fin n => (w i : ℝ)) : + QuadraticForm ℝ (Fin n → ℝ)) = + (Finset.univ.filter fun i : Fin n => w i = SignType.neg).card := by + simpa [diagForm, negSet, signSet] using (negDim_diagForm (n := n) w) + +lemma card_posSet_add_card_negSet_add_card_zeroSet (w : Fin n → SignType) : + (posSet (n := n) w).card + (negSet (n := n) w).card + (zeroSet (n := n) w).card = + Fintype.card (Fin n) := by + let A : Finset (Fin n) := posSet (n := n) w + let B : Finset (Fin n) := negSet (n := n) w + let C : Finset (Fin n) := zeroSet (n := n) w + have hAB : Disjoint A B := by + refine Finset.disjoint_left.2 ?_ + intro i hiA hiB + have hiPos : w i = SignType.pos := (mem_posSet (n := n) (w := w)).1 hiA + have hiNeg : w i = SignType.neg := (mem_negSet (n := n) (w := w)).1 hiB + have : (SignType.pos : SignType) = SignType.neg := hiPos.symm.trans hiNeg + cases this + have hABC : Disjoint (A ∪ B) C := by + refine Finset.disjoint_left.2 ?_ + intro i hiAB hiC + have hiC' : w i = 0 := (mem_zeroSet (n := n) (w := w)).1 hiC + rcases Finset.mem_union.1 hiAB with hiA | hiB + · have hiPos : w i = SignType.pos := (mem_posSet (n := n) (w := w)).1 hiA + have : (SignType.pos : SignType) = 0 := hiPos.symm.trans hiC' + cases this + · have hiNeg : w i = SignType.neg := (mem_negSet (n := n) (w := w)).1 hiB + have : (SignType.neg : SignType) = 0 := hiNeg.symm.trans hiC' + cases this + have hunion : (A ∪ B) ∪ C = Finset.univ := by + ext i + cases hi : w i <;> simp [A, B, C, signSet, hi] + have hcardAB : (A ∪ B).card = A.card + B.card := + Finset.card_union_of_disjoint hAB + have hcardABC : ((A ∪ B) ∪ C).card = (A ∪ B).card + C.card := + Finset.card_union_of_disjoint hABC + have hcard : ((A ∪ B) ∪ C).card = A.card + B.card + C.card := by + calc + ((A ∪ B) ∪ C).card = (A ∪ B).card + C.card := hcardABC + _ = (A.card + B.card) + C.card := by simp [hcardAB, Nat.add_assoc] + _ = A.card + B.card + C.card := by simp [Nat.add_assoc] + have huniv : ((A ∪ B) ∪ C).card = Fintype.card (Fin n) := by + have : ((A ∪ B) ∪ C).card = (Finset.univ : Finset (Fin n)).card := + congrArg Finset.card hunion + simpa using this + have : A.card + B.card + C.card = Fintype.card (Fin n) := by + calc + A.card + B.card + C.card = ((A ∪ B) ∪ C).card := by simpa [hcard] using hcard.symm + _ = Fintype.card (Fin n) := huniv + simpa [A, B, C, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using this + +private theorem zeroDim_diagForm (w : Fin n → SignType) : + QuadraticForm.zeroDim (E := Fin n → ℝ) (diagForm (n := n) w) = (zeroSet (n := n) w).card := by + have hfin : finrank ℝ (Fin n → ℝ) = Fintype.card (Fin n) := by simp + have hpos := posDim_diagForm (n := n) w + have hneg := negDim_diagForm (n := n) w + have hsum := card_posSet_add_card_negSet_add_card_zeroSet (n := n) w + let A : ℕ := (posSet (n := n) w).card + let B : ℕ := (negSet (n := n) w).card + let C : ℕ := (zeroSet (n := n) w).card + have hsum' : A + B + C = Fintype.card (Fin n) := by simpa [A, B, C] using hsum + have hz0 : Fintype.card (Fin n) - A - B = C := by + have hn : Fintype.card (Fin n) = A + (B + C) := by + simpa [Nat.add_assoc] using hsum'.symm + have h1 : Fintype.card (Fin n) - A = B + C := by + simp [hn] + calc + Fintype.card (Fin n) - A - B = (Fintype.card (Fin n) - A) - B := rfl + _ = (B + C) - B := by + simpa using congrArg (fun t => t - B) h1 + _ = C := by simp + set Q : QuadraticForm ℝ (Fin n → ℝ) := diagForm (n := n) w + have hposI : posIndex (V := Fin n → ℝ) Q = A := by + simpa [Q, A] using (posIndex_diag_signType (n := n) w) + have hnegI : posIndex (V := Fin n → ℝ) (-Q) = B := by + simpa [Q, B, QuadraticForm.negDim] using hneg + have : QuadraticForm.zeroDim (E := Fin n → ℝ) Q = C := by + dsimp [QuadraticForm.zeroDim, QuadraticForm.posDim, QuadraticForm.negDim] + rw [hfin, hposI, hnegI] + simpa using hz0 + simpa [Q, C] using this + +theorem zeroDim_weightedSumSquares_signType (w : Fin n → SignType) : + QuadraticForm.zeroDim (E := Fin n → ℝ) + ((QuadraticMap.weightedSumSquares ℝ fun i : Fin n => (w i : ℝ)) : + QuadraticForm ℝ (Fin n → ℝ)) = + (Finset.univ.filter fun i : Fin n => w i = 0).card := by + simpa [diagForm, zeroSet, signSet] using (zeroDim_diagForm (n := n) w) + +end + +end Diagonal + +end QuadraticForm + +#lint diff --git a/PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean b/PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean index 3caa55842..8b543fcf1 100644 --- a/PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean +++ b/PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean @@ -4,214 +4,128 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Matteo Cipollina -/ import PhysLean.Mathematics.Geometry.Metric.PseudoRiemannian.Defs -import Mathlib.Algebra.Lie.OfAssociative -import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic +import Mathlib.Geometry.Manifold.VectorBundle.Riemannian +import Mathlib.Geometry.Manifold.VectorBundle.Tangent /-! -# 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`). + +## 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 +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] -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)] +/-- A `C^n` Riemannian metric on `M`, packaged using Mathlib's modern bundle API. -/ +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) -/-- Coercion from RiemannianMetric to its underlying PseudoRiemannianMetric. -/ -instance : Coe (RiemannianMetric I n M) (PseudoRiemannianMetric E H M (n) I) where - coe g := g.toPseudoRiemannianMetric +namespace 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 +variable (g : RiemannianMetric (I := I) (n := n) M) +variable [∀ x : M, FiniteDimensional ℝ (TangentSpace I x)] + +/-- Forget the positivity to get a pseudo-Riemannian metric. The index is (locally constantly) `0`. +This is the bridge that makes pseudo-Riemannian API (musical isomorphisms, etc.) usable for a +Riemannian metric. -/ +def toPseudoRiemannianMetric (g : RiemannianMetric (I := I) (n := n) M) : + PseudoRiemannianMetric E H M n I where + val := g.inner + symm := g.symm + nondegenerate := by + intro x v hv + by_cases h : v = 0 + · simp [h] + · have hp : 0 < g.inner x v v := g.pos x v h + have h0 : g.inner x v v = 0 := hv v + exact (ne_of_gt hp h0).elim + contMDiff := g.contMDiff + negDim_isLocallyConstant := by + -- On a Riemannian metric, the associated quadratic form is positive definite, so `negDim = 0`. + refine IsLocallyConstant.of_constant _ (fun x y => ?_) + have hx : + (PseudoRiemannianMetric.valToQuadraticForm g.inner g.symm x).negDim = 0 := by + apply QuadraticForm.negDim_posDef + intro v hv + simpa [PseudoRiemannianMetric.valToQuadraticForm] using g.pos x v hv + have hy : + (PseudoRiemannianMetric.valToQuadraticForm g.inner g.symm y).negDim = 0 := by + apply QuadraticForm.negDim_posDef + intro v hv + simpa [PseudoRiemannianMetric.valToQuadraticForm] using g.pos y v hv + have hx' : + (-PseudoRiemannianMetric.valToQuadraticForm g.inner g.symm x).posIndex = 0 := by + simpa [QuadraticForm.negDim] using hx + have hy' : + (-PseudoRiemannianMetric.valToQuadraticForm g.inner g.symm y).posIndex = 0 := by + simpa [QuadraticForm.negDim] using hy + simp [hx', hy'] -/-- 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). -/ -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`. -/ -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`. -/ -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`. -/ -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 +lemma toPseudoRiemannianMetric_posIndex_neg_toQuadraticForm + (g : RiemannianMetric (I := I) (n := n) M) (x : M) : + (-(toPseudoRiemannianMetric (I := I) (n := n) (M := M) g).toQuadraticForm x).posIndex = 0 := by + have hx : (PseudoRiemannianMetric.valToQuadraticForm g.inner g.symm x).negDim = 0 := by + apply QuadraticForm.negDim_posDef + intro v hv + simpa [PseudoRiemannianMetric.valToQuadraticForm] using g.pos x v hv + simpa [PseudoRiemannianMetric.toQuadraticForm, toPseudoRiemannianMetric, QuadraticForm.negDim] + using hx + +lemma toPseudoRiemannianMetric_index (g : RiemannianMetric (I := I) (n := n) M) (x : M) : + (toPseudoRiemannianMetric (I := I) (n := n) (M := M) g).index x = 0 := by + have hx : (PseudoRiemannianMetric.valToQuadraticForm g.inner g.symm x).negDim = 0 := by + apply QuadraticForm.negDim_posDef + intro v hv + simpa [PseudoRiemannianMetric.valToQuadraticForm] using g.pos x v hv + simpa [PseudoRiemannianMetric.index, PseudoRiemannianMetric.toQuadraticForm, + toPseudoRiemannianMetric] using hx + +instance : + Coe (RiemannianMetric (I := I) (n := n) M) + (PseudoRiemannianMetric E H M n I) := + ⟨fun g => toPseudoRiemannianMetric (I := I) (n := n) (M := M) g⟩ 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 := I) (n := n) M)) : + Nonempty (PseudoRiemannianMetric E H M n I) := by + rcases h with ⟨g⟩ + exact ⟨RiemannianMetric.toPseudoRiemannianMetric (I := I) (n := n) (M := M) g⟩ + end -end RiemannianMetric + +end + end PseudoRiemannianMetric