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] [IsManifold I 1 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. This abuses the defeq between the tangent bundle to H and the bundle with constant fiber E.

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] [IsManifold I 1 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. This abuses the defeq between the tangent bundle to H and the bundle with constant fiber E.

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] [IsManifold I 1 M] {x y : M} (hsrc : x ∈ (chartAt H y).source) : mfderiv% ↑(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] [IsManifold I 1 M] {s : Set M} (hs : UniqueMDiff[s]) : UniqueMDiff[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] [IsManifold I 1 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'] [IsManifold I' 1 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 = d% ↑(extChartAt I' (g x₀)) (g x) ∘SL ϕ x ∘SL mfderiv[Set.range ↑I] ↑(extChartAt I (f x₀)).symm (↑(extChartAt I (f x₀)) (f x)) ∘SL ↑(NormedSpace.fromTangentSpace (↑(extChartAt I (f x₀)) (f x))).symm

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.

theorem inTangentCoordinates_eq_mfderiv_comp_abuse {𝕜 : 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 1 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'] [IsManifold I' 1 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% ↑(extChartAt I' (g x₀)) (g x) ∘SL ϕ x ∘SL mfderiv[Set.range ↑I] ↑(extChartAt I (f x₀)).symm (↑(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, abusing defeq between the tangent space to the model space and the model space.

def tangentBundleModelSpaceDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : ℕ∞) : Diffeomorph I.tangent (I.prod (modelWithCornersSelf 𝕜 E)) (TangentBundle I H) (ModelProd H E) ↑n

The canonical identification between the tangent bundle to the model space and the product, as a diffeomorphism.

Equations

• tangentBundleModelSpaceDiffeomorph I n = { toEquiv := Bundle.TotalSpace.toProd H E, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }