The covariant derivative of a field of bilinear forms

Let ∇ be a covariant derivative on a vector bundle V and let b be a field of continuous bilinear forms on the fibres of V. The covariant derivative of b is the tensor

(∇_X b)(σ, τ) = X (b(σ, τ)) - b(∇_X σ, τ) - b(σ, ∇_X τ).

This file constructs it as a continuous trilinear map on each fibre, by the tensoriality criterion TensorialAt.mkHom₂, whenever b pairs sections differentiable at the base point to a function differentiable there. No symmetry, nondegeneracy or positivity of b is assumed: besides metrics of any signature, this applies to the parameter derivative h = ∂ₜ gₜ of a family of metrics, whose covariant derivative appears in the first variation of the Levi-Civita connection.

For the inner product of a Riemannian bundle the tensor is Mathlib's CovariantDerivative.derivMetricTensor, whose vanishing defines metric compatibility.

Main definitions and results

• CovariantDerivative.derivBilinearTensor: the covariant derivative ∇b of a field of bilinear forms b, as a map V x →L[ℝ] V x →L[ℝ] (T_x M →L[ℝ] ℝ).
• CovariantDerivative.derivBilinearTensor_apply: its value on differentiable sections.
• CovariantDerivative.derivBilinearTensor_eq_zero_iff: ∇b vanishes exactly when ∇ satisfies the product rule v (b(σ, τ)) = b(∇_v σ, τ) + b(σ, ∇_v τ).
• CovariantDerivative.derivBilinearTensor_apply_comm: ∇b is symmetric when b is.
• CovariantDerivative.derivBilinearTensor_eq_derivMetricTensor: for the inner product of a Riemannian bundle, ∇b is CovariantDerivative.derivMetricTensor.
• CovariantDerivative.IsMetricCompatible.derivBilinearTensor_eq_zero_of_eq_mul_inner: for a metric-compatible connection, ∇b = 0 when b is a constant multiple of the inner product.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Ch. 4: covariant derivatives of tensor fields.
• Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric: the construction of CovariantDerivative.derivMetricTensor, generalized here from the inner product to an arbitrary differentiable field of bilinear forms.

noncomputable def CovariantDerivative.derivBilinearTensor {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] {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) [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] (b : (x : M) → V x →L[ℝ] V x →L[ℝ] ℝ) (x : M) : V x →L[ℝ] V x →L[ℝ] TangentSpace I x →L[ℝ] ℝ

The covariant derivative of a field of bilinear forms b at x: the tensor (σ₀, τ₀, v) ↦ (∇_v b)(σ₀, τ₀) determined by

(∇_X b)(σ, τ) = X (b(σ, τ)) - b(∇_X σ, τ) - b(σ, ∇_X τ)

on sections σ, τ differentiable at x, by CovariantDerivative.derivBilinearTensor_apply. It is defined when b pairs sections differentiable at x to a function differentiable at x, and is zero otherwise.

theorem CovariantDerivative.derivBilinearTensor_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] {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) {b : (x : M) → V x →L[ℝ] V x →L[ℝ] ℝ} {σ τ : (x : M) → V x} {x : M} [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] (hb : ∀ ⦃σ τ : (x : M) → V x⦄, (MDiffAt fun (x : M) => ⟨x, σ x⟩) x → (MDiffAt fun (x : M) => ⟨x, τ x⟩) x → (MDiffAt fun (y : M) => ((b y) (σ y)) (τ y)) x) (hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x) (hτ : (MDiffAt fun (x : M) => ⟨x, τ x⟩) x) (v : TangentSpace I x) : (((cov.derivBilinearTensor b x) (σ x)) (τ x)) v = ((d% fun (y : M) => ((b y) (σ y)) (τ y)) x) v - ((b x) ((↑cov σ x) v)) (τ x) - ((b x) (σ x)) ((↑cov τ x) v)

The covariant derivative of a field of bilinear forms b, evaluated on sections differentiable at x, is (∇_v b)(σ, τ) = v (b(σ, τ)) - b(∇_v σ, τ) - b(σ, ∇_v τ).

theorem CovariantDerivative.derivBilinearTensor_eq_zero_of_not {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] {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) {b : (x : M) → V x →L[ℝ] V x →L[ℝ] ℝ} {x : M} [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] (hb : ¬∀ ⦃σ τ : (x : M) → V x⦄, (MDiffAt fun (x : M) => ⟨x, σ x⟩) x → (MDiffAt fun (x : M) => ⟨x, τ x⟩) x → (MDiffAt fun (y : M) => ((b y) (σ y)) (τ y)) x) : cov.derivBilinearTensor b x = 0

The covariant derivative of a field of bilinear forms b is zero at x when b does not pair sections differentiable at x to a function differentiable at x.

theorem CovariantDerivative.derivBilinearTensor_apply_eq_extend {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] {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) {b : (x : M) → V x →L[ℝ] V x →L[ℝ] ℝ} {x : M} [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] (hb : ∀ ⦃σ τ : (x : M) → V x⦄, (MDiffAt fun (x : M) => ⟨x, σ x⟩) x → (MDiffAt fun (x : M) => ⟨x, τ x⟩) x → (MDiffAt fun (y : M) => ((b y) (σ y)) (τ y)) x) (σ₀ τ₀ : V x) (v : TangentSpace I x) : (((cov.derivBilinearTensor b x) σ₀) τ₀) v = ((d% fun (y : M) => ((b y) (FiberBundle.extend F σ₀ y)) (FiberBundle.extend F τ₀ y)) x) v - ((b x) ((↑cov (FiberBundle.extend F σ₀) x) v)) τ₀ - ((b x) σ₀) ((↑cov (FiberBundle.extend F τ₀) x) v)

The covariant derivative of a field of bilinear forms b, evaluated on arbitrary vectors in the fibre, through their extensions to sections by FiberBundle.extend.

theorem CovariantDerivative.derivBilinearTensor_apply_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] {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) {b : (x : M) → V x →L[ℝ] V x →L[ℝ] ℝ} {x : M} [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] (hsymm : ∀ (y : M) (v w : V y), ((b y) v) w = ((b y) w) v) (σ₀ τ₀ : V x) : ((cov.derivBilinearTensor b x) σ₀) τ₀ = ((cov.derivBilinearTensor b x) τ₀) σ₀

The covariant derivative of a symmetric field of bilinear forms is symmetric in its two fibre arguments.

theorem CovariantDerivative.derivBilinearTensor_eq_zero_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] {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) {b : (x : M) → V x →L[ℝ] V x →L[ℝ] ℝ} [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] (hb : ∀ (x : M) ⦃σ τ : (x : M) → V x⦄, (MDiffAt fun (x : M) => ⟨x, σ x⟩) x → (MDiffAt fun (x : M) => ⟨x, τ x⟩) x → (MDiffAt fun (y : M) => ((b y) (σ y)) (τ y)) x) : (∀ (x : M), cov.derivBilinearTensor b x = 0) ↔ ∀ ⦃x : M⦄ ⦃σ τ : (x : M) → V x⦄, (MDiffAt fun (x : M) => ⟨x, σ x⟩) x → (MDiffAt fun (x : M) => ⟨x, τ x⟩) x → ∀ (v : TangentSpace I x), ((d% fun (y : M) => ((b y) (σ y)) (τ y)) x) v = ((b x) ((↑cov σ x) v)) (τ x) + ((b x) (σ x)) ((↑cov τ x) v)

The covariant derivative of a field of bilinear forms b vanishes everywhere exactly when ∇ satisfies the product rule v (b(σ, τ)) = b(∇_v σ, τ) + b(σ, ∇_v τ) for all sections σ, τ differentiable at the base point.

theorem CovariantDerivative.derivBilinearTensor_eq_derivMetricTensor {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle 1 F V I] [IsContMDiffRiemannianBundle I 1 F V] [FiniteDimensional ℝ F] (cov : CovariantDerivative I F V) {b : (x : M) → V x →L[ℝ] V x →L[ℝ] ℝ} (hb : ∀ (x : M) (v w : V x), ((b x) v) w = inner ℝ v w) : cov.derivBilinearTensor b = cov.derivMetricTensor

For a field of bilinear forms given by the inner product of a C¹ Riemannian bundle, the covariant derivative is Mathlib's CovariantDerivative.derivMetricTensor.

theorem CovariantDerivative.isMetricCompatible_iff_derivBilinearTensor_eq_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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle 1 F V I] [IsContMDiffRiemannianBundle I 1 F V] [FiniteDimensional ℝ F] (cov : CovariantDerivative I F V) {b : (x : M) → V x →L[ℝ] V x →L[ℝ] ℝ} (hb : ∀ (x : M) (v w : V x), ((b x) v) w = inner ℝ v w) : cov.IsMetricCompatible ↔ ∀ (x : M), cov.derivBilinearTensor b x = 0

A covariant derivative on a C¹ Riemannian bundle is compatible with the metric exactly when the covariant derivative of the inner product, viewed as a field of bilinear forms, vanishes.

theorem CovariantDerivative.IsMetricCompatible.derivBilinearTensor_eq_zero_of_eq_mul_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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle 1 F V I] [IsContMDiffRiemannianBundle I 1 F V] [FiniteDimensional ℝ F] {cov : CovariantDerivative I F V} {b : (x : M) → V x →L[ℝ] V x →L[ℝ] ℝ} (hcov : cov.IsMetricCompatible) (c : ℝ) (hb : ∀ (x : M) (v w : V x), ((b x) v) w = c * inner ℝ v w) (x : M) : cov.derivBilinearTensor b x = 0

For a metric-compatible connection, the covariant derivative of a constant multiple c ⟪·, ·⟫ of the inner product vanishes.