Coordinates of tangent fields along curves

For a tangent field along a curve, the coordinate readings TauCeti.Manifold.sectionCoord in the preferred tangent-bundle trivializations at two points differ by the tangent coordinate change between the two charts, wherever the curve lies in both base sets.

Transporting a tangent field along γ by the differential of a map f which is C^n at the base point, with 2 ≤ n, gives a tangent field along f ∘ γ, and differentiability in local coordinates is preserved.

Main results

• TauCeti.Manifold.sectionCoord_coordChange: two chart readings of a tangent field along a curve differ by the tangent coordinate change.
• TauCeti.Manifold.sectionCoord_eventuallyEq_coordChange: the same relation near a parameter whose image lies in both base sets.
• TauCeti.Manifold.derivWithin_sectionCoord_eq: the derivative along the curve of the chart reading of a tangent field in a fixed chart, by the product rule for the coordinate change.
• ContMDiffAt.differentiableWithinAt_sectionCoord_mfderiv: the differential of a map C^n (2 ≤ n) at γ t preserves differentiability of tangent fields along curves in local coordinates.
• ContMDiffAt.differentiableAt_sectionCoord_mfderiv: the unrestricted form.

theorem TauCeti.Manifold.sectionCoord_coordChange {𝕜 : 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] (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) [IsManifold I 1 M] {x y : M} {r : 𝕜} (hx : γ r ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hy : γ r ∈ (trivializationAt E (TangentSpace I) y).baseSet) : sectionCoord γ V y r = (tangentCoordChange I x y (γ r)) (sectionCoord γ V x r)

The coordinate readings of a tangent field along a curve in the trivializations at two points whose base sets contain γ r differ by the tangent coordinate change between them.

theorem TauCeti.Manifold.sectionCoord_eventuallyEq_coordChange {𝕜 : 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] (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) [IsManifold I 1 M] {x y : M} {s : Set 𝕜} {r : 𝕜} (hγ : ContinuousWithinAt γ s r) (hx : γ r ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hy : γ r ∈ (trivializationAt E (TangentSpace I) y).baseSet) : sectionCoord γ V y =ᶠ[nhdsWithin r s] fun (q : 𝕜) => (tangentCoordChange I x y (γ q)) (sectionCoord γ V x q)

Near a parameter whose image lies in two base sets, the coordinate readings of a tangent field along a curve are related by the tangent coordinate change.

theorem TauCeti.Manifold.derivWithin_sectionCoord_eq {𝕜 : 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] (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) [IsManifold I 2 M] {x : M} {s : Set 𝕜} {t : 𝕜} (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hu : UniqueDiffWithinAt 𝕜 s t) (hγ : MDiffAt[s] γ t) (hV : DifferentiableWithinAt 𝕜 (sectionCoord γ V (γ t)) s t) : derivWithin (sectionCoord γ V x) s t = ((d% fun (z : M) => (tangentCoordChange I (γ t) x z) (sectionCoord γ V (γ t) t)) (γ t)) (curveVelocityWithin I γ s t) + (tangentCoordChange I (γ t) x (γ t)) (derivWithin (sectionCoord γ V (γ t)) s t)

The derivative along the curve of the reading of V in the chart at x, where the base set of the trivialization at x contains γ t: the product rule for the reading in the chart at γ t and the tangent coordinate change, whose inhomogeneous term is the derivative of the coordinate change applied to the fixed vector V t in the chart at γ t.

Transport by the differential of a map

theorem ContMDiffAt.differentiableWithinAt_sectionCoord_mfderiv {𝕜 : 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] {γ : 𝕜 → M} {V : (t : 𝕜) → TangentSpace I (γ t)} {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] {f : M → N} {n : WithTop ℕ∞} {s : Set 𝕜} {t : 𝕜} (hf : ContMDiffAt I J n f (γ t)) (hn : 2 ≤ n) (hγ : MDiffAt[s] γ t) (hV : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord (f ∘ γ) (fun (r : 𝕜) => (mfderiv% f (γ r)) (V r)) (f (γ t))) s t

The differential of a map which is C^n at γ t, with 2 ≤ n, carries a tangent field along γ that is differentiable in local coordinates to a tangent field along f ∘ γ that is differentiable in local coordinates.

theorem ContMDiffAt.differentiableAt_sectionCoord_mfderiv {𝕜 : 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] {γ : 𝕜 → M} {V : (t : 𝕜) → TangentSpace I (γ t)} {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {N : Type u_7} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] {f : M → N} {n : WithTop ℕ∞} {t : 𝕜} (hf : ContMDiffAt I J n f (γ t)) (hn : 2 ≤ n) (hγ : MDiffAt γ t) (hV : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) t) : DifferentiableAt 𝕜 (TauCeti.Manifold.sectionCoord (f ∘ γ) (fun (r : 𝕜) => (mfderiv% f (γ r)) (V r)) (f (γ t))) t

The unrestricted form of ContMDiffAt.differentiableWithinAt_sectionCoord_mfderiv.