Pseudo-Riemannian Metrics on Smooth Manifolds #
This file formalizes pseudo-Riemannian metrics on smooth manifolds and establishes their basic properties.
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 #
PseudoRiemannianMetric E H M n I: A structure representing aC^npseudo-Riemannian metric on a manifoldMmodelled on(E, H)with model with cornersI. It consists of a family of non-degenerate, symmetric, continuous bilinear formsgₓon each tangent spaceTₓM, varyingC^n-smoothly withxand having a locally constant negative dimension (negDim). The model spaceEmust be finite-dimensional, and the manifoldMmust beC^{n+1}smooth.PseudoRiemannianMetric.flatEquiv g x: The "musical isomorphism" from the tangent space atxto its dual space, representing the canonical isomorphism induced by the metric.PseudoRiemannianMetric.sharpEquiv g x: The inverse of the flat isomorphism, mapping from the dual space back to the tangent space.PseudoRiemannianMetric.toQuadraticForm g x: The quadratic formv ↦ gₓ(v, v)associated with the metric at pointx.
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[ℝ] ℝ.
Reference #
- 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
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."
Equations
- q.negDim = {i : Fin (Module.finrank ℝ E) | Classical.choose ⋯ i = SignType.neg}.card
Instances For
For a standard basis vector in a weighted sum of squares, only one term in the sum is nonzero.
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).
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.
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.
Pseudo-Riemannian Metric #
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.
The metric tensor at each point
x : M, represented as a continuous linear mapTₓM →L[ℝ] (TₓM →L[ℝ] ℝ). Applying it twice,(val x v) w, yieldsgₓ(v, w).The metric is symmetric:
gₓ(v, w) = gₓ(w, v).- nondegenerate (x : M) (v : TangentSpace I x) : (∀ (w : TangentSpace I x), ((self.val x) v) w = 0) → v = 0
The metric is non-degenerate: if
gₓ(v, w) = 0for allw, thenv = 0. - smooth_in_charts' (x₀ : M) (v w : E) : let e := extChartAt I x₀; ContDiffWithinAt ℝ n (fun (y : E) => ((self.val (↑e.symm y)) ((mfderiv I I (↑e.symm) y) v)) ((mfderiv I I (↑e.symm) y) w)) e.target (↑e x₀)
The metric varies smoothly: Expressed in local coordinates via the chart
e := extChartAt I x₀, the functiony ↦ g_{e.symm y}(mfderiv I I e.symm y v, mfderiv I I e.symm y w)isC^nsmooth on the chart's targete.targetfor any constant vectorsv, win the model spaceE. - negDim_isLocallyConstant : IsLocallyConstant fun (x : M) => let_fun this := ⋯; (pseudoRiemannianMetricValToQuadraticForm✝ self.val ⋯ x).negDim
The negative dimension (
QuadraticForm.negDim) of the metric's quadratic form is locally constant. On a connected manifold, this implies it is constant globally.
Instances For
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)
Equations
- g.toBilinForm x = { toFun := fun (v : TangentSpace I x) => { toFun := fun (w : TangentSpace I x) => ((g.val x) v) w, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Convert a pseudo-Riemannian metric at a point x to a quadratic form v ↦ gₓ(v, v).
Equations
Instances For
Coercion from PseudoRiemannianMetric to its function representation.
Equations
- PseudoRiemannianMetric.coeFunInst = { coe := fun (g : PseudoRiemannianMetric E H M n I) => g.val }
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).
Instances For
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.
Equations
Instances For
The musical isomorphism as a continuous linear map.
Equations
Instances For
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).
Equations
- g.flatEquiv x = (LinearEquiv.ofBijective ↑(g.flatL x) ⋯).toContinuousLinearEquiv
Instances For
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).
Equations
- g.sharpEquiv x = (g.flatEquiv x).symm
Instances For
The index raising map sharp as a continuous linear map.
Equations
- g.sharpL x = ↑(g.sharpEquiv x)
Instances For
The index raising map sharp as a linear map.
Equations
- g.sharp x = ↑(g.sharpEquiv x).toLinearEquiv
Instances For
The metric evaluated at v and sharp ω.
Cotangent #
The value of the induced metric on the cotangent space at point x.
Equations
- g.cotangentMetricVal x ω₁ ω₂ = ((g.val x) ((g.sharpL x) ω₁)) ((g.sharpL x) ω₂)
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- g.cotangentToQuadraticForm x = { toFun := fun (ω : TangentSpace I x →L[ℝ] ℝ) => g.cotangentMetricVal x ω ω, toFun_smul := ⋯, exists_companion' := ⋯ }
Instances For
The cotangent metric is non-degenerate: if cotangentMetricVal g x ω v = 0 for all v,
then ω = 0.