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 onTMCovariantDerivative.torsion: the torsion tensor of a bundled covariant derivative onTMCovariantDerivative.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 fieldsXandY.
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)
:
The torsion tensor of an unbundled covariant derivative on TM.
Instances For
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 (T% X) x)
{Y : (x : M) → TangentSpace I x}
(hY : MDiffAt (T% Y) 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)
:
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)
:
The torsion tensor of a covariant derivative on the tangent bundle of a manifold.
Instances For
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 (T% X) x)
(hY : MDiffAt (T% Y) 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)
:
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 (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = VectorField.mlieBracket I X Y x