Derivatives of maps in the tangent bundle

This file contains properties of derivatives which need the manifold structure of the tangent bundle. Notably, it includes formulas for the tangent maps to charts, and unique differentiability statements for subsets of the tangent bundle.

theorem tangentMap_chart {𝕜 : 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] [SmoothManifoldWithCorners I M] {p q : TangentBundle I M} (h : q.proj ∈ (chartAt H p.proj).source) : tangentMap I I (↑(chartAt H p.proj)) q = (Bundle.TotalSpace.toProd H E).symm (↑(chartAt (ModelProd H E) p) q)

The derivative of the chart at a base point is the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.

theorem tangentMap_chart_symm {𝕜 : 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] [SmoothManifoldWithCorners I M] {p : TangentBundle I M} {q : TangentBundle I H} (h : q.proj ∈ (chartAt H p.proj).target) : tangentMap I I (↑(chartAt H p.proj).symm) q = ↑(chartAt (ModelProd H E) p).symm ((Bundle.TotalSpace.toProd H E) q)

The derivative of the inverse of the chart at a base point is the inverse of the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.

theorem mfderiv_chartAt_eq_tangentCoordChange {𝕜 : 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] [SmoothManifoldWithCorners I M] {x y : M} (hsrc : x ∈ (chartAt H y).source) : mfderiv I I (↑(chartAt H y)) x = tangentCoordChange I x y x

theorem UniqueMDiffOn.tangentBundle_proj_preimage {𝕜 : 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] [SmoothManifoldWithCorners I M] {s : Set M} (hs : UniqueMDiffOn I s) : UniqueMDiffOn I.tangent (Bundle.TotalSpace.proj ⁻¹' s)

The preimage under the projection from the tangent bundle of a set with unique differential in the basis also has unique differential.

theorem inTangentCoordinates_eq_mfderiv_comp {𝕜 : 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] [SmoothManifoldWithCorners I M] {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type u_6} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] {N : Type u_8} {f : N → M} {g : N → M'} {ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)} {x₀ x : N} (hx : f x ∈ (chartAt H (f x₀)).source) (hy : g x ∈ (chartAt H' (g x₀)).source) : inTangentCoordinates I I' f g ϕ x₀ x = (mfderiv I' (modelWithCornersSelf 𝕜 E') (↑(extChartAt I' (g x₀))) (g x)).comp ((ϕ x).comp (mfderivWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I (f x₀)).symm) (Set.range ↑I) (↑(extChartAt I (f x₀)) (f x))))

To write a linear map between tangent spaces in coordinates amounts to precomposing and postcomposing it with derivatives of extended charts. Concrete version of inTangentCoordinates_eq.