Torsion-free covariant derivatives

This file names the pointwise torsion-free condition for a covariant derivative on the tangent bundle. When the bundled torsion tensor is available, isTorsionFree_iff_torsion_eq_zero identifies this condition with its vanishing. The condition is available without finite dimensionality or completeness, and supplies the torsion hypothesis for curvature identities such as the first Bianchi identity. isTorsionFree_addOneForm shows that adding a symmetric endomorphism-valued one-form to a torsion-free connection keeps it torsion-free, as used for the conformally changed Levi-Civita connection.

def CovariantDerivative.IsTorsionFree {𝕜 : 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] (cov : CovariantDerivative I E (TangentSpace I)) : Prop

A covariant derivative on the tangent bundle is torsion-free when it evaluates the Lie bracket of differentiable vector fields as the difference of their two covariant derivatives.

theorem CovariantDerivative.isTorsionFree_iff {𝕜 : 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] (cov : CovariantDerivative I E (TangentSpace I)) : cov.IsTorsionFree ↔ ∀ {X Y : (x : M) → TangentSpace I x} {x : M}, (MDiffAt fun (x : M) => ⟨x, X x⟩) x → (MDiffAt fun (x : M) => ⟨x, Y x⟩) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = VectorField.mlieBracket I X Y x

The pointwise characterization of a torsion-free covariant derivative.

theorem CovariantDerivative.isTorsionFree_addOneForm {𝕜 : 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] {cov : CovariantDerivative I E (TangentSpace I)} (ht : cov.IsTorsionFree) {A : (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] TangentSpace I x} (hA : ∀ (x : M) (v w : TangentSpace I x), ((A x) v) w = ((A x) w) v) : (cov.addOneForm A).IsTorsionFree

Adding a symmetric endomorphism-valued one-form to a torsion-free covariant derivative on the tangent bundle keeps it torsion-free.

theorem CovariantDerivative.covariantDerivative_mlieBracket_apply_eq_sub_of_torsion_free {𝕜 : 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] {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤] (ht : cov.IsTorsionFree) {Y Z : (x : M) → TangentSpace I x} (hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩) (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) (x : M) (u : TangentSpace I x) : (↑cov (VectorField.mlieBracket I Y Z) x) u = (↑cov (fun (y : M) => (↑cov Z y) (Y y)) x) u - (↑cov (fun (y : M) => (↑cov Y y) (Z y)) x) u

Applying a torsion-free connection to the Lie bracket of smooth vector fields gives the difference of applying it to their two covariant derivatives.

theorem CovariantDerivative.isTorsionFree_iff_torsion_eq_zero {𝕜 : 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] [CompleteSpace 𝕜] [CompleteSpace E] [FiniteDimensional 𝕜 E] [IsManifold I 2 M] (cov : CovariantDerivative I E (TangentSpace I)) : cov.IsTorsionFree ↔ cov.torsion = 0

The named torsion-free condition is equivalent to vanishing of the bundled torsion tensor.