The second covariant derivative of a section #
Let ∇ be a smooth connection on a vector bundle V and ∇ᵀ a connection on the tangent
bundle. The second covariant derivative of a smooth section σ of V is the tensor
∇²σ(X, Y) = ∇_X (∇_Y σ) - ∇_{∇ᵀ_X Y} σ.
It is linear over functions in both X and Y, so at each point it is a bilinear map from pairs
of tangent vectors to the fibre. This file constructs it with globally smooth extensions of the
tangent vectors and the tensoriality criterion TauCeti.Manifold.eq_of_contMDiff_tensorial.
The Ricci identity, which expresses the antisymmetric part of ∇²σ through curvature and
torsion, is CovariantDerivative.secondCovariantDerivative_sub_swap, in the curvature module
Curvature/SecondCovariantDerivative.lean.
Main definitions and results #
CovariantDerivative.secondCovariantDerivative: the second covariant derivative∇²σat a point, as a bilinear map. It is zero whenσis not smooth.CovariantDerivative.secondCovariantDerivative_apply: its value on a smooth vector field in the second slot,∇²σ(u, Y) = ∇_u (∇_Y σ) - ∇_{∇ᵀ_u Y} σ.CovariantDerivative.eq_secondCovariantDerivative_iff: this value characterizes∇²σ.CovariantDerivative.covariantDerivative_covariantDerivative_smul_section: the Leibniz rule for the iterated covariant derivative of a function multiple of a section, for aC^kconnection with1 ≤ k.CovariantDerivative.secondCovariantDerivative_smul_apply: the Leibniz rule for the second covariant derivative of a function multiple of a section.CovariantDerivative.secondCovariantDerivative_smul_smul_sub: the double commutator of∇²with multiplication by two functionsf,gis(df ⊗ dg + dg ⊗ df) σ, independently of the connections.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 4 (the total covariant derivative and the second covariant derivative).
theorem
CovariantDerivative.covariantDerivative_covariantDerivative_smul_section
{𝕜 : 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]
[IsManifold I 1 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) → Module 𝕜 (V x)]
[(x : M) → TopologicalSpace (V x)]
[∀ (x : M), IsTopologicalAddGroup (V x)]
[∀ (x : M), ContinuousSMul 𝕜 (V x)]
[FiberBundle F V]
[VectorBundle 𝕜 F V]
{k : WithTop ℕ∞}
(hk : 1 ≤ k)
(cov : CovariantDerivative I F V)
[cov.ContMDiffCovariantDerivative k]
{f : M → 𝕜}
{X Y : (y : M) → TangentSpace I y}
{σ : (y : M) → V y}
(hf : ContMDiff I (modelWithCornersSelf 𝕜 𝕜) (k + 1) f)
(hY : ContMDiff I I.tangent k fun (y : M) => ⟨y, Y y⟩)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) (k + 1) fun (y : M) => ⟨y, σ y⟩)
(x : M)
:
Second covariant derivative of a function multiple. For a C^k connection with 1 ≤ k,
a vector field X, a C^k vector field Y, a C^(k + 1) function f and a C^(k + 1) section
σ,
∇_X ∇_Y (f σ) = f ∇_X ∇_Y σ + (X f) ∇_Y σ + (Y f) ∇_X σ + (X (Y f)) σ.
noncomputable def
CovariantDerivative.secondCovariantDerivative
{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]
{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) → 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 ↑⊤]
(covT : CovariantDerivative I E (TangentSpace I))
[FiniteDimensional ℝ E]
[T2Space M]
(σ : (y : M) → V y)
(x : M)
:
The second covariant derivative ∇²σ(u, v) = ∇_u (∇_Y σ) - ∇_{∇ᵀ_u Y} σ of a smooth section
σ at x, where Y is any smooth vector field with Y x = v. It is bilinear in (u, v), and
is defined to be zero when σ is not smooth.
Instances For
theorem
CovariantDerivative.secondCovariantDerivative_apply
{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]
{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) → 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 ↑⊤]
(covT : CovariantDerivative I E (TangentSpace I))
{σ : (y : M) → V y}
[FiniteDimensional ℝ E]
[T2Space M]
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩)
(x : M)
{Y : (y : M) → TangentSpace I y}
(hY : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, Y y⟩)
(u : TangentSpace I x)
:
((cov.secondCovariantDerivative covT σ x) u) (Y x) = (↑cov (fun (y : M) => (↑cov σ y) (Y y)) x) u - (↑cov σ x) ((↑covT Y x) u)
The second covariant derivative of a smooth section, evaluated on a smooth vector field in
its second slot: ∇²σ(u, Y) = ∇_u (∇_Y σ) - ∇_{∇ᵀ_u Y} σ.
@[simp]
theorem
CovariantDerivative.secondCovariantDerivative_of_not_contMDiff
{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]
{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) → 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 ↑⊤]
(covT : CovariantDerivative I E (TangentSpace I))
{σ : (y : M) → V y}
[FiniteDimensional ℝ E]
[T2Space M]
(hσ : ¬ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩)
(x : M)
:
The second covariant derivative of a section which is not smooth is zero.
theorem
CovariantDerivative.eq_secondCovariantDerivative_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]
{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) → 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 ↑⊤]
(covT : CovariantDerivative I E (TangentSpace I))
{σ : (y : M) → V y}
[FiniteDimensional ℝ E]
[T2Space M]
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩)
(x : M)
(B : TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] V x)
:
B = cov.secondCovariantDerivative covT σ x ↔ ∀ (Y : (y : M) → TangentSpace I y),
(ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, Y y⟩) →
∀ (u : TangentSpace I x), (B u) (Y x) = (↑cov (fun (y : M) => (↑cov σ y) (Y y)) x) u - (↑cov σ x) ((↑covT Y x) u)
Evaluation on smooth vector fields in the second slot uniquely characterizes the second covariant derivative of a smooth section.
theorem
CovariantDerivative.secondCovariantDerivative_add
{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]
{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) → 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 ↑⊤]
(covT : CovariantDerivative I E (TangentSpace I))
{σ : (y : M) → V y}
[FiniteDimensional ℝ E]
[T2Space M]
{τ : (y : M) → V y}
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩)
(hτ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, τ y⟩)
(x : M)
:
cov.secondCovariantDerivative covT (σ + τ) x = cov.secondCovariantDerivative covT σ x + cov.secondCovariantDerivative covT τ x
The second covariant derivative is additive in the section.
theorem
CovariantDerivative.secondCovariantDerivative_const_smul
{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]
{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) → 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 ↑⊤]
(covT : CovariantDerivative I E (TangentSpace I))
{σ : (y : M) → V y}
[FiniteDimensional ℝ E]
[T2Space M]
(c : ℝ)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩)
(x : M)
:
The second covariant derivative commutes with multiplication of the section by a constant.
@[simp]
theorem
CovariantDerivative.secondCovariantDerivative_zero
{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]
{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) → 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 ↑⊤]
(covT : CovariantDerivative I E (TangentSpace I))
[FiniteDimensional ℝ E]
[T2Space M]
(x : M)
:
The second covariant derivative of the zero section is zero.
theorem
CovariantDerivative.secondCovariantDerivative_smul_apply
{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]
{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) → 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 ↑⊤]
(covT : CovariantDerivative I E (TangentSpace I))
{σ : (y : M) → V y}
[FiniteDimensional ℝ E]
[T2Space M]
{f : M → ℝ}
(hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩)
(x : M)
{Y : (y : M) → TangentSpace I y}
(hY : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, Y y⟩)
(u : TangentSpace I x)
:
Leibniz rule for the second covariant derivative. For smooth f and σ and a smooth
vector field Y,
∇²(f σ)(u, Y) = f ∇²σ(u, Y) + df(u) ∇_Y σ + df(Y) ∇_u σ + (u (Y f) - (∇ᵀ_u Y) f) σ.
The last coefficient is the second covariant derivative of f for ∇ᵀ.
theorem
CovariantDerivative.secondCovariantDerivative_smul_smul_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]
{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) → 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 ↑⊤]
(covT : CovariantDerivative I E (TangentSpace I))
{σ : (y : M) → V y}
[FiniteDimensional ℝ E]
[T2Space M]
{f g : M → ℝ}
(hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f)
(hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) g)
(hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩)
(x : M)
(u v : TangentSpace I x)
:
((cov.secondCovariantDerivative covT (f • g • σ) x) u) v - f x • ((cov.secondCovariantDerivative covT (g • σ) x) u) v - g x • ((cov.secondCovariantDerivative covT (f • σ) x) u) v + (f x * g x) • ((cov.secondCovariantDerivative covT σ x) u) v = ((d% f x) u * (d% g x) v + (d% g x) u * (d% f x) v) • σ x
The double commutator of the second covariant derivative with multiplication. For smooth
functions f, g and a smooth section σ,
∇²(f g σ) - f ∇²(g σ) - g ∇²(f σ) + f g ∇²σ = (df ⊗ dg + dg ⊗ df) σ.