Imports
/-
Copyright (c) 2025 Matteo Cipollina. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina
-/
module
public import Mathlib.Analysis.InnerProductSpace.Basic
public import Mathlib.Geometry.Manifold.MFDeriv.Defs
public import Mathlib.LinearAlgebra.BilinearForm.Properties
public import Mathlib.LinearAlgebra.QuadraticForm.Real
public import Mathlib.Topology.LocallyConstant.BasicPseudo-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 a C^n pseudo-Riemannian metric
on a manifold M modelled on (E, H) with model with corners I. It consists of a family
of non-degenerate, symmetric, continuous bilinear forms gₓ on each tangent space TₓM,
varying C^n-smoothly with x and having a locally constant negative dimension (negDim).
The model space E must be finite-dimensional, and the manifold M must be C^{n+1} smooth.
PseudoRiemannianMetric.flatEquiv g x: The "musical isomorphism" from the tangent space at x
to 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 form v ↦ gₓ(v, v) associated
with the metric at point x.
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
@[expose] public sectionNegative Index
For a standard basis vector in a weighted sum of squares, only one term in the sum is nonzero.
E:Type u_2inst✝¹:AddCommGroup Einst✝:Module ℝ Eweights:Fin (finrank ℝ E) → ℝi:Fin (finrank ℝ E)v:Fin (finrank ℝ E) → ℝhv:∀ (j : Fin (finrank ℝ E)), v j = if j = i then 1 else 0⊢ weights i • (v i * v i) = weights iE:Type u_2inst✝¹:AddCommGroup Einst✝:Module ℝ Eweights:Fin (finrank ℝ E) → ℝi:Fin (finrank ℝ E)v:Fin (finrank ℝ E) → ℝhv:∀ (j : Fin (finrank ℝ E)), v j = if j = i then 1 else 0⊢ ∀ b ∈ Finset.univ, b ≠ i → weights b • (v b * v b) = 0
E:Type u_2inst✝¹:AddCommGroup Einst✝:Module ℝ Eweights:Fin (finrank ℝ E) → ℝi:Fin (finrank ℝ E)v:Fin (finrank ℝ E) → ℝhv:∀ (j : Fin (finrank ℝ E)), v j = if j = i then 1 else 0⊢ weights i • (v i * v i) = weights i All goals completed! 🐙
E:Type u_2inst✝¹:AddCommGroup Einst✝:Module ℝ Eweights:Fin (finrank ℝ E) → ℝi:Fin (finrank ℝ E)v:Fin (finrank ℝ E) → ℝhv:∀ (j : Fin (finrank ℝ E)), v j = if j = i then 1 else 0⊢ ∀ b ∈ Finset.univ, b ≠ i → weights b • (v b * v b) = 0 E:Type u_2inst✝¹:AddCommGroup Einst✝:Module ℝ Eweights:Fin (finrank ℝ E) → ℝi:Fin (finrank ℝ E)v:Fin (finrank ℝ E) → ℝhv:∀ (j : Fin (finrank ℝ E)), v j = if j = i then 1 else 0j:Fin (finrank ℝ E)a✝:j ∈ Finset.univhj:j ≠ i⊢ weights j • (v j * v j) = 0
All goals completed! 🐙
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).
E:Type u_2inst✝¹:AddCommGroup Einst✝:Module ℝ Eq:QuadraticForm ℝ Ew:Fin (finrank ℝ E) → SignTypeh_equiv:QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))i:Fin (finrank ℝ E)hi:w i = SignType.negf:QuadraticMap.IsometryEquiv q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i)) := Classical.choice h_equivv_std:Fin (finrank ℝ E) → ℝ := fun j => if j = i then 1 else 0hw:(QuadraticMap.weightedSumSquares ℝ fun j => ↑(w j)) v_std = ↑(w i)⊢ -1 < 0
All goals completed! 🐙
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 := E:Type u_2inst✝¹:AddCommGroup Einst✝:Module ℝ Eq:QuadraticForm ℝ Ehq:QuadraticMap.PosDef qw:Fin (finrank ℝ E) → SignTypeh_equiv:QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))⊢ ∀ (i : Fin (finrank ℝ E)), w i ≠ SignType.neg
E:Type u_2inst✝¹:AddCommGroup Einst✝:Module ℝ Eq:QuadraticForm ℝ Ehq:QuadraticMap.PosDef qw:Fin (finrank ℝ E) → SignTypeh_equiv:QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))i:Fin (finrank ℝ E)hi:w i = SignType.neg⊢ False
E:Type u_2inst✝¹:AddCommGroup Einst✝:Module ℝ Eq:QuadraticForm ℝ Ehq:QuadraticMap.PosDef qw:Fin (finrank ℝ E) → SignTypeh_equiv:QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))i:Fin (finrank ℝ E)hi:w i = SignType.negv:Ehv:v ≠ 0hq_neg:q v < 0⊢ False
All goals completed! 🐙
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 := E:Type u_2inst✝²:AddCommGroup Einst✝¹:Module ℝ Einst✝:FiniteDimensional ℝ Eq:QuadraticForm ℝ Ehq:QuadraticMap.PosDef q⊢ q.negDim = 0
E:Type u_2inst✝²:AddCommGroup Einst✝¹:Module ℝ Einst✝:FiniteDimensional ℝ Eq:QuadraticForm ℝ Ehq:QuadraticMap.PosDef qthis:Invertible 2⊢ q.negDim = 0
E:Type u_2inst✝²:AddCommGroup Einst✝¹:Module ℝ Einst✝:FiniteDimensional ℝ Eq:QuadraticForm ℝ Ehq:QuadraticMap.PosDef qthis:Invertible 2⊢ (let P := fun w => QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i));
have h_exists := ⋯;
have w := Classical.choose h_exists;
#{i | w i = SignType.neg}) =
0
E:Type u_2inst✝²:AddCommGroup Einst✝¹:Module ℝ Einst✝:FiniteDimensional ℝ Eq:QuadraticForm ℝ Ehq:QuadraticMap.PosDef qthis:Invertible 2h_exists:∃ w, QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))⊢ (let P := fun w => QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i));
have h_exists := ⋯;
have w := Classical.choose h_exists;
#{i | w i = SignType.neg}) =
0
E:Type u_2inst✝²:AddCommGroup Einst✝¹:Module ℝ Einst✝:FiniteDimensional ℝ Eq:QuadraticForm ℝ Ehq:QuadraticMap.PosDef qthis:Invertible 2h_exists:∃ w, QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))w:Fin (finrank ℝ E) → SignType := Classical.choose h_exists⊢ (let P := fun w => QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i));
have h_exists := ⋯;
have w := Classical.choose h_exists;
#{i | w i = SignType.neg}) =
0
E:Type u_2inst✝²:AddCommGroup Einst✝¹:Module ℝ Einst✝:FiniteDimensional ℝ Eq:QuadraticForm ℝ Ehq:QuadraticMap.PosDef qthis:Invertible 2h_exists:∃ w, QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i))w:Fin (finrank ℝ E) → SignType := Classical.choose h_existsh_no_neg:∀ (i : Fin (finrank ℝ E)), w i ≠ SignType.neg⊢ (let P := fun w => QuadraticMap.Equivalent q (QuadraticMap.weightedSumSquares ℝ fun i => ↑(w i));
have h_exists := ⋯;
have w := Classical.choose h_exists;
#{i | w i = SignType.neg}) =
0
All goals completed! 🐙Pseudo-Riemannian Metric
Constructs a QuadraticForm on the tangent space TₓM at a point x from the
value of a pseudo-Riemannian metric at that point.
(O'Neill, p. 47, "The function q: V → R given by q(v) = b(v,v) is the associated quadratic
form of b.")
The pseudo-Riemannian metric is given by val, a family of continuous bilinear forms
gₓ: TₓM × TₓM → ℝ for each x : M.
The quadratic form Qₓ at x is defined as Qₓ(v) = gₓ(v,v).
The associated symmetric bilinear form required by QuadraticForm.exists_companion'
is Bₓ(v,w) = gₓ(v,w) + gₓ(w,v). Given the symmetry symm, this is 2 * gₓ(v,w).
def pseudoRiemannianMetricValToQuadraticForm
{E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E]
{H : Type w} [TopologicalSpace H]
{M : Type w} [TopologicalSpace M] [ChartedSpace H M]
{I : ModelWithCorners ℝ E H}
(val : ∀ (x : M), TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ))
(symm : ∀ (x : M) (v w : TangentSpace I x), (val x v) w = (val x w) v)
(x : M) : QuadraticForm ℝ (TangentSpace I x) where
toFun v := val x v v
toFun_smul a v := E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Ma:ℝv:TangentSpace I x⊢ ((val x) (a • v)) (a • v) = (a * a) • ((val x) v) v
All goals completed! 🐙
exists_companion' :=
⟨LinearMap.mk₂ ℝ (fun v y => val x v y + val x y v)
(fun v₁ v₂ y => E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Mv₁:TangentSpace I xv₂:TangentSpace I xy:TangentSpace I x⊢ ((val x) (v₁ + v₂)) y + ((val x) y) (v₁ + v₂) = ((val x) v₁) y + ((val x) y) v₁ + (((val x) v₂) y + ((val x) y) v₂) E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Mv₁:TangentSpace I xv₂:TangentSpace I xy:TangentSpace I x⊢ ((val x) v₁) y + ((val x) v₂) y + (((val x) y) v₁ + ((val x) y) v₂) =
((val x) v₁) y + ((val x) y) v₁ + (((val x) v₂) y + ((val x) y) v₂); All goals completed! 🐙)
(fun a v y => E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Ma:ℝv:TangentSpace I xy:TangentSpace I x⊢ ((val x) (a • v)) y + ((val x) y) (a • v) = a • (((val x) v) y + ((val x) y) v) E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Ma:ℝv:TangentSpace I xy:TangentSpace I x⊢ a • ((val x) v) y + a • ((val x) y) v = a • (((val x) v) y + ((val x) y) v); All goals completed! 🐙)
(fun v y₁ y₂ => E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Mv:TangentSpace I xy₁:TangentSpace I xy₂:TangentSpace I x⊢ ((val x) v) (y₁ + y₂) + ((val x) (y₁ + y₂)) v = ((val x) v) y₁ + ((val x) y₁) v + (((val x) v) y₂ + ((val x) y₂) v) E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Mv:TangentSpace I xy₁:TangentSpace I xy₂:TangentSpace I x⊢ ((val x) v) y₁ + ((val x) v) y₂ + (((val x) y₁) v + ((val x) y₂) v) =
((val x) v) y₁ + ((val x) y₁) v + (((val x) v) y₂ + ((val x) y₂) v); All goals completed! 🐙)
(fun a v y => E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Ma:ℝv:TangentSpace I xy:TangentSpace I x⊢ ((val x) v) (a • y) + ((val x) (a • y)) v = a • (((val x) v) y + ((val x) y) v) E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Ma:ℝv:TangentSpace I xy:TangentSpace I x⊢ a • ((val x) v) y + a • ((val x) y) v = a • (((val x) v) y + ((val x) y) v); All goals completed! 🐙),
E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:M⊢ ∀ (x_1 y : TangentSpace I x),
((val x) (x_1 + y)) (x_1 + y) =
((val x) x_1) x_1 + ((val x) y) y + ((LinearMap.mk₂ ℝ (fun v y => ((val x) v) y + ((val x) y) v) ⋯ ⋯ ⋯ ⋯) x_1) y
E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Mv:TangentSpace I xy:TangentSpace I x⊢ ((val x) (v + y)) (v + y) =
((val x) v) v + ((val x) y) y + ((LinearMap.mk₂ ℝ (fun v y => ((val x) v) y + ((val x) y) v) ⋯ ⋯ ⋯ ⋯) v) y
E:Type vinst✝⁴:NormedAddCommGroup Einst✝³:NormedSpace ℝ EH:Type winst✝²:TopologicalSpace HM:Type winst✝¹:TopologicalSpace Minst✝:ChartedSpace H MI:ModelWithCorners ℝ E Hval:(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) vx:Mv:TangentSpace I xy:TangentSpace I x⊢ ((val x) v) v + ((val x) v) y + (((val x) v) y + ((val x) y) y) =
((val x) v) v + ((val x) y) y + (((val x) v) y + ((val x) v) y)
All goals completed! 🐙⟩
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 map
TₓM →L[ℝ] (TₓM →L[ℝ] ℝ). Applying it twice, (val x v) w, yields gₓ(v, w).
The metric is symmetric: gₓ(v, w) = gₓ(w, v).
The metric is non-degenerate: if gₓ(v, w) = 0 for all w, then 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.
The negative dimension (QuadraticForm.negDim) of the metric's quadratic form is
locally constant. On a connected manifold, this implies it is constant globally.
@[ext]
structure PseudoRiemannianMetric
(E : Type v) (H : Type w) (M : Type w) (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 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 nondegenerate : ∀ (x : M) (v : TangentSpace I x), (∀ w : TangentSpace I x,
(val x v) w = 0) → v = 0 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₀) negDim_isLocallyConstant :
IsLocallyConstant (fun x : M =>
have : FiniteDimensional ℝ (TangentSpace I x) := inferInstance
(pseudoRiemannianMetricValToQuadraticForm val symm x).negDim)
Given a pseudo-Riemannian metric g on manifold M and a point x : M,
this function constructs a bilinear form on the tangent space at x.
For tangent vectors u v : T_x M, the bilinear form is given by:
g_x(u, v) = g(x)(u, v)
def toBilinForm (g : PseudoRiemannianMetric E H M n I) (x : M) :
LinearMap.BilinForm ℝ (TangentSpace I x) where
toFun := λ v => { toFun := λ w => g.val x v w,
map_add' := λ w₁ w₂ => E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Mv:TangentSpace I xw₁:TangentSpace I xw₂:TangentSpace I x⊢ ((g.val x) v) (w₁ + w₂) = ((g.val x) v) w₁ + ((g.val x) v) w₂
All goals completed! 🐙,
map_smul' := λ c w => E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Mv:TangentSpace I xc:ℝw:TangentSpace I x⊢ ((g.val x) v) (c • w) = (RingHom.id ℝ) c • ((g.val x) v) w
All goals completed! 🐙 }
map_add' := λ v₁ v₂ => E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Mv₁:TangentSpace I xv₂:TangentSpace I x⊢ { toFun := fun w => ((g.val x) (v₁ + v₂)) w, map_add' := ⋯, map_smul' := ⋯ } =
{ toFun := fun w => ((g.val x) v₁) w, map_add' := ⋯, map_smul' := ⋯ } +
{ toFun := fun w => ((g.val x) v₂) w, map_add' := ⋯, map_smul' := ⋯ }
E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Mv₁:TangentSpace I xv₂:TangentSpace I xw:TangentSpace I x⊢ { toFun := fun w => ((g.val x) (v₁ + v₂)) w, map_add' := ⋯, map_smul' := ⋯ } w =
({ toFun := fun w => ((g.val x) v₁) w, map_add' := ⋯, map_smul' := ⋯ } +
{ toFun := fun w => ((g.val x) v₂) w, map_add' := ⋯, map_smul' := ⋯ })
w
All goals completed! 🐙
map_smul' := λ c v => E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Mc:ℝv:TangentSpace I x⊢ { toFun := fun w => ((g.val x) (c • v)) w, map_add' := ⋯, map_smul' := ⋯ } =
(RingHom.id ℝ) c • { toFun := fun w => ((g.val x) v) w, map_add' := ⋯, map_smul' := ⋯ }
E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Mc:ℝv:TangentSpace I xw:TangentSpace I x⊢ { toFun := fun w => ((g.val x) (c • v)) w, map_add' := ⋯, map_smul' := ⋯ } w =
((RingHom.id ℝ) c • { toFun := fun w => ((g.val x) v) w, map_add' := ⋯, map_smul' := ⋯ }) w
All goals completed! 🐙
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) :=
pseudoRiemannianMetricValToQuadraticForm g.val g.symm xCoercion 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@[simp]
lemma toBilinForm_isSymm (g : PseudoRiemannianMetric E H M n I) (x : M) :
(toBilinForm g x).IsSymm := ⟨g.symm x⟩@[simp]
lemma toBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) :
(toBilinForm g x).Nondegenerate := E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:M⊢ (g.toBilinForm x).Nondegenerate
E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:Mv:TangentSpace I xhv:∀ (x_1 : TangentSpace I x), ((g.toBilinForm x) x_1) v = 0⊢ v = 0
All goals completed! 🐙
The inner product (or scalar product) on the tangent space at point x
induced by the pseudo-Riemannian metric g. This is gₓ(v, w).
def inner (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) : ℝ :=
g.val x v w@[simp]
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 := rflFlat
The "musical" isomorphism (index lowering) v ↦ gₓ(v, -).
The non-degeneracy of gₓ (O'Neill, Def 17 (3), p. 46) means its matrix representation
is invertible (O'Neill, Lemma 19, p. 47), and that this map is an isomorphism from TₓM
to its dual.
def flat (g : PseudoRiemannianMetric E H M n I) (x : M) :
TangentSpace I x →ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
{ toFun := λ v => g.val x v,
map_add' := λ v w => E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Mv:TangentSpace I xw:TangentSpace I x⊢ (g.val x) (v + w) = (g.val x) v + (g.val x) w All goals completed! 🐙,
map_smul' := λ a v => E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Ma:ℝv:TangentSpace I x⊢ (g.val x) (a • v) = (RingHom.id ℝ) a • (g.val x) v E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Ma:ℝv:TangentSpace I x⊢ a • (g.val x) v = (RingHom.id ℝ) a • (g.val x) v; All goals completed! 🐙 }@[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 := E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:Mv:TangentSpace I xw:TangentSpace I x⊢ ((g.flat x) v) w = ((g.val x) v) w All goals completed! 🐙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 => E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Mv:TangentSpace I xw:TangentSpace I x⊢ (g.val x) (v + w) = (g.val x) v + (g.val x) w All goals completed! 🐙
map_smul' := λ a v => E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Ma:ℝv:TangentSpace I x⊢ (g.val x) (a • v) = (RingHom.id ℝ) a • (g.val x) v E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g✝:PseudoRiemannianMetric E H M n Ig:PseudoRiemannianMetric E H M n Ix:Ma:ℝv:TangentSpace I x⊢ a • (g.val x) v = (RingHom.id ℝ) a • (g.val x) v; All goals completed! 🐙
cont := ContinuousLinearMap.continuous (g.val x)@[simp]
lemma flatL_apply (g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) :
(flatL g x v) w = g.val x v w := rflE:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:M⊢ ∀ (m : TangentSpace I x), (g.flat x) m = 0 → m = 0
All goals completed! 🐙@[simp]
lemma flatL_inj (g : PseudoRiemannianMetric 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) := E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:M⊢ Surjective ⇑(g.flatL x)
E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:Mthis:FiniteDimensional ℝ (TangentSpace I x)⊢ Surjective ⇑(g.flatL x)
E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:Mthis✝:FiniteDimensional ℝ (TangentSpace I x)this:T2Space (TangentSpace I x)⊢ Surjective ⇑(g.flatL x)
E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:Mthis✝:FiniteDimensional ℝ (TangentSpace I x)this:T2Space (TangentSpace I x)h_finrank_eq:finrank ℝ (TangentSpace I x) = finrank ℝ (TangentSpace I x →L[ℝ] ℝ)⊢ Surjective ⇑(g.flatL x)
All goals completed! 🐙
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) :
TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
have : T2Space (TangentSpace I x) := inferInstanceAs (T2Space E)
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@[simp]
lemma flatEquiv_apply
(g : PseudoRiemannianMetric E H M n I) (x : M) (v w : TangentSpace I x) :
(g.flatEquiv x v) w = g.val x v w := rflSharp
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) :
(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).toContinuousLinearMaplemma sharpL_eq_toContinuousLinearMap
(g : PseudoRiemannianMetric E H M n I) (x : M) :
g.sharpL x = (g.sharpEquiv x).toContinuousLinearMap := rfllemma 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@[simp]
lemma sharpL_apply_flatL
(g : PseudoRiemannianMetric E H M n I) (x : M) (v : TangentSpace I x) :
g.sharpL x (g.flatL x v) = v :=
(g.flatEquiv x).left_inv v@[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 ω
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 ω) = ω :=
flatL_apply_sharpL g x ω@[simp]
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 :=
sharpL_apply_flatL g x v
The metric evaluated at sharp ω₁ and sharp ω₂.
All goals completed! 🐙
The metric evaluated at v and sharp ω.
All goals completed! 🐙Cotangent
@[simp]
lemma cotangentMetricVal_eq_apply_sharp (g : PseudoRiemannianMetric E H M n I) (x : M)
(ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) :
cotangentMetricVal g x ω₁ ω₂ = ω₁ (g.sharpL x ω₂) :=
apply_sharp_sharp g x ω₁ ω₂lemma cotangentMetricVal_symm (g : PseudoRiemannianMetric E H M n I) (x : M)
(ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) :
cotangentMetricVal g x ω₁ ω₂ = cotangentMetricVal g x ω₂ ω₁ := E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:Mω₁:TangentSpace I x →L[ℝ] ℝω₂:TangentSpace I x →L[ℝ] ℝ⊢ g.cotangentMetricVal x ω₁ ω₂ = g.cotangentMetricVal x ω₂ ω₁
All goals completed! 🐙@[simp]
lemma cotangentToBilinForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M)
(ω₁ ω₂ : TangentSpace I x →L[ℝ] ℝ) :
cotangentToBilinForm g x ω₁ ω₂ = cotangentMetricVal g x ω₁ ω₂ := rfl@[simp]
lemma cotangentToQuadraticForm_apply (g : PseudoRiemannianMetric E H M n I) (x : M)
(ω : TangentSpace I x →L[ℝ] ℝ) :
cotangentToQuadraticForm g x ω = cotangentMetricVal g x ω ω := rfl@[simp]
lemma cotangentToBilinForm_isSymm (g : PseudoRiemannianMetric E H M n I) (x : M) :
(cotangentToBilinForm g x).IsSymm := ⟨cotangentMetricVal_symm g x⟩
The cotangent metric is non-degenerate: if cotangentMetricVal g x ω v = 0 for all v,
then ω = 0.
E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:Mω:TangentSpace I x →L[ℝ] ℝh:∀ (v : TangentSpace I x →L[ℝ] ℝ), g.cotangentMetricVal x ω v = 0w:TangentSpace I xhw:ω w = 0⊢ ω w = 0 w
All goals completed! 🐙@[simp]
lemma cotangentToBilinForm_nondegenerate (g : PseudoRiemannianMetric E H M n I) (x : M) :
(cotangentToBilinForm g x).Nondegenerate := E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:M⊢ (g.cotangentToBilinForm x).Nondegenerate
E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:Mω:TangentSpace I x →L[ℝ] ℝhω:∀ (x_1 : TangentSpace I x →L[ℝ] ℝ), ((g.cotangentToBilinForm x) x_1) ω = 0⊢ ω = 0
E:Type vH:Type wM:Type wn:WithTop ℕ∞inst✝⁶:NormedAddCommGroup Einst✝⁵:NormedSpace ℝ Einst✝⁴:TopologicalSpace Hinst✝³:TopologicalSpace Minst✝²:ChartedSpace H Minst✝¹:ChartedSpace H EI:ModelWithCorners ℝ E Hinst✝:IsManifold I (n + 1) Minst_tangent_findim:∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)g:PseudoRiemannianMetric E H M n Ix:Mω:TangentSpace I x →L[ℝ] ℝhω:∀ (x_1 : TangentSpace I x →L[ℝ] ℝ), ((g.cotangentToBilinForm x) x_1) ω = 0v:TangentSpace I x →L[ℝ] ℝ⊢ g.cotangentMetricVal x ω v = 0
All goals completed! 🐙