Metric connections

This file defines connections on a Riemannian vector bundle which are compatible with the ambient metric. A bundled connection ∇ on a Riemannian vector bundle (V, g) is compatible with the metric g if and only if the differentiated metric tensor ∇ g (defined by (X, σ, τ) ↦ 𝓛_X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)) vanishes on all differentiable vector fields X and differentiable sections σ, τ.

Main definitions and results

• CovariantDerivative.derivMetricTensor: the tensor (X, σ, τ) ↦ 𝓛_X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ) defining when a connection ∇ on a Riemannian vector bundle (V, g) is compatible with the metric g.
• CovariantDerivative.derivMetricTensor_apply and CovariantDerivative.derivMetricTensor_apply_eq_extend give formulas for applying the compatibility tensor at x to vector fields and sections which are differentiable at x, resp. to extensions of tangent vectors and sections at x to differentiable vector fields and sections near x.
• CovariantDerivative.IsMetricCompatible: predicate for a connection to be metric, namely that ∇ is metric iff its derivMetricTensor vanishes

TODO

• When Mathlib has a notion of parallel transport, prove the equivalence of CovariantDerivative.IsMetricCompatible with the characterisation that parallel transport be an isometry.

• Given connections on bundles V and W, there is an induced connection on the bundle Hom(V, W). When this induced connection has been defined in Mathlib, rephrase the definition of CovariantDerivative.derivMetricTensor, to be simply the covariant derivative of the metric tensor (considered as a section of Hom(V, Hom(V, ℝ))).

Compatible connections

A connection on V is compatible with the metric on V iff 𝓛_X ⟨σ, τ⟩ = ⟨∇_X σ, τ⟩ + ⟨σ, ∇_X τ⟩ holds for all sufficiently nice vector fields X on M and sections σ, τ of V. The left hand side is the Lie derivative of the function ⟨σ, τ⟩ w.r.t. the vector field X: its value at x is df(X x), where f := ⟨σ, τ⟩ (ie. X is seen a derivation on the algebra of functions on the base manifold acting on the function ⟨σ, τ⟩). In our definition, we ask for this identity to hold at each x : M, whenever X, σ and τ are differentiable at x.

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

The tensor (X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ) defining when a connection ∇ on a Riemannian bundle (M, V) is compatible with the metric g.

Equations

• cov.derivMetricTensor x = TensorialAt.mkHom₂ (fun (x1 x2 : (x : M) → V x) => CovariantDerivative.derivMetricTensorAux✝ I cov x1 x2 x) x ⋯ ⋯

theorem CovariantDerivative.derivMetricTensor_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) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] {σ τ : (x : M) → V x} (cov : CovariantDerivative I F V) [VectorBundle ℝ F V] [IsContMDiffRiemannianBundle I 1 F V] {X : (x : M) → TangentSpace I x} [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] (x : M) (hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x) (hτ : (MDiffAt fun (x : M) => ⟨x, τ x⟩) x) : (((cov.derivMetricTensor x) (σ x)) (τ x)) (X x) = ((d% fun (x : M) => inner ℝ (σ x) (τ x)) x) (X x) - (fun (x : M) => inner ℝ ((fun (x : M) => (↑cov σ x) (X x)) x) (τ x)) x - (fun (x : M) => inner ℝ (σ x) ((fun (x : M) => (↑cov τ x) (X x)) x)) x

theorem CovariantDerivative.derivMetricTensor_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) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] (cov : CovariantDerivative I F V) [VectorBundle ℝ F V] [IsContMDiffRiemannianBundle I 1 F V] {x : M} [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] (X₀ : TangentSpace I x) (σ₀ τ₀ : V x) : (((cov.derivMetricTensor x) σ₀) τ₀) X₀ = ((d% fun (x_1 : M) => inner ℝ (FiberBundle.extend F σ₀ x_1) (FiberBundle.extend F τ₀ x_1)) x) X₀ - inner ℝ ((↑cov (FiberBundle.extend F σ₀) x) X₀) τ₀ - inner ℝ σ₀ ((↑cov (FiberBundle.extend F τ₀) x) X₀)

def CovariantDerivative.IsMetricCompatible {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] (cov : CovariantDerivative I F V) [VectorBundle ℝ F V] [IsContMDiffRiemannianBundle I 1 F V] [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] : Prop

Predicate saying that a connection ∇ on a Riemannian bundle (V, g) is compatible with the ambient metric, i.e. for all differentiable vector fields X on M and sections σ and τ of V, we have X ⟨σ, τ⟩ = ⟨∇_X σ, τ⟩ + ⟨σ, ∇_X τ⟩.

Equations

• cov.IsMetricCompatible = (cov.derivMetricTensor = 0)

theorem CovariantDerivative.IsMetricCompatible.mvfderiv_inner_eq {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] {cov : CovariantDerivative I F V} [VectorBundle ℝ F V] [IsContMDiffRiemannianBundle I 1 F V] [ContMDiffVectorBundle 1 F V I] [FiniteDimensional ℝ F] (hcov : cov.IsMetricCompatible) {x : M} (X : (x : M) → TangentSpace I x) {σ τ : (x : M) → V x} (hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x) (hτ : (MDiffAt fun (x : M) => ⟨x, τ x⟩) x) : ((d% fun (x : M) => inner ℝ (σ x) (τ x)) x) (X x) = (fun (x : M) => inner ℝ ((fun (x : M) => (↑cov σ x) (X x)) x) (τ x)) x + (fun (x : M) => inner ℝ (σ x) ((fun (x : M) => (↑cov τ x) (X x)) x)) x

theorem CovariantDerivative.isMetricCompatible_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) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] (cov : CovariantDerivative I F V) [VectorBundle ℝ F V] [IsContMDiffRiemannianBundle I 1 F V] [ContMDiffVectorBundle 1 F V I] [IsManifold I 1 M] [FiniteDimensional ℝ F] : cov.IsMetricCompatible ↔ ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x}, (MDiffAt fun (x : M) => ⟨x, X x⟩) x → (MDiffAt fun (x : M) => ⟨x, σ x⟩) x → (MDiffAt fun (x : M) => ⟨x, τ x⟩) x → ((d% fun (x : M) => inner ℝ (σ x) (τ x)) x) (X x) = (fun (x : M) => inner ℝ ((fun (x : M) => (↑cov σ x) (X x)) x) (τ x)) x + (fun (x : M) => inner ℝ (σ x) ((fun (x : M) => (↑cov τ x) (X x)) x)) x