Torsion of an affine connection

We define the torsion tensor of an affine connection, i.e. a covariant derivative on the tangent bundle TM of some manifold M.

Main definitions and results

• IsCovariantDerivativeOn.torsion: the torsion tensor of an unbundled covariant derivative on TM
• CovariantDerivative.torsion: the torsion tensor of a bundled covariant derivative on TM
• CovariantDerivative.torsion_eq_zero_iff: the torsion tensor of a bundled covariant derivative ∇ vanishes if and only if ∇_X Y - ∇_Y X = [X, Y] for all differentiable vector fields X and Y.

Torsion tensor of an unbundled covariant derivative on TM on a set s

noncomputable def IsCovariantDerivativeOn.torsion {𝕜 : 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 2 M] [CompleteSpace E] {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov) (x : M) : TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] TangentSpace I x

The torsion tensor of an unbundled covariant derivative on TM.

Equations

• hcov.torsion x = TensorialAt.mkHom₂ (fun (x1 x2 : (x : M) → TangentSpace I x) => IsCovariantDerivativeOn.torsionAux✝ cov x1 x2 x) x ⋯ ⋯

theorem IsCovariantDerivativeOn.torsion_apply {𝕜 : 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 2 M] [CompleteSpace E] {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov) {x : M} {X : (x : M) → TangentSpace I x} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) {Y : (x : M) → TangentSpace I x} (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) : ((hcov.torsion x) (X x)) (Y x) = (cov Y x) (X x) - (cov X x) (Y x) - VectorField.mlieBracket I X Y x

theorem IsCovariantDerivativeOn.torsion_apply_eq_extend {𝕜 : 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 2 M] [CompleteSpace E] {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov) {x : M} (X₀ Y₀ : TangentSpace I x) : ((hcov.torsion x) X₀) Y₀ = (cov (FiberBundle.extend E Y₀) x) X₀ - (cov (FiberBundle.extend E X₀) x) Y₀ - VectorField.mlieBracket I (FiberBundle.extend E X₀) (FiberBundle.extend E Y₀) x

@[simp]

theorem IsCovariantDerivativeOn.torsion_self {𝕜 : 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] {x : M} [IsManifold I 2 M] [CompleteSpace E] {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov) (X₀ : TangentSpace I x) : ((hcov.torsion x) X₀) X₀ = 0

theorem IsCovariantDerivativeOn.torsion_antisymm {𝕜 : 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] {x : M} [IsManifold I 2 M] [CompleteSpace E] {cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] (hcov : IsCovariantDerivativeOn E cov) (X₀ Y₀ : TangentSpace I x) : ((hcov.torsion x) X₀) Y₀ = -((hcov.torsion x) Y₀) X₀

Torsion tensor of a bundled covariant derivative on TM

noncomputable def CovariantDerivative.torsion {𝕜 : 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] [CompleteSpace 𝕜] [CompleteSpace E] [FiniteDimensional 𝕜 E] [IsManifold I 2 M] (cov : CovariantDerivative I E (TangentSpace I)) (x : M) : TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] TangentSpace I x

The torsion tensor of a covariant derivative on the tangent bundle of a manifold.

Equations

• cov.torsion x = ⋯.torsion x

theorem CovariantDerivative.torsion_apply {𝕜 : 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] {x : M} [CompleteSpace 𝕜] [CompleteSpace E] [FiniteDimensional 𝕜 E] [IsManifold I 2 M] (cov : CovariantDerivative I E (TangentSpace I)) {X Y : (x : M) → TangentSpace I x} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) : ((cov.torsion x) (X x)) (Y x) = (↑cov Y x) (X x) - (↑cov X x) (Y x) - VectorField.mlieBracket I X Y x

theorem CovariantDerivative.torsion_apply_eq_extend {𝕜 : 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] {x : M} [CompleteSpace 𝕜] [CompleteSpace E] [FiniteDimensional 𝕜 E] [IsManifold I 2 M] (cov : CovariantDerivative I E (TangentSpace I)) (X₀ Y₀ : TangentSpace I x) : ((cov.torsion x) X₀) Y₀ = (↑cov (FiberBundle.extend E Y₀) x) (FiberBundle.extend E X₀ x) - (↑cov (FiberBundle.extend E X₀) x) (FiberBundle.extend E Y₀ x) - VectorField.mlieBracket I (FiberBundle.extend E X₀) (FiberBundle.extend E Y₀) x

@[simp]

theorem CovariantDerivative.torsion_self {𝕜 : 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] {x : M} [CompleteSpace 𝕜] [CompleteSpace E] [FiniteDimensional 𝕜 E] [IsManifold I 2 M] (cov : CovariantDerivative I E (TangentSpace I)) (X₀ : TangentSpace I x) : ((cov.torsion x) X₀) X₀ = 0

theorem CovariantDerivative.torsion_antisymm {𝕜 : 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] {x : M} [CompleteSpace 𝕜] [CompleteSpace E] [FiniteDimensional 𝕜 E] [IsManifold I 2 M] (cov : CovariantDerivative I E (TangentSpace I)) (X₀ Y₀ : TangentSpace I x) : ((cov.torsion x) X₀) Y₀ = -((cov.torsion x) Y₀) X₀

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