Documentation

TauCeti.Geometry.Manifold.Riemannian.Isometry.Restriction

Curvature of a metric restricted to an open submanifold #

Let g be a smooth Riemannian metric on M and U ⊆ M an open set. The inclusion U → M is a local Riemannian isometry from the restricted metric g|_U (Bundle.ContMDiffRiemannianMetric.restrictOpenTangentSpace) to g, so every curvature quantity of g|_U at x ∈ U is that of g at x. In particular Scal(g|_U) = Scal(g) on U.

Consequently scalar curvature is local in the metric: two metrics that agree on a neighbourhood of x have the same scalar curvature at x, and two metrics that agree on an open set have the same scalar curvature there. This is what lets constructions that modify a metric only away from a set, such as gluing along collars or interpolating in a tube, keep the scalar curvature unchanged where the metric is unchanged.

Likewise, the restriction of a metric on M × ℝ to the manifold with boundary M × [a, b] (Bundle.ContMDiffRiemannianMetric.restrictIcc) is a pullback along a map with invertible differential, so its scalar curvature at (x, t) is that of the metric at (x, t).

Main results #

References #

source
theorem Bundle.ContMDiffRiemannianMetric.isLocalRiemannianIsometry_restrictOpenTangentSpace {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 1 M] {n : WithTop ℕ∞} (g : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (U : TopologicalSpace.Opens M) :
TauCeti.IsLocalRiemannianIsometry I I Subtype.val

The inclusion of an open submanifold U ⊆ M is a local Riemannian isometry from the restriction of a metric g to U to the metric g itself.

source
@[simp]
theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_restrictOpenTangentSpace {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] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (U : TopologicalSpace.Opens M) (x : ↥U) :
(g.restrictOpenTangentSpace U).scalarCurvature x = g.scalarCurvature ↑x

Scalar curvature is local. The scalar curvature of the restriction of a metric g to an open submanifold U is the scalar curvature of g at each point of U.

source
theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_eq_of_eventually_inner_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] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {g₁ g₂ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} {x : M} (h : ∀ᶠ (y : M) in nhds x, g₁.inner y = g₂.inner y) :
g₁.scalarCurvature x = g₂.scalarCurvature x

Locality of scalar curvature. Two metrics that agree on a neighbourhood of x have the same scalar curvature at x.

source
theorem Bundle.ContMDiffRiemannianMetric.eqOn_scalarCurvature {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] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {g₁ g₂ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} {U : Set M} (hU : IsOpen U) (h : ∀ x ∈ U, g₁.inner x = g₂.inner x) :
Set.EqOn g₁.scalarCurvature g₂.scalarCurvature U

Two metrics that agree on an open set have the same scalar curvature on it.

source
@[simp]
theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_restrictIcc {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] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] {a b : ℝ} [Fact (a < b)] (G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p) (p : M × ↑(Set.Icc a b)) :
(restrictIcc a b G).scalarCurvature p = G.scalarCurvature (p.1, ↑p.2)

The scalar curvature of the restriction of a metric G on M × ℝ to M × [a, b] at (x, t) is that of G at (x, t).