Covariant differentiation commutes with the metric trace

Let ∇ be a connection on the tangent bundle of a Riemannian manifold which is compatible with the metric, and let b be a field of bilinear forms on the tangent spaces. The metric trace tr_g b is then a function on the manifold whose derivative is the metric trace of the covariant derivative of b:

d (tr_g b)(v) = ∑ᵢ (∇_v b)(eᵢ, eᵢ)

for every orthonormal basis eᵢ of the tangent space at the point. Since the metric is parallel, the contraction against it commutes with covariant differentiation. This is the identity that turns the contracted second Bianchi identity into 2 div Ric = d Scal, and more generally computes the derivative of any metric trace of a covariant two-tensor.

The proof works in the chart-local frame Fᵢ and its metric-dual frame Dᵢ = ∑ⱼ (G⁻¹)ᵢⱼ Fⱼ, where G is the Gram matrix of Fᵢ. Near the point, tr_g b = ∑ᵢ b(Fᵢ, Dᵢ). Differentiating ⟪Dᵢ, Fⱼ⟫ = δᵢⱼ with the metric shows that the terms of d (∑ᵢ b(Fᵢ, Dᵢ)) involving ∇Fᵢ and ∇Dᵢ cancel, which leaves ∑ᵢ (∇_v b)(Fᵢ, Dᵢ).

Main results

• CovariantDerivative.IsMetricCompatible.mvfderiv_bilinFormTrace: the derivative of the metric trace of a field of bilinear forms is the trace of its covariant derivative.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Ch. 4: covariant derivatives of tensor fields commute with contractions, and the metric is parallel.

theorem CovariantDerivative.IsMetricCompatible.mvfderiv_bilinFormTrace {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E (TangentSpace I)} (hcov : cov.IsMetricCompatible) {b : (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} {x : M} (hb : ∀ ⦃σ τ : (x : M) → TangentSpace I x⦄, (MDiffAt fun (x : M) => ⟨x, σ x⟩) x → (MDiffAt fun (x : M) => ⟨x, τ x⟩) x → (MDiffAt fun (y : M) => ((b y) (σ y)) (τ y)) x) {ι : Type u_4} [Fintype ι] (e : OrthonormalBasis ι ℝ (TangentSpace I x)) (v : TangentSpace I x) : ((d% fun (y : M) => TauCeti.bilinFormTrace (ContinuousLinearMap.toLinearMap₁₂ (b y))) x) v = ∑ i : ι, (((cov.derivBilinearTensor b x) (e i)) (e i)) v

Covariant differentiation commutes with the metric trace. For a connection compatible with the metric and a field of bilinear forms b pairing sections differentiable at x to functions differentiable at x, the derivative of the metric trace of b along v is the metric trace of ∇_v b, computed in any orthonormal basis of the tangent space at x.