Physicslib4.Geometry.PseudoRiemannian.Basic

Pseudo-Riemannian metrics

A pseudo-Riemannian metric on a manifold M modelled on (E, H) with model I is a smooth family of symmetric, nondegenerate continuous bilinear forms on the tangent spaces. Unlike Mathlib's Bundle.ContMDiffRiemannianMetric, no positivity is required, so Lorentzian metrics are included. The smoothness condition has the same bundle-section shape as Bundle.ContMDiffRiemannianMetric.contMDiff.

Main definitions

• Physicslib4.Geometry.PseudoRiemannianMetric: the structure.
• Physicslib4.Spacetime.toPseudoRiemannianMetric: the metric of a spacetime.

Main results

• Physicslib4.Geometry.PseudoRiemannianMetric.bijective_val: at each point, v ↦ g_x(v, ·) is a linear isomorphism T_xM → T_x*M (the musical isomorphism), packaged as flatEquiv.
• Physicslib4.Geometry.PseudoRiemannianMetric.contMDiff_flatEquiv_symm: x ↦ ♭_x⁻¹ is a C^∞ section of Hom(T*M, TM).

Blueprint reference: def:pseudo-riemannian-metric, lmm:musical-isomorphism, lmm:musical-inverse-smooth.

structure Physicslib4.Geometry.PseudoRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] : Type (max u_1 u_3)

A pseudo-Riemannian metric on a manifold M: a smooth field of symmetric, non-degenerate bilinear forms g_x on the tangent spaces TₓM.

No signature is imposed, so Riemannian and Lorentzian metrics are both examples; the metric of a spacetime is one (Spacetime.toPseudoRiemannianMetric). Non-degeneracy makes v ↦ g_x(v, ·) an isomorphism of TₓM onto its dual (bijective_val, flatEquiv), the index lowering of physics notation. The Levi-Civita connection and geodesics are built on this structure (PseudoRiemannianMetric.leviCivita), and they do not use the signature.

Implementation note: Mathlib's Bundle.ContMDiffRiemannianMetric requires positivity, so it is not reused; the field contMDiff has the same bundle-section shape as its smoothness field.

Blueprint: def:pseudo-riemannian-metric

• val (x : M) : TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ

  The metric g: at each point x, a continuous bilinear form g_x on TₓM.

• symm (x : M) (v w : TangentSpace I x) : ((self.val x) v) w = ((self.val x) w) v

  g is symmetric: g_x(v, w) = g_x(w, v).

• nondegenerate (x : M) (v : TangentSpace I x) : (∀ (w : TangentSpace I x), ((self.val x) v) w = 0) → v = 0

  g is non-degenerate: if g_x(v, w) = 0 for every w, then v = 0.

• contMDiff : ContMDiff I (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) ↑⊤ fun (x : M) => ⟨x, self.val x⟩

  g is smooth: a C^∞ section of the bundle of continuous bilinear forms on the tangent bundle.

theorem Physicslib4.Geometry.PseudoRiemannianMetric.bijective_val {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) (x : M) : Function.Bijective ⇑(g.val x)

The musical isomorphism. At each point x, the map v ↦ g_x(v, ·) from T_xM to its dual is bijective: injective by nondegeneracy and hence bijective since T_xM is finite-dimensional.

Blueprint reference: lmm:musical-isomorphism.

noncomputable def Physicslib4.Geometry.PseudoRiemannianMetric.flatEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) (x : M) : TangentSpace I x ≃L[ℝ] TangentSpace I x →L[ℝ] ℝ

The musical isomorphism ♭_x : T_xM ≃ T_x*M, v ↦ g_x(v, ·), as a continuous linear equivalence (bijective_val; continuity of the inverse is automatic in finite dimension).

Blueprint reference: lmm:musical-isomorphism.

Equations

• g.flatEquiv x = (LinearEquiv.ofBijective ↑(g.val x) ⋯).toContinuousLinearEquiv

theorem Physicslib4.Geometry.PseudoRiemannianMetric.flatEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) (x : M) (v : TangentSpace I x) : (g.flatEquiv x) v = (g.val x) v

theorem Physicslib4.Geometry.PseudoRiemannianMetric.contMDiff_flatEquiv_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) : ContMDiff I (I.prod (modelWithCornersSelf ℝ ((E →L[ℝ] ℝ) →L[ℝ] E))) ↑⊤ fun (x : M) => ⟨x, ↑(g.flatEquiv x).symm⟩

Smoothness of the inverse musical isomorphism. The map x ↦ ♭_x⁻¹ is a C^∞ section of the bundle Hom(T*M, TM), whose fibre at x is T_x*M →L[ℝ] T_xM, stated in the same bundle-section idiom as the smoothness of g itself.

Blueprint reference: lmm:musical-inverse-smooth.

def Physicslib4.Spacetime.toPseudoRiemannianMetric (M : Spacetime) : Geometry.PseudoRiemannianMetric M.model M.Carrier

The metric of a spacetime, as a pseudo-Riemannian metric on its manifold.

The fields are those of the spacetime (Spacetime.val, Spacetime.symm, Spacetime.nondegenerate, Spacetime.contMDiff); the Lorentzian condition is forgotten. This gives a spacetime the general API, in particular its Levi-Civita connection M.toPseudoRiemannianMetric.leviCivita, which Spacetime.IsGeodesic uses.

Blueprint: def:pseudo-riemannian-metric

Equations

• M.toPseudoRiemannianMetric = { val := M.val, symm := ⋯, nondegenerate := ⋯, contMDiff := ⋯ }