|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Patrick Massot. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Patrick Massot, Michael Rothgang, Heather Macbeth |
| 5 | +-/ |
| 6 | +module |
| 7 | + |
| 8 | +public import Mathlib.Topology.FiberBundle.Basic |
| 9 | +public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic |
| 10 | +public import Mathlib.Geometry.Manifold.VectorField.LieBracket |
| 11 | + |
| 12 | +/-! # Torsion of an affine connection |
| 13 | +
|
| 14 | +We define the torsion tensor of an affine connection, i.e. a covariant derivative on the tangent |
| 15 | +bundle `TM` of some manifold `M`. |
| 16 | +
|
| 17 | +## Main definitions and results |
| 18 | +
|
| 19 | +* `IsCovariantDerivativeOn.torsion`: the torsion tensor of an unbundled covariant derivative |
| 20 | + on `TM` |
| 21 | +* `CovariantDerivative.torsion`: the torsion tensor of a bundled covariant derivative on `TM` |
| 22 | +* `CovariantDerivative.torsion_eq_zero_iff`: the torsion tensor of a bundled covariant derivative |
| 23 | + `∇` vanishes if and only if `∇_X Y - ∇_Y X = [X, Y]` for all differentiable vector fields |
| 24 | + `X` and `Y`. |
| 25 | +
|
| 26 | +-/ |
| 27 | + |
| 28 | +public noncomputable section |
| 29 | + |
| 30 | +open Bundle Set NormedSpace FiberBundle |
| 31 | +open scoped Manifold ContDiff |
| 32 | + |
| 33 | +variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] |
| 34 | + {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] |
| 35 | + {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} |
| 36 | + {M : Type*} [TopologicalSpace M] [ChartedSpace H M] {x : M} |
| 37 | + |
| 38 | +/-! ## Torsion tensor of an unbundled covariant derivative on `TM` on a set `s` -/ |
| 39 | +namespace IsCovariantDerivativeOn |
| 40 | + |
| 41 | +/-- The torsion of a covariant derivative on the tangent bundle `TM`, as a bare function. |
| 42 | +Prefer to use `IsCovariantDerivativeOn.torsion` (which is a 2-tensor) instead. -/ |
| 43 | +private def torsionAux |
| 44 | + (cov : (Π x : M, TangentSpace I x) → (Π x : M, TangentSpace I x →L[𝕜] TangentSpace I x)) : |
| 45 | + (Π x : M, TangentSpace I x) → (Π x : M, TangentSpace I x) → (Π x : M, TangentSpace I x) := |
| 46 | + fun X Y x ↦ cov Y x (X x) - cov X x (Y x) - VectorField.mlieBracket I X Y x |
| 47 | + |
| 48 | +variable [IsManifold I 2 M] [CompleteSpace E] |
| 49 | + {cov cov' : (Π x : M, TangentSpace I x) → (Π x : M, TangentSpace I x →L[𝕜] TangentSpace I x)} |
| 50 | + {X X' Y : Π x : M, TangentSpace I x} |
| 51 | + |
| 52 | +private theorem torsionAux_tensorial₁ (hcov : IsCovariantDerivativeOn E cov) (x : M) |
| 53 | + (Y : Π x, TangentSpace I x) : |
| 54 | + TensorialAt I E (torsionAux cov · Y x) x where |
| 55 | + smul hf hX := by |
| 56 | + simp [torsionAux, hcov.leibniz hX hf, VectorField.mlieBracket_smul_left hf hX] |
| 57 | + module |
| 58 | + add hX hX' := by |
| 59 | + simp [torsionAux, hcov.add hX hX', VectorField.mlieBracket_add_left hX hX'] |
| 60 | + module |
| 61 | + |
| 62 | +private theorem torsionAux_tensorial₂ (hcov : IsCovariantDerivativeOn E cov) (x : M) |
| 63 | + (X : Π x, TangentSpace I x) : |
| 64 | + TensorialAt I E (torsionAux cov X · x) x where |
| 65 | + smul hf hY := by |
| 66 | + simp [torsionAux, hcov.leibniz hY hf, VectorField.mlieBracket_smul_right hf hY] |
| 67 | + module |
| 68 | + add hY hY' := by |
| 69 | + simp [torsionAux, hcov.add hY hY', VectorField.mlieBracket_add_right hY hY'] |
| 70 | + module |
| 71 | + |
| 72 | +variable [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] |
| 73 | + |
| 74 | +/-- The torsion tensor of an unbundled covariant derivative on `TM`. -/ |
| 75 | +noncomputable def torsion (hcov : IsCovariantDerivativeOn E cov univ) (x : M) : |
| 76 | + TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] TangentSpace I x := |
| 77 | + TensorialAt.mkHom₂ (torsionAux cov · · x) _ |
| 78 | + (fun τ _ ↦ hcov.torsionAux_tensorial₁ x τ) |
| 79 | + (fun σ _ ↦ hcov.torsionAux_tensorial₂ x σ) |
| 80 | + |
| 81 | +theorem torsion_apply (hcov : IsCovariantDerivativeOn E cov univ) {x} |
| 82 | + {X : Π x : M, TangentSpace I x} (hX : MDiffAt (T% X) x) |
| 83 | + {Y : Π x : M, TangentSpace I x} (hY : MDiffAt (T% Y) x) : |
| 84 | + torsion hcov x (X x) (Y x) = cov Y x (X x) - cov X x (Y x) - VectorField.mlieBracket I X Y x := |
| 85 | + TensorialAt.mkHom₂_apply _ _ hX hY |
| 86 | + |
| 87 | +theorem torsion_apply_eq_extend (hcov : IsCovariantDerivativeOn E cov univ) {x} |
| 88 | + (X₀ Y₀ : TangentSpace I x) : |
| 89 | + torsion hcov x X₀ Y₀ = |
| 90 | + cov (extend E Y₀) x X₀ - cov (extend E X₀) x Y₀ - |
| 91 | + VectorField.mlieBracket I (extend E X₀) (extend E Y₀) x := by |
| 92 | + simp [torsion, torsionAux, TensorialAt.mkHom₂_apply_eq_extend] |
| 93 | + |
| 94 | +variable (X) in |
| 95 | +@[simp] |
| 96 | +lemma torsion_self (hcov : IsCovariantDerivativeOn E cov univ) (X₀ : TangentSpace I x) : |
| 97 | + hcov.torsion x X₀ X₀ = 0 := by |
| 98 | + simp [torsion_apply_eq_extend] |
| 99 | + |
| 100 | +variable (X Y) in |
| 101 | +lemma torsion_antisymm (hcov : IsCovariantDerivativeOn E cov univ) (X₀ Y₀ : TangentSpace I x) : |
| 102 | + hcov.torsion x X₀ Y₀ = - hcov.torsion x Y₀ X₀ := by |
| 103 | + simp only [torsion_apply_eq_extend, neg_sub] |
| 104 | + rw [VectorField.mlieBracket_swap] |
| 105 | + dsimp |
| 106 | + module |
| 107 | + |
| 108 | +end IsCovariantDerivativeOn |
| 109 | + |
| 110 | +/-! ## Torsion tensor of a bundled covariant derivative on `TM` -/ |
| 111 | +namespace CovariantDerivative |
| 112 | + |
| 113 | +open VectorField |
| 114 | + |
| 115 | +variable [CompleteSpace 𝕜] [CompleteSpace E] [FiniteDimensional 𝕜 E] [IsManifold I 2 M] |
| 116 | + (cov : CovariantDerivative I E (TangentSpace I : M → Type _)) |
| 117 | + {X Y : Π x : M, TangentSpace I x} |
| 118 | + |
| 119 | +/-- The torsion tensor of a covariant derivative on the tangent bundle of a manifold. -/ |
| 120 | +def torsion (x : M) : TangentSpace I x →L[𝕜] TangentSpace I x →L[𝕜] TangentSpace I x := |
| 121 | + cov.isCovariantDerivativeOn.torsion x |
| 122 | + |
| 123 | +lemma torsion_apply (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) : |
| 124 | + cov.torsion x (X x) (Y x) = cov Y x (X x) - cov X x (Y x) - mlieBracket I X Y x := by |
| 125 | + unfold torsion IsCovariantDerivativeOn.torsion |
| 126 | + apply TensorialAt.mkHom₂_apply |
| 127 | + exacts [hX, hY] |
| 128 | + |
| 129 | +lemma torsion_apply_eq_extend (X₀ Y₀ : TangentSpace I x) : |
| 130 | + cov.torsion x X₀ Y₀ = |
| 131 | + cov (extend E Y₀) x (extend E X₀ x) - cov (extend E X₀) x (extend E Y₀ x) - |
| 132 | + mlieBracket I (extend E X₀) (extend E Y₀) x := by |
| 133 | + unfold torsion IsCovariantDerivativeOn.torsion |
| 134 | + apply TensorialAt.mkHom₂_apply_eq_extend |
| 135 | + |
| 136 | +@[simp] |
| 137 | +lemma torsion_self (X₀ : TangentSpace I x) : cov.torsion x X₀ X₀ = 0 := |
| 138 | + cov.isCovariantDerivativeOn.torsion_self .. |
| 139 | + |
| 140 | +lemma torsion_antisymm (X₀ Y₀ : TangentSpace I x) : cov.torsion x X₀ Y₀ = - cov.torsion x Y₀ X₀ := |
| 141 | + cov.isCovariantDerivativeOn.torsion_antisymm .. |
| 142 | + |
| 143 | +lemma torsion_eq_zero_iff : cov.torsion = 0 ↔ |
| 144 | + ∀ {X Y x}, MDiffAt (T% X) x → MDiffAt (T% Y) x → |
| 145 | + cov Y x (X x) - cov X x (Y x) = mlieBracket I X Y x := by |
| 146 | + constructor |
| 147 | + · intro h X Y x hX hY |
| 148 | + replace h := congr($h x (X x) (Y x)) |
| 149 | + rw [cov.torsion_apply hX hY] at h |
| 150 | + simpa [sub_eq_iff_eq_add'] using h |
| 151 | + · intro h |
| 152 | + ext x u v |
| 153 | + rw [torsion_apply_eq_extend, h] |
| 154 | + · simp |
| 155 | + · apply mdifferentiableAt_extend |
| 156 | + · apply mdifferentiableAt_extend |
| 157 | + |
| 158 | +end CovariantDerivative |
0 commit comments