Curvature in a moving frame

For a local frame s write Aˡⱼ(X) for the coefficient of ∇_X sⱼ along sₗ. The coefficients of curvature in this frame are

Rˡⱼ(X,Y) = X(Aˡⱼ(Y)) - Y(Aˡⱼ(X)) - Aˡⱼ([X,Y]) + Σₘ (Aˡₘ(X) Aᵐⱼ(Y) - Aˡₘ(Y) Aᵐⱼ(X)).

Thus, with section coefficients read as columns, the matrix convention is F = dA + A∧A. The Lie bracket term is retained: neither the frame nor the direction fields need be coordinate fields. On the tangent bundle, expanding that bracket gives the usual structure-coefficient correction to the coordinate curvature formula. These formulas allow curvature computations in orthonormal and other noncoordinate frames using the native IsLocalFrameOn and its coefficients.

Only a C² frame, a C¹ connection on its open domain and C¹ direction fields are required. No metric or torsion condition is imposed, and the bundle need not be the tangent bundle.

References

• J. M. Lee, Introduction to Riemannian Manifolds, second edition, Chapter 7 (curvature in local frames).
• The local differentiation formula extends TauCeti.Manifold.covariantDerivative_eq_frameCovariantDerivative_add_sum from trivialization frames to arbitrary local frames; coefficient regularity uses IsLocalFrameOn.trivialization_mem_maximalAtlas.

theorem IsLocalFrameOn.coeff_curvatureOperator {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {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] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [FiniteDimensional 𝕜 F] {V : M → Type u_6} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module 𝕜 (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul 𝕜 (V x)] [FiberBundle F V] [VectorBundle 𝕜 F V] [ContMDiffVectorBundle 2 F V I] {ι : Type u_7} [Fintype ι] {s : ι → (x : M) → V x} {u : Set M} (hs : IsLocalFrameOn I F 2 s u) (hu : IsOpen u) (cov : CovariantDerivative I F V) [ContMDiffCovariantDerivativeOn F 1 (↑cov) u] {X Y : (x : M) → TangentSpace I x} {x : M} (hx : x ∈ u) (hX : ContMDiffOn I I.tangent 1 (fun (x : M) => ⟨x, X x⟩) u) (hY : ContMDiffOn I I.tangent 1 (fun (x : M) => ⟨x, Y x⟩) u) (j l : ι) : (hs.coeff l x) (cov.curvatureOperator X Y (s j) x) = (d% ((fun (j l : ι) (Z : (x : M) → TangentSpace I x) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (Z y))) j l Y) x) (X x) - (d% ((fun (j l : ι) (Z : (x : M) → TangentSpace I x) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (Z y))) j l X) x) (Y x) + ∑ m : ι, ((fun (j l : ι) (Z : (x : M) → TangentSpace I x) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (Z y))) j m Y x * (fun (j l : ι) (Z : (x : M) → TangentSpace I x) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (Z y))) m l X x - (fun (j l : ι) (Z : (x : M) → TangentSpace I x) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (Z y))) j m X x * (fun (j l : ι) (Z : (x : M) → TangentSpace I x) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (Z y))) m l Y x) - (hs.coeff l x) ((↑cov (s j) x) (VectorField.mlieBracket I X Y x))

The curvature matrix in a C² moving frame is dA + A∧A, evaluated on arbitrary C¹ vector fields. The exterior derivative includes the noncoordinate term -A([X,Y]).

theorem IsLocalFrameOn.coeff_curvatureOperator_frame {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 3 M] {ι : Type u_5} [Fintype ι] {s : ι → (x : M) → TangentSpace I x} {u : Set M} (hs : IsLocalFrameOn I E 2 s u) (hu : IsOpen u) (cov : CovariantDerivative I E (TangentSpace I)) [ContMDiffCovariantDerivativeOn E 1 (↑cov) u] {x : M} (hx : x ∈ u) (i j k l : ι) : (hs.coeff l x) (cov.curvatureOperator (s i) (s j) (s k) x) = (d% ((fun (i j l : ι) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (s i y))) j k l) x) (s i x) - (d% ((fun (i j l : ι) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (s i y))) i k l) x) (s j x) + ∑ m : ι, ((fun (i j l : ι) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (s i y))) j k m x * (fun (i j l : ι) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (s i y))) i m l x - (fun (i j l : ι) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (s i y))) i k m x * (fun (i j l : ι) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (s i y))) j m l x) - ∑ m : ι, (hs.coeff m x) (VectorField.mlieBracket I (s i) (s j) x) * (fun (i j l : ι) (y : M) => (hs.coeff l y) ((↑cov (s j) y) (s i y))) m k l x

The curvature coefficients in a C² tangent frame, with the Lie bracket expanded in the same frame. Its structure coefficients supply the correction absent from a coordinate frame.