Positive scalar curvature, surgery and bordism

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremBundle.ContMDiffRiemannianMetric.equivalence_concordant#

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

Bundle.ContMDiffRiemannianMetric.equivalence_concordant.{u_1, u_2, u_3} {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₀).Concordant ↑g₁
Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.equivalence_concordant.

Sources
LeanBundle.ContMDiffRiemannianMetric.equivalence_concordant
Uses 3
Statement usesBundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature
Proof usesThe Koszul formula · The scalar curvature of a product metric

TheoremBundle.ContMDiffRiemannianMetric.concordant_iff_exists_isCollaredConcordance#

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

Bundle.ContMDiffRiemannianMetric.concordant_iff_exists_isCollaredConcordance.{u_1, u_2, u_3}
  {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₁ : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => TangentSpace I x} :
  g₀.Concordant g₁ ↔ ∃ Gc, Gc.IsCollaredConcordance g₀ g₁
Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.concordant_iff_exists_isCollaredConcordance.

Sources
LeanBundle.ContMDiffRiemannianMetric.concordant_iff_exists_isCollaredConcordance
Uses 3
Statement usesBundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature
Proof usesThe Koszul formula · The scalar curvature of a product metric

TheoremCompact 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.

TauCeti.Manifold.exists_pos_forall_le_scalarCurvature.{u_1, u_2, u_3, u_4, u_5} {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 => TangentSpace I x)
  {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ E) [CompactSpace P]
  [CompactSpace M]
  (h₀ :
    ∀ (p : P) (x : M),
      ContinuousAt
        (fun r =>
          (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 k i j =>
          (fderiv ℝ (fun z => (((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 m k i j =>
          (fderiv ℝ
              (fun z =>
                (fderiv ℝ (fun z' => (((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
Lean

Formalized in Tau Ceti as TauCeti.Manifold.exists_pos_forall_le_scalarCurvature.

Sources
LeanTauCeti.Manifold.exists_pos_forall_le_scalarCurvature
Uses 4
Statement usesBundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature
Proof usesThe Koszul formula · Scalar curvature is continuous in the second-order jet of the metric · TauCeti.Manifold.scalarCurvatureOfJet

TheoremThe scalar curvature of a product metric#

The scalar curvature of a product metric g₁ × g₂ is the sum of the scalar curvatures of the factors: Scal(x, y) = Scal_{g₁}(x) + Scal_{g₂}(y).

Bundle.ContMDiffRiemannianMetric.scalarCurvature_prodTangentSpace.{u_1, u_2, u_3, u_4, u_5, u_6}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [T2Space M]
  [ChartedSpace H M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F]
  [FiniteDimensional ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G}
  {N : Type u_6} [TopologicalSpace N] [T2Space N] [ChartedSpace G N] [IsManifold J (↑⊤) N]
  (g₁ : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => TangentSpace I x)
  (g₂ : Bundle.ContMDiffRiemannianMetric J (↑⊤) F fun y => TangentSpace J y) (p : M × N) :
  (g₁.prodTangentSpace g₂).scalarCurvature p = g₁.scalarCurvature p.1 + g₂.scalarCurvature p.2
Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.scalarCurvature_prodTangentSpace.

Sources
LeanBundle.ContMDiffRiemannianMetric.scalarCurvature_prodTangentSpace
Uses 1 · Used by 3
Proof usesThe Koszul formula
Used byBundle.ContMDiffRiemannianMetric.concordant_iff_exists_isCollaredConcordance · Bundle.ContMDiffRiemannianMetric.equivalence_concordant · Shrinking a compact factor of positive scalar curvature

TheoremShrinking a compact factor of positive scalar curvature#

Let g₂ be a metric of positive scalar curvature on a compact manifold N, and let g be a metric whose scalar curvature is bounded below. Then there is ε > 0 such that g × c g₂ has positive scalar curvature for every 0 < c < ε.

Bundle.ContMDiffRiemannianMetric.exists_pos_hasPositiveScalarCurvature_prodTangentSpace_rescale.{u_1,
    u_2, u_3, u_4, u_5, u_6}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [T2Space M]
  [ChartedSpace H M] [IsManifold I (↑⊤) M]
  (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => 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]
  {g₂ : Bundle.ContMDiffRiemannianMetric J (↑⊤) F fun y => TangentSpace J y} [CompactSpace N]
  (h : BddBelow (Set.range g.scalarCurvature)) (h₂ : g₂.HasPositiveScalarCurvature) :
  ∃ ε,
    0 < ε ∧
      ∀ (c : ℝ) (hc : 0 < c),
        c < ε → (g.prodTangentSpace (g₂.rescale (fun x => c) ⋯ ⋯)).HasPositiveScalarCurvature
Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.exists_pos_hasPositiveScalarCurvature_prodTangentSpace_rescale.

Sources
LeanBundle.ContMDiffRiemannianMetric.exists_pos_hasPositiveScalarCurvature_prodTangentSpace_rescale
Uses 3
Statement usesBundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature
Proof usesThe Koszul formula · The scalar curvature of a product metric

TheoremScalar curvature of the round sphere#

The round n-sphere of radius r has scalar curvature n (n - 1) / r².

TauCeti.scalarCurvature_sphereRoundMetricOfRadius.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] {r : ℝ} (hr : 0 < r)
  (p : ↑(Metric.sphere 0 1)) :
  (TauCeti.sphereRoundMetricOfRadius r hr).scalarCurvature p = ↑n * (↑n - 1) / r ^ 2
Lean

Formalized in Tau Ceti as TauCeti.scalarCurvature_sphereRoundMetricOfRadius.

Sources
LeanTauCeti.scalarCurvature_sphereRoundMetricOfRadius
Uses 2
Proof usesThe Gauss formula · The Koszul formula

DefinitionBundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature#

A smooth Riemannian metric has positive scalar curvature if its scalar curvature is positive at every point.

Bundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [T2Space M]
  [ChartedSpace H M] [IsManifold I (↑⊤) M]
  (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun x => TangentSpace I x) : Prop
Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature.

Sources
LeanBundle.ContMDiffRiemannianMetric.HasPositiveScalarCurvature
Uses 1 · Used by 4
Proof usesThe Koszul formula
Used byBundle.ContMDiffRiemannianMetric.concordant_iff_exists_isCollaredConcordance · Bundle.ContMDiffRiemannianMetric.equivalence_concordant · Compact families of metrics of positive scalar curvature have a uniform scalar gap · Shrinking a compact factor of positive scalar curvature

DefinitionTauCeti.Manifold.scalarCurvatureOfJet#

The scalar curvature of a coordinate jet (g, ∂g, ∂²g): the contraction Σⱼₖ g^(jk) Σᵢ Rⁱᵢⱼₖ of the curvature coefficients riemannOfJet against the inverse of the Gram matrix g.

TauCeti.Manifold.scalarCurvatureOfJet.{u_1} {ι : Type u_1} [Fintype ι] [DecidableEq ι]
  (g : Matrix ι ι ℝ) (dg : ι → ι → ι → ℝ) (ddg : ι → ι → ι → ι → ℝ) : ℝ
Lean

Formalized in Tau Ceti as TauCeti.Manifold.scalarCurvatureOfJet.

Sources
LeanTauCeti.Manifold.scalarCurvatureOfJet
Used by 2
Used byCompact families of metrics of positive scalar curvature have a uniform scalar gap · Scalar curvature is continuous in the second-order jet of the metric

TheoremScalar curvature is continuous in the second-order jet of the metric#

The scalar curvature of a coordinate jet depends continuously on the jet at every jet whose Gram matrix is invertible.

ContinuousAt.scalarCurvatureOfJet.{u_1, u_2} {ι : Type u_1} [Fintype ι] [DecidableEq ι]
  {X : Type u_2} [TopologicalSpace X] {g : X → Matrix ι ι ℝ} {dg : X → ι → ι → ι → ℝ}
  {ddg : X → ι → ι → ι → ι → ℝ} {x : X} (hg : ContinuousAt g x) (hdet : (g x).det ≠ 0)
  (hdg : ContinuousAt dg x) (hddg : ContinuousAt ddg x) :
  ContinuousAt (fun y => TauCeti.Manifold.scalarCurvatureOfJet (g y) (dg y) (ddg y)) x
Lean

Formalized in Tau Ceti as ContinuousAt.scalarCurvatureOfJet.

Sources
LeanContinuousAt.scalarCurvatureOfJet
Uses 1 · Used by 1
Statement usesTauCeti.Manifold.scalarCurvatureOfJet
Used byCompact families of metrics of positive scalar curvature have a uniform scalar gap

DefinitionBundle.ContMDiffRiemannianMetric.positiveDefiniteSymmetricSectionEquiv#

Native finite-rank C^n metrics are exactly the positive-definite C^n sections of the bundle of symmetric bilinear forms.

Bundle.ContMDiffRiemannianMetric.positiveDefiniteSymmetricSectionEquiv.{u_1, u_2, u_3, u_4, u_5}
  {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB]
  {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B]
  [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_5}
  [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)]
  [(x : B) → AddCommGroup (V x)] [(x : B) → _root_.Module ℝ (V x)] [FiberBundle F V]
  [VectorBundle ℝ F V] [FiniteDimensional ℝ F] :
  Bundle.ContMDiffRiemannianMetric IB n F V ≃
    ↑(TauCeti.Manifold.positiveDefiniteSymmetricSections IB n F V)
Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.positiveDefiniteSymmetricSectionEquiv.

Sources
LeanBundle.ContMDiffRiemannianMetric.positiveDefiniteSymmetricSectionEquiv

TheoremContMDiffVectorBundle.symmetricBilinearMaps#

When two is invertible, the symmetric bilinear maps on the fibres of a C^n vector bundle form a C^n vector bundle.

ContMDiffVectorBundle.symmetricBilinearMaps.{u_1, u_2, u_3, u_4, u_5, u_6, u_7} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] [NeZero 2] {EB : Type u_2} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB]
  {HB : Type u_3} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} {B : Type u_4}
  [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {V : B → Type u_6} [(x : B) → AddCommGroup (V x)] [(x : B) → _root_.Module 𝕜 (V x)]
  [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [FiberBundle F V]
  [VectorBundle 𝕜 F V] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞}
  [ContMDiffVectorBundle n F V IB] :
  ContMDiffVectorBundle n (↥(TauCeti.symmetricBilinearMaps 𝕜 F G))
    (fun x => ↥(TauCeti.symmetricBilinearMaps 𝕜 (V x) G)) IB
Lean

Formalized in Tau Ceti as ContMDiffVectorBundle.symmetricBilinearMaps.

Sources
LeanContMDiffVectorBundle.symmetricBilinearMaps

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.