Uniform positive scalar curvature for compact families of metrics

Let g p be a family of smooth Riemannian metrics on a manifold without boundary, indexed by a topological space P. The family is continuous in the C² sense when, in the chart at each point and in a fixed basis of the model, the Gram matrix of the chart metric and its first and second derivatives depend jointly continuously on the parameter and the chart point. Scalar curvature is a continuous function of this second-order jet wherever the Gram matrix is invertible (ContinuousAt.scalarCurvatureOfJet), so for such a family (p, x) ↦ Scal(g p)(x) is jointly continuous. Consequently, on a compact set of parameters and points at which the scalar curvature is positive, it has a uniform positive lower bound. In particular, a family of metrics of positive scalar curvature on a compact manifold, indexed by a compact space, has a common positive lower bound for its scalar curvature.

The bound also holds relative to a closed set C near which the family is fixed: if every g p agrees with one metric g₀ on a common neighbourhood of C, then the scalar curvature of g p is that of g₀ there, so positivity of the scalar curvature of g₀ on C together with the hypotheses above at the points outside C already gives a uniform positive lower bound. No continuity in the parameter needs to be checked near C.

This uniform scalar gap is the margin consumed when a compact family of metrics of positive scalar curvature is perturbed, for instance when a path of such metrics is smoothed or reparametrized.

Main results

• TauCeti.Manifold.exists_pos_le_scalarCurvature_of_isCompact: a uniform positive lower bound on a compact set of parameters and points where the scalar curvature is positive.
• TauCeti.Manifold.exists_pos_forall_le_scalarCurvature: a compact family of metrics of positive scalar curvature on a compact manifold has a common positive lower bound.
• TauCeti.Manifold.exists_pos_le_scalarCurvature_of_isCompact_of_eventually_inner_eq: a uniform positive lower bound on a compact set of parameters and points for a family fixed near a closed set.
• TauCeti.Manifold.exists_pos_forall_le_scalarCurvature_of_eventually_inner_eq: on a compact manifold, a compact family fixed near a closed set and of positive scalar curvature away from it has a common positive lower bound.

References

• M. Gromov, H. B. Lawson, The classification of simply connected manifolds of positive scalar curvature, Ann. of Math. 111 (1980), 423–434.

theorem TauCeti.Manifold.exists_pos_le_scalarCurvature_of_isCompact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {P : Type u_4} [TopologicalSpace P] (g : P → Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) {S : Set (P × M)} (hS : IsCompact S) (h₀ : ∀ q ∈ S, ContinuousAt (fun (r : P × E) => (LinearMap.toMatrix₂ b b) ((g r.1).toNondegenerateMetric.chartMetric q.2 r.2).toBilinForm) (q.1, ↑(extChartAt I q.2) q.2)) (h₁ : ∀ q ∈ S, ContinuousAt (fun (r : P × E) (k i j : ι) => (fderiv ℝ (fun (z : E) => (((g r.1).toNondegenerateMetric.chartMetric q.2 z) (b i)) (b j)) r.2) (b k)) (q.1, ↑(extChartAt I q.2) q.2)) (h₂ : ∀ q ∈ S, ContinuousAt (fun (r : P × E) (m k i j : ι) => (fderiv ℝ (fun (z : E) => (fderiv ℝ (fun (z' : E) => (((g r.1).toNondegenerateMetric.chartMetric q.2 z') (b i)) (b j)) z) (b k)) r.2) (b m)) (q.1, ↑(extChartAt I q.2) q.2)) (hpos : ∀ q ∈ S, 0 < (g q.1).scalarCurvature q.2) : ∃ (ε : ℝ), 0 < ε ∧ ∀ q ∈ S, ε ≤ (g q.1).scalarCurvature q.2

A uniform scalar-curvature gap on compact sets. Let g p be a family of metrics whose chart metrics have Gram matrices, first and second derivatives in the basis b depending continuously on the parameter and the chart point at every point of a compact set S ⊆ P × M. If the scalar curvature of g p is positive at x for every (p, x) ∈ S, then it is bounded below on S by a positive constant.

theorem TauCeti.Manifold.exists_pos_forall_le_scalarCurvature {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {P : Type u_4} [TopologicalSpace P] (g : P → Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) [CompactSpace P] [CompactSpace M] (h₀ : ∀ (p : P) (x : M), ContinuousAt (fun (r : P × E) => (LinearMap.toMatrix₂ b b) ((g r.1).toNondegenerateMetric.chartMetric x r.2).toBilinForm) (p, ↑(extChartAt I x) x)) (h₁ : ∀ (p : P) (x : M), ContinuousAt (fun (r : P × E) (k i j : ι) => (fderiv ℝ (fun (z : E) => (((g r.1).toNondegenerateMetric.chartMetric x z) (b i)) (b j)) r.2) (b k)) (p, ↑(extChartAt I x) x)) (h₂ : ∀ (p : P) (x : M), ContinuousAt (fun (r : P × E) (m k i j : ι) => (fderiv ℝ (fun (z : E) => (fderiv ℝ (fun (z' : E) => (((g r.1).toNondegenerateMetric.chartMetric x z') (b i)) (b j)) z) (b k)) r.2) (b m)) (p, ↑(extChartAt I x) x)) (hpos : ∀ (p : P), (g p).HasPositiveScalarCurvature) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (p : P) (x : M), ε ≤ (g p).scalarCurvature x

Compact families of metrics of positive scalar curvature have a uniform scalar gap. On a compact manifold, a family of metrics of positive scalar curvature indexed by a compact space, whose chart metrics have Gram matrices, first and second derivatives in the basis b depending continuously on the parameter and the chart point, has scalar curvature bounded below by a common positive constant.

theorem TauCeti.Manifold.exists_pos_le_scalarCurvature_of_isCompact_of_eventually_inner_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {P : Type u_4} [TopologicalSpace P] (g : P → Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) {S : Set (P × M)} (hS : IsCompact S) {C : Set M} (hC : IsClosed C) (g₀ : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hfix : ∀ᶠ (x : M) in nhdsSet C, ∀ (p : P), (g p).inner x = g₀.inner x) (h₀ : ∀ q ∈ S, q.2 ∉ C → ContinuousAt (fun (r : P × E) => (LinearMap.toMatrix₂ b b) ((g r.1).toNondegenerateMetric.chartMetric q.2 r.2).toBilinForm) (q.1, ↑(extChartAt I q.2) q.2)) (h₁ : ∀ q ∈ S, q.2 ∉ C → ContinuousAt (fun (r : P × E) (k i j : ι) => (fderiv ℝ (fun (z : E) => (((g r.1).toNondegenerateMetric.chartMetric q.2 z) (b i)) (b j)) r.2) (b k)) (q.1, ↑(extChartAt I q.2) q.2)) (h₂ : ∀ q ∈ S, q.2 ∉ C → ContinuousAt (fun (r : P × E) (m k i j : ι) => (fderiv ℝ (fun (z : E) => (fderiv ℝ (fun (z' : E) => (((g r.1).toNondegenerateMetric.chartMetric q.2 z') (b i)) (b j)) z) (b k)) r.2) (b m)) (q.1, ↑(extChartAt I q.2) q.2)) (hpos₀ : ∀ q ∈ S, q.2 ∈ C → 0 < g₀.scalarCurvature q.2) (hpos : ∀ q ∈ S, q.2 ∉ C → 0 < (g q.1).scalarCurvature q.2) : ∃ (ε : ℝ), 0 < ε ∧ ∀ q ∈ S, ε ≤ (g q.1).scalarCurvature q.2

A uniform scalar-curvature gap relative to a closed set. Let g p be a family of metrics, all of which agree with a fixed metric g₀ on a common neighbourhood of a closed set C, and let S ⊆ P × M be compact. Suppose that the scalar curvature of g₀ is positive at x for every (p, x) ∈ S with x ∈ C, and that for every (p, x) ∈ S with x ∉ C the scalar curvature of g p is positive at x and the chart metrics have Gram matrices, first and second derivatives in the basis b depending continuously on the parameter and the chart point. Then the scalar curvature is bounded below on S by a positive constant.

theorem TauCeti.Manifold.exists_pos_forall_le_scalarCurvature_of_eventually_inner_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {P : Type u_4} [TopologicalSpace P] (g : P → Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) [CompactSpace P] [CompactSpace M] {C : Set M} (hC : IsClosed C) (g₀ : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hfix : ∀ᶠ (x : M) in nhdsSet C, ∀ (p : P), (g p).inner x = g₀.inner x) (h₀ : ∀ (p : P), ∀ x ∉ C, ContinuousAt (fun (r : P × E) => (LinearMap.toMatrix₂ b b) ((g r.1).toNondegenerateMetric.chartMetric x r.2).toBilinForm) (p, ↑(extChartAt I x) x)) (h₁ : ∀ (p : P), ∀ x ∉ C, ContinuousAt (fun (r : P × E) (k i j : ι) => (fderiv ℝ (fun (z : E) => (((g r.1).toNondegenerateMetric.chartMetric x z) (b i)) (b j)) r.2) (b k)) (p, ↑(extChartAt I x) x)) (h₂ : ∀ (p : P), ∀ x ∉ C, ContinuousAt (fun (r : P × E) (m k i j : ι) => (fderiv ℝ (fun (z : E) => (fderiv ℝ (fun (z' : E) => (((g r.1).toNondegenerateMetric.chartMetric x z') (b i)) (b j)) z) (b k)) r.2) (b m)) (p, ↑(extChartAt I x) x)) (hpos₀ : ∀ x ∈ C, 0 < g₀.scalarCurvature x) (hpos : ∀ (p : P), ∀ x ∉ C, 0 < (g p).scalarCurvature x) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (p : P) (x : M), ε ≤ (g p).scalarCurvature x

Compact families fixed near a closed set have a uniform scalar gap. On a compact manifold, let g p be a family of metrics, indexed by a compact space, all of which agree with a fixed metric g₀ on a common neighbourhood of a closed set C. If the scalar curvature of g₀ is positive on C, and outside C the scalar curvature of each g p is positive and the chart metrics have Gram matrices, first and second derivatives in the basis b depending continuously on the parameter and the chart point, then the scalar curvatures of the metrics g p are bounded below by a common positive constant.