Signature of a smooth nondegenerate metric

The positive and negative inertia indices of a continuous family of symmetric nondegenerate tangent bilinear forms are locally constant. The family is any continuous map into the total space of the tangent bilinear-form bundle, so this covers a smooth nondegenerate metric as well as a family of metrics depending on a parameter. The proof reads the forms in a tangent-bundle trivialization and applies stability of the signature for continuous families of forms on the fixed model space. The coordinate form is isometric to the original form, so its inertia indices are intrinsic.

Thus a smooth nondegenerate metric has one fixed signature on each connected component. This is the topological input for treating a nondegenerate metric of fixed signature as a pseudo-Riemannian metric.

Main results

• TauCeti.Manifold.isLocallyConstant_sigPos_sigNeg_of_continuous proves that the inertia indices of a continuous family of symmetric nondegenerate tangent bilinear forms are locally constant.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.signature is the pair consisting of the positive and negative inertia indices.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.isLocallyConstant_signature proves that this pair is locally constant.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.signature_eq_of_mem_connectedComponent and signature_eq give the connected-component and preconnected-space consequences.

References

• B. O'Neill, Semi-Riemannian Geometry, Academic Press, 1983, Chapter 3.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Chapter 2.

noncomputable def TauCeti.Manifold.ContMDiffNondegenerateMetric.signature {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] (g : ContMDiffNondegenerateMetric) (x : M) : ℕ × ℕ

The signature of a smooth nondegenerate metric at a point, with the positive inertia index first and the negative inertia index second.

@[simp]

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.signature_fst {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] (g : ContMDiffNondegenerateMetric) (x : M) : (g.signature x).1 = sigPos (LinearMap.BilinMap.toQuadraticMap (g.toContMDiffSection x).toBilinForm)

The first component of the metric signature is its positive inertia index.

@[simp]

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.signature_snd {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] (g : ContMDiffNondegenerateMetric) (x : M) : (g.signature x).2 = sigNeg (LinearMap.BilinMap.toQuadraticMap (g.toContMDiffSection x).toBilinForm)

The second component of the metric signature is its negative inertia index.

theorem TauCeti.Manifold.sigPos_sigNeg_tangentBilinFormInCoordinates {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] (a : M) {x : M} (hx : x ∈ (trivializationAt E (fun (y : M) => TangentSpace I y) a).baseSet) (ϕ : TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ) : (sigPos (LinearMap.BilinMap.toQuadraticMap (tangentBilinFormInCoordinates a x ϕ).toBilinForm), sigNeg (LinearMap.BilinMap.toQuadraticMap (tangentBilinFormInCoordinates a x ϕ).toBilinForm)) = (sigPos (LinearMap.BilinMap.toQuadraticMap ϕ.toBilinForm), sigNeg (LinearMap.BilinMap.toQuadraticMap ϕ.toBilinForm))

A tangent bilinear form read in a trivialization has the same positive and negative inertia indices as the form itself, on the base set of that trivialization.

theorem TauCeti.Manifold.isLocallyConstant_sigPos_sigNeg_of_continuous {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] {X : Type u_4} [TopologicalSpace X] {q : X → Bundle.TotalSpace (E →L[ℝ] E →L[ℝ] ℝ) fun (x : M) => TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} (hq : Continuous q) (hsymm : ∀ (y : X), (q y).snd.toBilinForm.IsSymm) (hnd : ∀ (y : X), (q y).snd.toBilinForm.Nondegenerate) : IsLocallyConstant fun (y : X) => (sigPos (LinearMap.BilinMap.toQuadraticMap (q y).snd.toBilinForm), sigNeg (LinearMap.BilinMap.toQuadraticMap (q y).snd.toBilinForm))

The positive and negative inertia indices of a continuous family of symmetric nondegenerate tangent bilinear forms are locally constant. The family is a continuous map from an arbitrary topological space to the total space of the tangent bilinear-form bundle, so its base point may vary as well as the form.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isLocallyConstant_signature {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 : ContMDiffNondegenerateMetric) : IsLocallyConstant g.signature

The signature of a smooth nondegenerate metric is locally constant.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.signature_eq_of_mem_connectedComponent {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 : ContMDiffNondegenerateMetric) {x y : M} (hy : y ∈ connectedComponent x) : g.signature y = g.signature x

The metric signature is constant on each connected component.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.signature_eq {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] [PreconnectedSpace M] (g : ContMDiffNondegenerateMetric) (x y : M) : g.signature x = g.signature y

On a preconnected manifold, a smooth nondegenerate metric has one fixed signature.