Concordance of metrics of positive scalar curvature

Two metrics g₀ and g₁ of positive scalar curvature on M are concordant if there is a metric of positive scalar curvature on the cylinder M × ℝ which is the product metric g₀ + dt² where t ≤ 0 and g₁ + dt² where t ≥ 1. Concordance is the relation between metrics of positive scalar curvature produced by the surgery and bordism constructions.

This file sets up the cylinder metric g + dt², whose scalar curvature at (x, t) is that of g at x, and reparametrisations of the ℝ-coordinate of a metric on M × ℝ, pullbacks along (x, t) ↦ (x, φ t) for a smooth φ with nowhere vanishing derivative. Reparametrising by t ↦ 1 - t reverses a concordance. To concatenate two concordances, the second is translated by 2, glued to the first along 1 < t < 2, where both are the same product metric, and the window [0, 3] is compressed into [0, 1]. The compression is a reparametrisation which is a translation near both ends: an affine rescaling of t would replace dt² by a multiple and destroy the product ends. Hence concordance is an equivalence relation on metrics of positive scalar curvature.

Concordance is natural. Pulling a concordance back along (x, t) ↦ (f x, t), for a smooth map f whose differential is invertible at every point, such as a diffeomorphism or a covering map, gives a concordance between the pullbacks of its ends. Multiplying a concordance by a constant c > 0 multiplies dt² by c as well; reparametrising by t ↦ t / √c restores the product ends, so c g₀ and c g₁ are concordant when g₀ and g₁ are. The product of a concordance from g₀ to g₁ with a metric g₂ of nonnegative scalar curvature, with the cylinder coordinate moved from M × ℝ to (M × N) × ℝ, is a concordance from g₀ × g₂ to g₁ × g₂.

Concordances can equivalently be taken on the manifold with boundary M × [0, 1]: a collared concordance is a metric of positive scalar curvature on M × [0, 1] which is g₀ + dt² near t = 0 and g₁ + dt² near t = 1, where g + dt² on M × [0, 1] is the restriction Bundle.ContMDiffRiemannianMetric.restrictIcc of the cylinder metric. The restriction of a concordance to M × [0, 1] itself need not have product collars. Instead, a concordance is pulled back along (x, t) ↦ (x, ψ t) for a smooth increasing ψ : [0, 1] → [-1, 2] which is t ↦ t - 1 near 0 and t ↦ t + 1 near 1. Conversely, a collared concordance is extended by the product ends: it is pulled back to M × ℝ along (x, t) ↦ (x, θ t) for a smooth increasing θ : ℝ → (0, 1) which is the identity away from the two collars, and glued to g₀ + dt² and g₁ + dt² over the collars.

Main definitions

• Bundle.ContMDiffRiemannianMetric.cylinder: the cylinder metric g + dt² on M × ℝ.
• Bundle.ContMDiffRiemannianMetric.reparamTime: the pullback of a metric on M × ℝ along (x, t) ↦ (x, φ t).
• Bundle.ContMDiffRiemannianMetric.IsConcordance: a concordance from g₀ to g₁.
• Bundle.ContMDiffRiemannianMetric.Concordant: g₀ and g₁ are concordant, characterised by Bundle.ContMDiffRiemannianMetric.concordant_iff.
• Bundle.ContMDiffRiemannianMetric.IsCollaredConcordance: a collared concordance from g₀ to g₁ on M × [0, 1].

Main results

• Bundle.ContMDiffRiemannianMetric.scalarCurvature_cylinder: Scal(g + dt²)(x, t) = Scal(g)(x).
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_reparamTime: the scalar curvature of the reparametrised metric at (x, t) is that of the original metric at (x, φ t).
• Bundle.ContMDiffRiemannianMetric.cylinder_reparamTime_inner: a reparametrisation with |φ'| = 1 preserves the cylinder metric.
• Bundle.ContMDiffRiemannianMetric.IsConcordance.hasPositiveScalarCurvature_left and Bundle.ContMDiffRiemannianMetric.IsConcordance.hasPositiveScalarCurvature_right: the ends of a concordance have positive scalar curvature.
• Bundle.ContMDiffRiemannianMetric.concordant_self_iff: a metric is concordant to itself exactly when it has positive scalar curvature.
• Bundle.ContMDiffRiemannianMetric.IsConcordance.reparamTime_one_sub and Bundle.ContMDiffRiemannianMetric.Concordant.symm: reversal of concordances.
• Bundle.ContMDiffRiemannianMetric.Concordant.trans: concatenation of concordances.
• Bundle.ContMDiffRiemannianMetric.equivalence_concordant: concordance is an equivalence relation on metrics of positive scalar curvature.
• Bundle.ContMDiffRiemannianMetric.concordant_of_inner_eq_cylinder: a metric of positive scalar curvature on M × ℝ with product ends outside any window [a, b] witnesses a concordance.
• Bundle.ContMDiffRiemannianMetric.Concordant.pullback and Bundle.ContMDiffRiemannianMetric.concordant_pullback_iff: concordance is preserved by pullback along maps with invertible differential, and preserved and reflected by pullback along diffeomorphisms.
• Bundle.ContMDiffRiemannianMetric.Concordant.rescale_const and Bundle.ContMDiffRiemannianMetric.concordant_rescale_const_iff: rescaling by a positive constant preserves and reflects concordance.
• Bundle.ContMDiffRiemannianMetric.Concordant.prodTangentSpace_of_nonneg: concordance is preserved by products with a metric of nonnegative scalar curvature.
• Bundle.ContMDiffRiemannianMetric.IsConcordance.exists_isCollaredConcordance and Bundle.ContMDiffRiemannianMetric.IsCollaredConcordance.concordant: concordances give collared concordances with the same ends, and conversely, so that Bundle.ContMDiffRiemannianMetric.concordant_iff_exists_isCollaredConcordance.

References

• M. Gromov, H. B. Lawson, The classification of simply connected manifolds of positive scalar curvature, Ann. of Math. 111 (1980), 423–434.
• S. Stolz, Positive scalar curvature—constructions and obstructions, arXiv:2202.05904, for concordance and isotopy of metrics of positive scalar curvature.

noncomputable def Bundle.ContMDiffRiemannianMetric.cylinder {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 : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p

The cylinder metric g + dt² on M × ℝ: the product of g with the standard metric of ℝ.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.cylinder_inner {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 : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (p : M × ℝ) (v w : TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p) : ((g.cylinder.inner p) v) w = ((g.inner p.1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).1 + (NormedSpace.fromTangentSpace p.2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).2 * (NormedSpace.fromTangentSpace p.2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).2

The cylinder metric g + dt² pairs the M-components with g and multiplies the ℝ-components.

theorem Bundle.ContMDiffRiemannianMetric.cylinder_inner_mk {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 : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (x : M) (s t : ℝ) : g.cylinder.inner (x, s) = g.cylinder.inner (x, t)

The cylinder metric g + dt² at (x, s) and at (x, t) is the same bilinear form.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_cylinder {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 : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) [FiniteDimensional ℝ E] [T2Space M] (p : M × ℝ) : g.cylinder.scalarCurvature p = g.scalarCurvature p.1

The scalar curvature of the cylinder metric g + dt² at (x, t) is that of g at x.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.hasPositiveScalarCurvature_cylinder_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] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) [FiniteDimensional ℝ E] [T2Space M] : g.cylinder.HasPositiveScalarCurvature ↔ g.HasPositiveScalarCurvature

The cylinder metric g + dt² has positive scalar curvature exactly when g does.

noncomputable def Bundle.ContMDiffRiemannianMetric.reparamTime {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 : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p) (hφ : ContDiff ℝ (↑⊤) φ) (hφ' : ∀ (t : ℝ), deriv φ t ≠ 0) : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p

Reparametrise the ℝ-coordinate of a metric G on M × ℝ by a smooth φ : ℝ → ℝ with nowhere vanishing derivative: the pullback of G along (x, t) ↦ (x, φ t).

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.reparamTime_inner {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 : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} (hφ : ContDiff ℝ (↑⊤) φ) (hφ' : ∀ (t : ℝ), deriv φ t ≠ 0) (p : M × ℝ) (v w : TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p) : (((G.reparamTime hφ hφ').inner p) v) w = ((G.inner (p.1, φ p.2)) ((mfderiv% (Prod.map id φ) p) v)) ((mfderiv% (Prod.map id φ) p) w)

The reparametrised metric at (x, t) is G at (x, φ t), evaluated on the images of the tangent vectors under the differential of (x, t) ↦ (x, φ t).

theorem Bundle.ContMDiffRiemannianMetric.reparamTime_inner_congr {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 G' : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} (hφ : ContDiff ℝ (↑⊤) φ) (hφ' : ∀ (t : ℝ), deriv φ t ≠ 0) {p : M × ℝ} (h : G.inner (p.1, φ p.2) = G'.inner (p.1, φ p.2)) : (G.reparamTime hφ hφ').inner p = (G'.reparamTime hφ hφ').inner p

The reparametrised metric at (x, t) only depends on G at (x, φ t).

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_reparamTime {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 : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} [T2Space M] (hφ : ContDiff ℝ (↑⊤) φ) (hφ' : ∀ (t : ℝ), deriv φ t ≠ 0) (p : M × ℝ) : (G.reparamTime hφ hφ').scalarCurvature p = G.scalarCurvature (p.1, φ p.2)

The scalar curvature of the reparametrised metric at (x, t) is that of G at (x, φ t).

theorem Bundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature.reparamTime {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 : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} [T2Space M] (h : G.HasPositiveScalarCurvature) (hφ : ContDiff ℝ (↑⊤) φ) (hφ' : ∀ (t : ℝ), deriv φ t ≠ 0) : (G.reparamTime hφ hφ').HasPositiveScalarCurvature

Reparametrising the ℝ-coordinate preserves positive scalar curvature.

theorem Bundle.ContMDiffRiemannianMetric.cylinder_reparamTime_inner {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 : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hφ : ContDiff ℝ (↑⊤) φ) (hφ' : ∀ (t : ℝ), deriv φ t ≠ 0) {p : M × ℝ} (h : |deriv φ p.2| = 1) : (g.cylinder.reparamTime hφ hφ').inner p = g.cylinder.inner p

A reparametrisation of the ℝ-coordinate with |φ' t| = 1 leaves the cylinder metric g + dt² unchanged at (x, t).

theorem Bundle.ContMDiffRiemannianMetric.reparamTime_inner_eq_cylinder_inner {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 : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} {g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (hφ : ContDiff ℝ (↑⊤) φ) (hφ' : ∀ (t : ℝ), deriv φ t ≠ 0) {p : M × ℝ} (h : G.inner (p.1, φ p.2) = g.cylinder.inner (p.1, φ p.2)) (hd : |deriv φ p.2| = 1) : (G.reparamTime hφ hφ').inner p = g.cylinder.inner p

A reparametrisation of the ℝ-coordinate with |φ' t| = 1 of a metric which is the cylinder metric g + dt² at (x, φ t) is the cylinder metric g + dt² at (x, t).

structure Bundle.ContMDiffRiemannianMetric.IsConcordance {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] [T2Space M] (G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p) (g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) : Prop

A concordance from g₀ to g₁ is a metric of positive scalar curvature on M × ℝ which is the cylinder metric g₀ + dt² where t ≤ 0 and the cylinder metric g₁ + dt² where t ≥ 1.

• hasPositiveScalarCurvature : G.HasPositiveScalarCurvature

  A concordance has positive scalar curvature.

• inner_of_nonpos (p : M × ℝ) : p.2 ≤ 0 → G.inner p = g₀.cylinder.inner p

  A concordance from g₀ is g₀ + dt² where t ≤ 0.

• inner_of_one_le (p : M × ℝ) : 1 ≤ p.2 → G.inner p = g₁.cylinder.inner p

  A concordance to g₁ is g₁ + dt² where t ≥ 1.

def Bundle.ContMDiffRiemannianMetric.Concordant {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] [T2Space M] (g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) : Prop

Two metrics on M are concordant if there is a concordance from one to the other.

theorem Bundle.ContMDiffRiemannianMetric.concordant_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] [FiniteDimensional ℝ E] [T2Space M] (g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) : g₀.Concordant g₁ ↔ ∃ (G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p), G.IsConcordance g₀ g₁

Two metrics are concordant exactly when there is a concordance from one to the other.

theorem Bundle.ContMDiffRiemannianMetric.IsConcordance.concordant {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] [T2Space M] {G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : G.IsConcordance g₀ g₁) : g₀.Concordant g₁

The ends of a concordance are concordant.

theorem Bundle.ContMDiffRiemannianMetric.IsConcordance.hasPositiveScalarCurvature_left {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] [T2Space M] {G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : G.IsConcordance g₀ g₁) : g₀.HasPositiveScalarCurvature

The metric at the start of a concordance has positive scalar curvature.

theorem Bundle.ContMDiffRiemannianMetric.IsConcordance.hasPositiveScalarCurvature_right {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] [T2Space M] {G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : G.IsConcordance g₀ g₁) : g₁.HasPositiveScalarCurvature

The metric at the end of a concordance has positive scalar curvature.

theorem Bundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature.isConcordance_cylinder {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] [T2Space M] {g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : g.HasPositiveScalarCurvature) : g.cylinder.IsConcordance g g

The cylinder metric g + dt² of a metric of positive scalar curvature is a concordance from g to itself.

theorem Bundle.ContMDiffRiemannianMetric.concordant_self_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] [FiniteDimensional ℝ E] [T2Space M] {g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} : g.Concordant g ↔ g.HasPositiveScalarCurvature

A metric is concordant to itself exactly when it has positive scalar curvature.

theorem Bundle.ContMDiffRiemannianMetric.IsConcordance.reparamTime_one_sub {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] [T2Space M] {G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : G.IsConcordance g₀ g₁) : (G.reparamTime ⋯ ⋯).IsConcordance g₁ g₀

Reversing the ℝ-coordinate by t ↦ 1 - t turns a concordance from g₀ to g₁ into a concordance from g₁ to g₀.

theorem Bundle.ContMDiffRiemannianMetric.Concordant.symm {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] [T2Space M] {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : g₀.Concordant g₁) : g₁.Concordant g₀

Concordance is symmetric.

theorem Bundle.ContMDiffRiemannianMetric.concordant_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] [FiniteDimensional ℝ E] [T2Space M] {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} : g₀.Concordant g₁ ↔ g₁.Concordant g₀

Concordance is a symmetric relation.

theorem Bundle.ContMDiffRiemannianMetric.concordant_of_inner_eq_cylinder {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] [T2Space M] {G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (hG : G.HasPositiveScalarCurvature) {a b : ℝ} (h₀ : ∀ (p : M × ℝ), p.2 ≤ a → G.inner p = g₀.cylinder.inner p) (h₁ : ∀ (p : M × ℝ), b ≤ p.2 → G.inner p = g₁.cylinder.inner p) : g₀.Concordant g₁

If a metric of positive scalar curvature on M × ℝ is g₀ + dt² where t ≤ a and g₁ + dt² where t ≥ b, then g₀ and g₁ are concordant, whatever the window [a, b].

theorem Bundle.ContMDiffRiemannianMetric.Concordant.trans {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] [T2Space M] {g₀ g₁ g₂ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h₁ : g₀.Concordant g₁) (h₂ : g₁.Concordant g₂) : g₀.Concordant g₂

Concatenation of concordances: concordance is transitive. Translate a concordance from g₁ to g₂ to the window [2, 3], glue it to a concordance from g₀ to g₁ along 1 < t < 2, where both are g₁ + dt², and compress the window [0, 3] into [0, 1].

theorem Bundle.ContMDiffRiemannianMetric.equivalence_concordant {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] [T2Space M] : Equivalence fun (g₀ g₁ : { g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x // g.HasPositiveScalarCurvature }) => (↑g₀).Concordant ↑g₁

Concordance is an equivalence relation on the metrics of positive scalar curvature on M.

Collared concordances on M × [0, 1]

The time map used to extend a collared concordance by product ends.

structure Bundle.ContMDiffRiemannianMetric.IsCollaredConcordance {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] [T2Space M] (Gc : ContMDiffRiemannianMetric (I.prod (modelWithCornersEuclideanHalfSpace 1)) (↑⊤) (E × EuclideanSpace ℝ (Fin 1)) fun (p : M × ↑unitInterval) => TangentSpace (I.prod (modelWithCornersEuclideanHalfSpace 1)) p) (g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) : Prop

A collared concordance from g₀ to g₁ is a metric of positive scalar curvature on the manifold with boundary M × [0, 1] with product collars: for some ε > 0 it is the product metric g₀ + dt² where t < ε and the product metric g₁ + dt² where t > 1 - ε. Here g + dt² on M × [0, 1] is the restriction of the cylinder metric.

• hasPositiveScalarCurvature : Gc.HasPositiveScalarCurvature

  A collared concordance has positive scalar curvature.

• exists_collar : ∃ (ε : ℝ), 0 < ε ∧ (∀ (p : M × ↑unitInterval), ↑p.2 < ε → Gc.inner p = (restrictIcc 0 1 g₀.cylinder).inner p) ∧ ∀ (p : M × ↑unitInterval), 1 - ε < ↑p.2 → Gc.inner p = (restrictIcc 0 1 g₁.cylinder).inner p

  A collared concordance is g₀ + dt² where t < ε and g₁ + dt² where t > 1 - ε.

theorem Bundle.ContMDiffRiemannianMetric.IsCollaredConcordance.hasPositiveScalarCurvature_left {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] [T2Space M] {Gc : ContMDiffRiemannianMetric (I.prod (modelWithCornersEuclideanHalfSpace 1)) (↑⊤) (E × EuclideanSpace ℝ (Fin 1)) fun (p : M × ↑unitInterval) => TangentSpace (I.prod (modelWithCornersEuclideanHalfSpace 1)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : Gc.IsCollaredConcordance g₀ g₁) : g₀.HasPositiveScalarCurvature

The metric at the start of a collared concordance has positive scalar curvature.

theorem Bundle.ContMDiffRiemannianMetric.IsCollaredConcordance.hasPositiveScalarCurvature_right {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] [T2Space M] {Gc : ContMDiffRiemannianMetric (I.prod (modelWithCornersEuclideanHalfSpace 1)) (↑⊤) (E × EuclideanSpace ℝ (Fin 1)) fun (p : M × ↑unitInterval) => TangentSpace (I.prod (modelWithCornersEuclideanHalfSpace 1)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : Gc.IsCollaredConcordance g₀ g₁) : g₁.HasPositiveScalarCurvature

The metric at the end of a collared concordance has positive scalar curvature.

theorem Bundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature.isCollaredConcordance_restrictIcc_cylinder {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] [T2Space M] {g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : g.HasPositiveScalarCurvature) : (ContMDiffRiemannianMetric.restrictIcc 0 1 g.cylinder).IsCollaredConcordance g g

The product metric g + dt² on M × [0, 1] of a metric of positive scalar curvature is a collared concordance from g to itself.

theorem Bundle.ContMDiffRiemannianMetric.IsConcordance.exists_isCollaredConcordance {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] [T2Space M] {G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : G.IsConcordance g₀ g₁) : ∃ (Gc : ContMDiffRiemannianMetric (I.prod (modelWithCornersEuclideanHalfSpace 1)) (↑⊤) (E × EuclideanSpace ℝ (Fin 1)) fun (p : M × ↑unitInterval) => TangentSpace (I.prod (modelWithCornersEuclideanHalfSpace 1)) p), Gc.IsCollaredConcordance g₀ g₁

Concordances give collared concordances. A concordance from g₀ to g₁ gives a collared concordance from g₀ to g₁ on M × [0, 1].

theorem Bundle.ContMDiffRiemannianMetric.IsCollaredConcordance.concordant {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] [T2Space M] {Gc : ContMDiffRiemannianMetric (I.prod (modelWithCornersEuclideanHalfSpace 1)) (↑⊤) (E × EuclideanSpace ℝ (Fin 1)) fun (p : M × ↑unitInterval) => TangentSpace (I.prod (modelWithCornersEuclideanHalfSpace 1)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (h : Gc.IsCollaredConcordance g₀ g₁) : g₀.Concordant g₁

Collared concordances give concordances. If there is a collared concordance from g₀ to g₁, then g₀ and g₁ are concordant.

theorem Bundle.ContMDiffRiemannianMetric.concordant_iff_exists_isCollaredConcordance {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] [T2Space M] {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} : g₀.Concordant g₁ ↔ ∃ (Gc : ContMDiffRiemannianMetric (I.prod (modelWithCornersEuclideanHalfSpace 1)) (↑⊤) (E × EuclideanSpace ℝ (Fin 1)) fun (p : M × ↑unitInterval) => TangentSpace (I.prod (modelWithCornersEuclideanHalfSpace 1)) p), Gc.IsCollaredConcordance g₀ g₁

Two metrics are concordant exactly when there is a collared concordance from one to the other.

Pullback and rescaling of concordances

theorem Bundle.ContMDiffRiemannianMetric.pullback_prodMap_cylinder {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] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {f : M' → M} (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hf : ContMDiff I' I (↑⊤ + 1) f) (hinj : ∀ (x : M'), Function.Injective ⇑(mfderiv% f x)) (hinj' : ∀ (p : M' × ℝ), Function.Injective ⇑(mfderiv% (Prod.map f id) p)) : g.cylinder.pullback (Prod.map f id) ⋯ hinj' = (g.pullback f hf hinj).cylinder

The cylinder metric g + dt² pulled back along (x, t) ↦ (f x, t) is the cylinder metric f^* g + dt² of the pullback of g.

theorem Bundle.ContMDiffRiemannianMetric.IsConcordance.pullback_prodMap {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] [T2Space M] {G : ContMDiffRiemannianMetric (I.prod (modelWithCornersSelf ℝ ℝ)) (↑⊤) (E × ℝ) fun (p : M × ℝ) => TangentSpace (I.prod (modelWithCornersSelf ℝ ℝ)) p} {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [T2Space M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {f : M' → M} (h : G.IsConcordance g₀ g₁) (hf : ContMDiff I' I (↑⊤ + 1) f) (hinv : ∀ (x : M'), (mfderiv% f x).IsInvertible) : (G.pullback (Prod.map f id) ⋯ ⋯).IsConcordance (g₀.pullback f hf ⋯) (g₁.pullback f hf ⋯)

Pulling a concordance from g₀ to g₁ back along (x, t) ↦ (f x, t), for a smooth map f whose differential is invertible at every point, gives a concordance from f^* g₀ to f^* g₁.

theorem Bundle.ContMDiffRiemannianMetric.Concordant.pullback {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] [T2Space M] {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [T2Space M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] {f : M' → M} (h : g₀.Concordant g₁) (hf : ContMDiff I' I (↑⊤ + 1) f) (hinv : ∀ (x : M'), (mfderiv% f x).IsInvertible) : (g₀.pullback f hf ⋯).Concordant (g₁.pullback f hf ⋯)

Naturality of concordance. If g₀ and g₁ are concordant, then so are their pullbacks along a smooth map whose differential is invertible at every point, such as a diffeomorphism or a covering map.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.concordant_pullback_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] [FiniteDimensional ℝ E] [T2Space M] {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type u_6} [TopologicalSpace M'] [T2Space M'] [ChartedSpace H' M'] [IsManifold I' (↑⊤) M'] (Φ : Diffeomorph I' I M' M ↑⊤) (hf : ContMDiff I' I (↑⊤ + 1) ⇑Φ) (hinj : ∀ (x : M'), Function.Injective ⇑(mfderiv% ⇑Φ x)) : (g₀.pullback (⇑Φ) hf hinj).Concordant (g₁.pullback (⇑Φ) hf hinj) ↔ g₀.Concordant g₁

Two metrics are concordant exactly when their pullbacks along a diffeomorphism are.

theorem Bundle.ContMDiffRiemannianMetric.reparamTime_rescale_cylinder {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] {c : ℝ} (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hc : 0 < c) : (g.cylinder.rescale (fun (x : M × ℝ) => c) ⋯ ⋯).reparamTime ⋯ ⋯ = (g.rescale (fun (x : M) => c) ⋯ ⋯).cylinder

The cylinder metric c g + dt² of a rescaled metric is the rescaled cylinder metric c (g + dt²) reparametrised by t ↦ t / √c.

theorem Bundle.ContMDiffRiemannianMetric.Concordant.rescale_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] [FiniteDimensional ℝ E] [T2Space M] {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} {c : ℝ} (h : g₀.Concordant g₁) (hc : 0 < c) : (g₀.rescale (fun (x : M) => c) ⋯ ⋯).Concordant (g₁.rescale (fun (x : M) => c) ⋯ ⋯)

If g₀ and g₁ are concordant, then so are c g₀ and c g₁ for every constant c > 0.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.concordant_rescale_const_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] [FiniteDimensional ℝ E] [T2Space M] {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} {c : ℝ} (hc : 0 < c) : (g₀.rescale (fun (x : M) => c) ⋯ ⋯).Concordant (g₁.rescale (fun (x : M) => c) ⋯ ⋯) ↔ g₀.Concordant g₁

Rescaling by a positive constant preserves and reflects concordance.

theorem Bundle.ContMDiffRiemannianMetric.Concordant.prodTangentSpace_of_nonneg {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] [T2Space M] {g₀ g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {H'' : Type u_5} [TopologicalSpace H''] {J : ModelWithCorners ℝ F H''} {N : Type u_6} [TopologicalSpace N] [T2Space N] [ChartedSpace H'' N] [IsManifold J (↑⊤) N] (h : g₀.Concordant g₁) {g₂ : ContMDiffRiemannianMetric J (↑⊤) F fun (y : N) => TangentSpace J y} (h₂ : ∀ (y : N), 0 ≤ g₂.scalarCurvature y) : (g₀.prodTangentSpace g₂).Concordant (g₁.prodTangentSpace g₂)

Products of concordances. If g₀ and g₁ are concordant and g₂ has nonnegative scalar curvature, then g₀ × g₂ and g₁ × g₂ are concordant.