Smooth families of nondegenerate metrics #
Let P be a parameter manifold. A smooth family of nondegenerate metrics on M parametrized by
P assigns to each (p, x) : P × M a symmetric nondegenerate bilinear form on T_x M, smoothly
in (p, x) jointly. This file realizes such a family as a native smooth section over P × M of
the pullback, along the projection P × M → M, of the tangent bilinear-form bundle of M.
Freezing the parameter gives a smooth nondegenerate metric on M for every p : P. Every single
metric is a constant family, and a family can be restricted along a smooth map of parameter
manifolds, for example along a smooth curve t ↦ p t. The signature of the frozen metrics is
locally constant jointly in the parameter and the point, so it is fixed on each connected
component of P × M.
These families are the carrier for the parameter dependence of the Levi-Civita connection of a varying, possibly indefinite, metric and for its first variation.
Main definitions and results #
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily: a smooth family of symmetric nondegenerate tangent bilinear forms onM, parametrized byP.TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.contMDiff: joint smoothness of the family as a map into the tangent bilinear-form bundle ofM.TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.ofContMDiff: the converse construction.TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.metric: the metric at a fixed parameter.TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.constandTauCeti.Manifold.ContMDiffNondegenerateMetricFamily.comp: constant families and restriction along a smooth parameter map.TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.contMDiffAt_comp: a family restricted along aC^nparameter map is jointlyC^n.TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.isLocallyConstant_signature_metric: the signature is locally constant onP × M.
References #
- B. O'Neill, Semi-Riemannian Geometry, Academic Press, 1983, Chapter 3.
structure
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
(IP : ModelWithCorners ℝ EP HP)
(P : Type u_6)
[TopologicalSpace P]
[ChartedSpace HP P]
:
Type (max (max u_1 u_3) u_6)
A smooth family, parametrized by P, of symmetric nondegenerate real bilinear forms on the
tangent bundle of M.
The family is a native smooth section over P × M of the pullback of the tangent
bilinear-form bundle of M along the projection P × M → M; its value at (p, x) is a bilinear
form on T_x M. As for a single metric, no positivity or signature is imposed.
- toContMDiffSection : ContMDiffSection (IP.prod I) (E →L[ℝ] E →L[ℝ] ℝ) (↑⊤) (⇑ContMDiffMap.snd *ᵖ fun (x : M) => TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ)
The smooth section of the pulled-back bundle of continuous bilinear forms.
- symm (q : P × M) : (ContinuousLinearMap.toBilinForm (self.toContMDiffSection q)).IsSymm
The bilinear form at every parameter and point is symmetric.
- nondegenerate (q : P × M) : (ContinuousLinearMap.toBilinForm (self.toContMDiffSection q)).Nondegenerate
The bilinear form at every parameter and point is nondegenerate.
Instances For
def
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.toFun
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
(q : P × M)
:
The bilinear form of a smooth nondegenerate metric family at a parameter and a point.
Instances For
@[instance_reducible]
instance
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.instCoeFunForallContinuousLinearMapRealIdTangentSpaceSnd
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
:
CoeFun (ContMDiffNondegenerateMetricFamily I M IP P) fun (x : ContMDiffNondegenerateMetricFamily I M IP P) =>
(q : P × M) → TangentSpace I q.2 →L[ℝ] TangentSpace I q.2 →L[ℝ] ℝ
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.toContMDiffSection_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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
(q : P × M)
:
The underlying smooth section of a smooth nondegenerate metric family evaluates as the family.
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.apply_comm
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
(q : P × M)
(v w : TangentSpace I q.2)
:
Evaluation of a smooth nondegenerate metric family is symmetric in its tangent arguments.
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.ext
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
{g h : ContMDiffNondegenerateMetricFamily I M IP P}
(heq : ∀ (q : P × M) (v w : TangentSpace I q.2), ((↑g q) v) w = ((↑h q) v) w)
:
Smooth nondegenerate metric families are equal when all their fibrewise pairings agree.
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.ext_iff
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
{g h : ContMDiffNondegenerateMetricFamily I M IP P}
:
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.contMDiff
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
:
A smooth nondegenerate metric family is jointly smooth in the parameter and the point, as a
map into the tangent bilinear-form bundle of M.
def
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.ofContMDiff
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(φ : (q : P × M) → TangentSpace I q.2 →L[ℝ] TangentSpace I q.2 →L[ℝ] ℝ)
(hφ : ContMDiff (IP.prod I) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) ↑⊤ fun (q : P × M) => ⟨q.2, φ q⟩)
(hsymm : ∀ (q : P × M), (φ q).toBilinForm.IsSymm)
(hnd : ∀ (q : P × M), (φ q).toBilinForm.Nondegenerate)
:
ContMDiffNondegenerateMetricFamily I M IP P
A jointly smooth field of symmetric nondegenerate tangent bilinear forms on M,
parametrized by P, as a smooth nondegenerate metric family.
Instances For
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.ofContMDiff_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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(φ : (q : P × M) → TangentSpace I q.2 →L[ℝ] TangentSpace I q.2 →L[ℝ] ℝ)
(hφ : ContMDiff (IP.prod I) (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) ↑⊤ fun (q : P × M) => ⟨q.2, φ q⟩)
(hsymm : ∀ (q : P × M), (φ q).toBilinForm.IsSymm)
(hnd : ∀ (q : P × M), (φ q).toBilinForm.Nondegenerate)
(q : P × M)
:
The family built from a jointly smooth field of forms evaluates to that field.
def
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.metric
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
(p : P)
:
The smooth nondegenerate metric on M obtained by freezing the parameter at p.
Instances For
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.metric_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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
(p : P)
(x : M)
:
The metric at a fixed parameter evaluates as the family.
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.metric_injective
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
:
A smooth nondegenerate metric family is determined by its metrics at fixed parameters.
def
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.const
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g₀ : ContMDiffNondegenerateMetric)
:
ContMDiffNondegenerateMetricFamily I M IP P
The constant family with value a smooth nondegenerate metric.
Instances For
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.const_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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g₀ : ContMDiffNondegenerateMetric)
(q : P × M)
:
The constant family takes the value of its metric at every parameter.
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.metric_const
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g₀ : ContMDiffNondegenerateMetric)
(p : P)
:
Freezing the parameter of a constant family recovers its metric.
def
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.comp
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
{EP' : Type u_7}
[NormedAddCommGroup EP']
[NormedSpace ℝ EP']
{HP' : Type u_8}
[TopologicalSpace HP']
{IP' : ModelWithCorners ℝ EP' HP'}
{P' : Type u_9}
[TopologicalSpace P']
[ChartedSpace HP' P']
(c : ContMDiffMap IP' IP P' P ↑⊤)
:
ContMDiffNondegenerateMetricFamily I M IP' P'
The restriction of a smooth nondegenerate metric family along a smooth map of parameter
manifolds c : P' → P; its value at (p', x) is the value of the family at (c p', x).
Instances For
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.comp_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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
{EP' : Type u_7}
[NormedAddCommGroup EP']
[NormedSpace ℝ EP']
{HP' : Type u_8}
[TopologicalSpace HP']
{IP' : ModelWithCorners ℝ EP' HP'}
{P' : Type u_9}
[TopologicalSpace P']
[ChartedSpace HP' P']
(c : ContMDiffMap IP' IP P' P ↑⊤)
(q : P' × M)
:
The restriction along a parameter map evaluates the family at the image parameter.
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.contMDiffAt_comp
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
{EP' : Type u_7}
[NormedAddCommGroup EP']
[NormedSpace ℝ EP']
{HP' : Type u_8}
[TopologicalSpace HP']
{IP' : ModelWithCorners ℝ EP' HP'}
{P' : Type u_9}
[TopologicalSpace P']
[ChartedSpace HP' P']
{n : WithTop ℕ∞}
(hn : n ≤ ↑⊤)
{c : P' → P}
{p' : P'}
(hc : ContMDiffAt IP' IP n c p')
(x : M)
:
Restricted along a parameter map c which is C^n at p', for n ≤ ∞, a smooth
nondegenerate metric family is jointly C^n at (p', x), as a map into the tangent
bilinear-form bundle of M.
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.metric_comp
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
{EP' : Type u_7}
[NormedAddCommGroup EP']
[NormedSpace ℝ EP']
{HP' : Type u_8}
[TopologicalSpace HP']
{IP' : ModelWithCorners ℝ EP' HP'}
{P' : Type u_9}
[TopologicalSpace P']
[ChartedSpace HP' P']
(c : ContMDiffMap IP' IP P' P ↑⊤)
(p' : P')
:
Freezing the parameter of a restricted family freezes the original family at the image parameter.
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.comp_id
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
:
Restricting a family along the identity parameter map gives the family back.
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.comp_comp
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
{EP' : Type u_7}
[NormedAddCommGroup EP']
[NormedSpace ℝ EP']
{HP' : Type u_8}
[TopologicalSpace HP']
{IP' : ModelWithCorners ℝ EP' HP'}
{P' : Type u_9}
[TopologicalSpace P']
[ChartedSpace HP' P']
{EP'' : Type u_10}
[NormedAddCommGroup EP'']
[NormedSpace ℝ EP'']
{HP'' : Type u_11}
[TopologicalSpace HP'']
{IP'' : ModelWithCorners ℝ EP'' HP''}
{P'' : Type u_12}
[TopologicalSpace P'']
[ChartedSpace HP'' P'']
(c : ContMDiffMap IP' IP P' P ↑⊤)
(c' : ContMDiffMap IP'' IP' P'' P' ↑⊤)
:
Restricting a family along two parameter maps in turn is restricting along their composite.
@[simp]
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.const_comp
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
{EP' : Type u_7}
[NormedAddCommGroup EP']
[NormedSpace ℝ EP']
{HP' : Type u_8}
[TopologicalSpace HP']
{IP' : ModelWithCorners ℝ EP' HP'}
{P' : Type u_9}
[TopologicalSpace P']
[ChartedSpace HP' P']
(g₀ : ContMDiffNondegenerateMetric)
(c : ContMDiffMap IP' IP P' P ↑⊤)
:
Restricting a constant family along a parameter map gives the constant family.
@[instance_reducible]
noncomputable def
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.instNormedAddCommGroupContinuousLinearMapRealId
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
:
Cache the canonical normed additive group while elaborating bilinear bundle coordinates.
Instances For
@[instance_reducible]
noncomputable def
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.instNormedSpaceRealContinuousLinearMapId
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
:
Cache the canonical real normed space while elaborating bilinear bundle coordinates.
Instances For
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.contMDiffAt_inCoordinates
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
(a : M)
{q : P × M}
(hq : q.2 ∈ (trivializationAt E (TangentSpace I) a).baseSet)
:
ContMDiffAt (IP.prod I) (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ)) (↑⊤)
(fun (q : P × M) => (g.metric q.1).inCoordinates a q.2) q
The coordinate metrics of a smooth metric family are jointly smooth in parameter and base point on the base set of the chosen tangent trivialization.
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.contMDiffAt_chartMetric
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
(a : M)
{q : P × E}
(hq : q.2 ∈ (extChartAt I a).target)
(hint : q.2 ∈ interior (Set.range ↑I))
:
ContMDiffAt (IP.prod (modelWithCornersSelf ℝ E)) (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ)) (↑⊤)
(fun (q : P × E) => (g.metric q.1).chartMetric a q.2) q
In a base chart, the coordinate metrics of a smooth family are jointly smooth at every parameter and every interior point of the chart target.
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.isLocallyConstant_signature_metric
{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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
[FiniteDimensional ℝ E]
:
IsLocallyConstant fun (q : P × M) => (g.metric q.1).signature q.2
The signature of the metrics of a smooth nondegenerate family is locally constant jointly in the parameter and the point.
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.signature_metric_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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
[FiniteDimensional ℝ E]
{q q' : P × M}
(hq' : q' ∈ connectedComponent q)
:
A smooth nondegenerate metric family has one fixed signature on each connected component of
P × M.
theorem
TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.signature_metric_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]
{EP : Type u_4}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_5}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_6}
[TopologicalSpace P]
[ChartedSpace HP P]
(g : ContMDiffNondegenerateMetricFamily I M IP P)
[FiniteDimensional ℝ E]
[PreconnectedSpace P]
[PreconnectedSpace M]
(p p' : P)
(x x' : M)
:
Over a preconnected parameter manifold and a preconnected manifold, a smooth nondegenerate metric family has one fixed signature.