Curvature, Jacobi fields, submanifolds, and Bochner geometry

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

TheoremThe second Bianchi identity#

Let ∇ be a smooth connection on a vector bundle and ∇ᵀ a smooth torsion-free connection on the tangent bundle. Writing (∇_X R)(Y, Z) σ = ∇_X (R(Y, Z) σ) - R(∇ᵀ_X Y, Z) σ - R(Y, ∇ᵀ_X Z) σ - R(Y, Z) (∇_X σ), the cyclic sum (∇_X R)(Y, Z) σ + (∇_Y R)(Z, X) σ + (∇_Z R)(X, Y) σ vanishes.

CovariantDerivative.covariantDerivative_curvatureOperator_cyclic_eq_zero.{u_1, u_2, u_3, u_4, u_5}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {H : Type u_2}
  [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F]
  {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)]
  [(x : M) → _root_.Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)]
  [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V]
  [VectorBundle ℝ F V] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤]
  {X Y Z : (x : M) → TangentSpace I x} {σ : (x : M) → V x}
  (covT : CovariantDerivative I E (TangentSpace I)) [covT.ContMDiffCovariantDerivative ↑⊤]
  (ht : covT.IsTorsionFree) (hX : ContMDiff I I.tangent ↑⊤ fun x => ⟨x, X x⟩)
  (hY : ContMDiff I I.tangent ↑⊤ fun x => ⟨x, Y x⟩)
  (hZ : ContMDiff I I.tangent ↑⊤ fun x => ⟨x, Z x⟩)
  (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun x => ⟨x, σ x⟩) (x : M) :
  (↑cov (cov.curvatureOperator Y Z σ) x) (X x) -
              cov.curvatureOperator (fun y => (↑covT Y y) (X y)) Z σ x -
            cov.curvatureOperator Y (fun y => (↑covT Z y) (X y)) σ x -
          cov.curvatureOperator Y Z (fun y => (↑cov σ y) (X y)) x +
        ((↑cov (cov.curvatureOperator Z X σ) x) (Y x) -
              cov.curvatureOperator (fun y => (↑covT Z y) (Y y)) X σ x -
            cov.curvatureOperator Z (fun y => (↑covT X y) (Y y)) σ x -
          cov.curvatureOperator Z X (fun y => (↑cov σ y) (Y y)) x) +
      ((↑cov (cov.curvatureOperator X Y σ) x) (Z x) -
            cov.curvatureOperator (fun y => (↑covT X y) (Z y)) Y σ x -
          cov.curvatureOperator X (fun y => (↑covT Y y) (Z y)) σ x -
        cov.curvatureOperator X Y (fun y => (↑cov σ y) (Z y)) x) =
    0
Lean

Formalized in Tau Ceti as CovariantDerivative.covariantDerivative_curvatureOperator_cyclic_eq_zero.

Other forms

The second Bianchi identity, pointwise. Formalized in Tau Ceti as CovariantDerivative.derivCurvatureTensor_cyclic_eq_zero.

CovariantDerivative.derivCurvatureTensor_cyclic_eq_zero.{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} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F]
  [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5}
  [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)]
  [(x : M) → _root_.Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)]
  [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V]
  [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V)
  [cov.ContMDiffCovariantDerivative ↑⊤] (covT : CovariantDerivative I E (TangentSpace I))
  [covT.ContMDiffCovariantDerivative ↑⊤] (ht : covT.torsion = 0) (x : M)
  (u v w : TangentSpace I x) :
  (((cov.derivCurvatureTensor covT x) u) v) w + (((cov.derivCurvatureTensor covT x) v) w) u +
      (((cov.derivCurvatureTensor covT x) w) u) v =
    0

The second Bianchi identity with torsion. Formalized in Tau Ceti as CovariantDerivative.derivCurvatureTensor_cyclic_eq_neg_torsion.

CovariantDerivative.derivCurvatureTensor_cyclic_eq_neg_torsion.{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} {M : Type u_3} [TopologicalSpace M]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F]
  [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5}
  [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)]
  [(x : M) → _root_.Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)]
  [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V]
  [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V)
  [cov.ContMDiffCovariantDerivative ↑⊤] (covT : CovariantDerivative I E (TangentSpace I)) (x : M)
  (u v w : TangentSpace I x) :
  (((cov.derivCurvatureTensor covT x) u) v) w + (((cov.derivCurvatureTensor covT x) v) w) u +
      (((cov.derivCurvatureTensor covT x) w) u) v =
    -(((cov.curvatureTensor x) (((covT.torsion x) u) v)) w +
          ((cov.curvatureTensor x) (((covT.torsion x) v) w)) u +
        ((cov.curvatureTensor x) (((covT.torsion x) w) u)) v)
Sources
LeanCovariantDerivative.covariantDerivative_curvatureOperator_cyclic_eq_zero · CovariantDerivative.derivCurvatureTensor_cyclic_eq_zero · CovariantDerivative.derivCurvatureTensor_cyclic_eq_neg_torsion
Uses 1 · Used by 3
Proof usesVectorField.jacobi_identity_mlieBracket_apply
Used byEinstein's constancy theorem · Schur's theorem (CovariantDerivative.eq_of_forall_hasSectionalCurvatureAt) · Weyl–Schouten in dimension three, on a model space

TheoremCovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_of_forall_linearIndependent#

For a metric-compatible torsion-free connection, the Riemann curvature tensor at x is the only quadrilinear form with the algebraic symmetries of a curvature tensor whose values T(u, v, v, u) on linearly independent pairs are the sectional-curvature numerators ⟨R(u, v)v, u⟩.

CovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_of_forall_linearIndependent.{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]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle (TangentSpace I)]
  {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤]
  [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible)
  (ht : cov.torsion = 0) (x : M)
  {T :
    TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] ℝ}
  (h₁ : ∀ (u v w z : TangentSpace I x), (((T u) v) w) z = -(((T v) u) w) z)
  (h₂ : ∀ (u v w z : TangentSpace I x), (((T u) v) w) z = -(((T u) v) z) w)
  (h₃ : ∀ (u v w z : TangentSpace I x), (((T u) v) w) z + (((T v) w) u) z + (((T w) u) v) z = 0)
  (hT :
    ∀ (u v : TangentSpace I x),
      LinearIndependent ℝ ![u, v] →
        ((((cov.riemannCurvatureTensor x) u) v) v) u = (((T u) v) v) u) :
  cov.riemannCurvatureTensor x = T
Lean

Formalized in Tau Ceti as CovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_of_forall_linearIndependent.

Sources
LeanCovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_of_forall_linearIndependent
Uses 1 · Used by 2
Proof usesLinearMap.six_mul_apply_eq_of_cyclic_eq_zero
Used byCovariantDerivative.hasConstantSectionalCurvature_iff_isConstantCurvatureTensor · Schur's theorem (CovariantDerivative.eq_of_forall_hasSectionalCurvatureAt)

TheoremCovariantDerivative.hasConstantSectionalCurvature_iff_isConstantCurvatureTensor#

A metric-compatible torsion-free connection has constant sectional curvature κ if and only if its curvature tensor is the constant-curvature tensor R(w, u)v = κ (⟨u, v⟩ w - ⟨w, v⟩ u) at every point. Applied to the Levi-Civita connection, this identifies constant sectional curvature of a Riemannian manifold with the constant-curvature equation.

CovariantDerivative.hasConstantSectionalCurvature_iff_isConstantCurvatureTensor.{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]
  [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M]
  [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsContMDiffRiemannianBundle I 2 E fun x => TangentSpace I x]
  (cov : CovariantDerivative I E fun x => TangentSpace I x) [cov.ContMDiffCovariantDerivative ↑⊤]
  (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (κ : ℝ) :
  cov.HasConstantSectionalCurvature hcov κ ↔
    Bundle.RiemannianBundle.g.IsConstantCurvatureTensor cov ⋯ κ
Lean

Formalized in Tau Ceti as CovariantDerivative.hasConstantSectionalCurvature_iff_isConstantCurvatureTensor.

Sources
LeanCovariantDerivative.hasConstantSectionalCurvature_iff_isConstantCurvatureTensor
Uses 1
Proof usesCovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_of_forall_linearIndependent

TheoremCurvature under conformal change#

Let ∇ be a Levi-Civita connection of a C¹ metric g and A the conformal connection tensor of a positive function f. Then the curvature of the Levi-Civita connection of f g is

R^(f g)(X, Y) Z = R^∇(X, Y) Z + (∇_X A)(Z, Y) - (∇_Y A)(Z, X) + A(A(Z, Y), X) - A(A(Z, X), Y),

with (∇_X A)(Z, Y) = ∇_X (A(Z, Y)) - A(∇_X Z, Y) - A(Z, ∇_X Y). The metric g and the function f are assumed Cⁿ on all of M for some 1 ≤ n, and Z differentiable on all of M; the remaining hypotheses are differentiability at x of X, Y, ∇_X Z, ∇_Y Z, A(Z, X) and A(Z, Y).

Bundle.ContMDiffRiemannianMetric.curvatureOperator_leviCivitaConnection_rescale.{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]
  [ChartedSpace H M] [IsManifold I 2 M] {n : WithTop ℕ∞}
  (g : Bundle.ContMDiffRiemannianMetric I n E fun x => TangentSpace I x) (hn : 1 ≤ n) {f : M → ℝ}
  (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) (hf_pos : ∀ (x : M), 0 < f x)
  {cov : CovariantDerivative I E fun x => TangentSpace I x}
  (hcov : CovariantDerivative.IsLeviCivitaConnection I cov) {X Y Z : (x : M) → TangentSpace I x}
  {x : M} (hX : (MDiffAt fun x => ⟨x, X x⟩) x) (hY : (MDiffAt fun x => ⟨x, Y x⟩) x)
  (hZ : MDiff fun x => ⟨x, Z x⟩) (hXZ : (MDiffAt fun y => ⟨y, (↑cov Z y) (X y)⟩) x)
  (hYZ : (MDiffAt fun y => ⟨y, (↑cov Z y) (Y y)⟩) x)
  (hAX : (MDiffAt fun y => ⟨y, ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (X y)⟩) x)
  (hAY :
    (MDiffAt fun y => ⟨y, ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (Y y)⟩) x) :
  (CovariantDerivative.leviCivitaConnection I M).curvatureOperator X Y Z x =
    cov.curvatureOperator X Y Z x +
          ((↑cov (fun y => ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (Y y)) x)
                (X x) -
              ((TauCeti.Manifold.conformalConnectionTensor I f x) ((↑cov Z x) (X x))) (Y x) -
            ((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) ((↑cov Y x) (X x))) -
        ((↑cov (fun y => ((TauCeti.Manifold.conformalConnectionTensor I f y) (Z y)) (X y)) x)
              (Y x) -
            ((TauCeti.Manifold.conformalConnectionTensor I f x) ((↑cov Z x) (Y x))) (X x) -
          ((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) ((↑cov X x) (Y x))) +
      (((TauCeti.Manifold.conformalConnectionTensor I f x)
            (((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) (Y x)))
          (X x) -
        ((TauCeti.Manifold.conformalConnectionTensor I f x)
            (((TauCeti.Manifold.conformalConnectionTensor I f x) (Z x)) (X x)))
          (Y x))
Lean

Formalized in Tau Ceti as Bundle.ContMDiffRiemannianMetric.curvatureOperator_leviCivitaConnection_rescale.

Sources
LeanBundle.ContMDiffRiemannianMetric.curvatureOperator_leviCivitaConnection_rescale
Uses 1 · Used by 3
Proof usesCurvature of a connection plus a one-form
Used byScalar curvature of a conformal metric · Weyl–Schouten in dimension three, on a model space · Weyl tensor under conformal change

TheoremCurvature of a connection plus a one-form#

If A is a one-form with values in the endomorphisms of V, then

R^(∇ + A)(X, Y) σ = R^∇(X, Y) σ + (∇_X (A(σ, Y)) - ∇_Y (A(σ, X)) - A(σ, [X, Y])) + (A(∇_Y σ, X) - A(∇_X σ, Y)) + (A(A(σ, Y), X) - A(A(σ, X), Y)),

where A(σ, X) = A x (σ x) (X x). The hypotheses are the differentiability at the point of the four sections differentiated by the outer covariant derivatives.

CovariantDerivative.curvatureOperator_addOneForm.{u_1, u_2, u_3, u_4, u_5, u_6} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3}
  [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M]
  [ChartedSpace H M] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : M → Type u_6}
  [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)]
  [(x : M) → _root_.Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)]
  [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [FiberBundle F V]
  (cov : CovariantDerivative I F V) (A : (x : M) → V x →L[𝕜] TangentSpace I x →L[𝕜] V x)
  {X Y : (x : M) → TangentSpace I x} {σ : (x : M) → V x} {x : M}
  (hXσ : (MDiffAt fun y => ⟨y, (↑cov σ y) (X y)⟩) x)
  (hYσ : (MDiffAt fun y => ⟨y, (↑cov σ y) (Y y)⟩) x)
  (hAX : (MDiffAt fun y => ⟨y, ((A y) (σ y)) (X y)⟩) x)
  (hAY : (MDiffAt fun y => ⟨y, ((A y) (σ y)) (Y y)⟩) x) :
  (cov.addOneForm A).curvatureOperator X Y σ x =
    cov.curvatureOperator X Y σ x +
          ((↑cov (fun y => ((A y) (σ y)) (Y y)) x) (X x) -
              (↑cov (fun y => ((A y) (σ y)) (X y)) x) (Y x) -
            ((A x) (σ x)) (VectorField.mlieBracket I X Y x)) +
        (((A x) ((↑cov σ x) (Y x))) (X x) - ((A x) ((↑cov σ x) (X x))) (Y x)) +
      (((A x) (((A x) (σ x)) (Y x))) (X x) - ((A x) (((A x) (σ x)) (X x))) (Y x))
Lean

Formalized in Tau Ceti as CovariantDerivative.curvatureOperator_addOneForm.

Sources
LeanCovariantDerivative.curvatureOperator_addOneForm
Used by 1
Used byCurvature under conformal change

TheoremLinearMap.six_mul_apply_eq_of_cyclic_eq_zero#

The polarization identity for curvature-type tensors: for a quadrilinear form T antisymmetric in its first and in its last pair of arguments and satisfying the first Bianchi identity, 6 T(x, y, z, w) is an explicit combination of values T(a, b, b, a). This recovers T itself only when multiplication by 6 is injective, see LinearMap.eq_of_cyclic_eq_zero.

LinearMap.six_mul_apply_eq_of_cyclic_eq_zero.{u_1, u_2} {R : Type u_1} {M : Type u_2} [CommRing R]
  [AddCommGroup M] [_root_.Module R M] {T : M →ₗ[R] M →ₗ[R] M →ₗ[R] M →ₗ[R] R}
  (h₁ : ∀ (x y z w : M), (((T x) y) z) w = -(((T y) x) z) w)
  (h₂ : ∀ (x y z w : M), (((T x) y) z) w = -(((T x) y) w) z)
  (h₃ : ∀ (x y z w : M), (((T x) y) z) w + (((T y) z) x) w + (((T z) x) y) w = 0) (x y z w : M) :
  6 * (((T x) y) z) w =
    (((T (x + w)) (y + z)) (y + z)) (x + w) - (((T (x + z)) (y + w)) (y + w)) (x + z) -
                            (((T x) (y + z)) (y + z)) x -
                          (((T w) (y + z)) (y + z)) w +
                        (((T x) (y + w)) (y + w)) x +
                      (((T z) (y + w)) (y + w)) z -
                    (((T (x + w)) y) y) (x + w) +
                  (((T (x + z)) y) y) (x + z) -
                (((T (x + w)) z) z) (x + w) +
              (((T (x + z)) w) w) (x + z) +
            (((T w) y) y) w -
          (((T z) y) y) z +
        (((T x) z) z) x -
      (((T x) w) w) x
Lean

Formalized in Tau Ceti as LinearMap.six_mul_apply_eq_of_cyclic_eq_zero.

Sources
LeanLinearMap.six_mul_apply_eq_of_cyclic_eq_zero
Used by 1
Used byCovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_of_forall_linearIndependent

TheoremVectorField.jacobi_identity_mlieBracket_apply#

The Jacobi identity for the manifold Lie bracket, in cyclic form: [U, [V, W]] + [V, [W, U]] + [W, [U, V]] = 0. This rearranges Mathlib's Leibniz form leibniz_identity_mlieBracket_apply.

VectorField.jacobi_identity_mlieBracket_apply.{u_1, u_2, u_4, u_5} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [CompleteSpace E] {H : Type u_4} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_5}
  [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 3) M]
  {U V W : (y : M) → TangentSpace I y} {x : M}
  (hU : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun y => ⟨y, U y⟩) x)
  (hV : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun y => ⟨y, V y⟩) x)
  (hW : ContMDiffAt I I.tangent (minSmoothness 𝕜 2) (fun y => ⟨y, W y⟩) x) :
  VectorField.mlieBracket I U (VectorField.mlieBracket I V W) x +
        VectorField.mlieBracket I V (VectorField.mlieBracket I W U) x +
      VectorField.mlieBracket I W (VectorField.mlieBracket I U V) x =
    0
Lean

Formalized in Tau Ceti as VectorField.jacobi_identity_mlieBracket_apply.

Sources
LeanVectorField.jacobi_identity_mlieBracket_apply
Used by 1
Used byThe second Bianchi identity

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.