Tangent lifts of diffeomorphisms

The differential of a smooth diffeomorphism, bundled over the map itself, is a smooth diffeomorphism between the tangent bundles. Its inverse is the tangent lift of the inverse diffeomorphism. This packages the tangent map in a form suitable for transporting vector fields, integral curves, and their maximal domains.

The construction is functorial: tangent lifts preserve identity maps, inverses, and composition. The underlying function is Mathlib's tangentMap; no parallel tangent-map API is introduced.

Main definitions and results

• Diffeomorph.tangent: the tangent lift of a smooth diffeomorphism.
• Diffeomorph.tangent_symm: taking a tangent lift commutes with inversion.
• Diffeomorph.tangent_symm_mk: the inverse tangent lift acts on fibres by (dh_x)⁻¹.
• Diffeomorph.tangent_refl: the tangent lift of the identity is the identity.
• Diffeomorph.tangent_trans: taking a tangent lift commutes with composition.
• Diffeomorph.tangent_curveVelocityLift: tangent lifts carry the velocity lift of a differentiable curve to the velocity lift of its image.

noncomputable def Diffeomorph.tangent {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] (h : Diffeomorph I J M N ↑⊤) : Diffeomorph I.tangent J.tangent (TangentBundle I M) (TangentBundle J N) ↑⊤

The tangent lift of a smooth diffeomorphism. Its value at (x, v) is (h x, mfderiv I J h x v), and its inverse is the tangent lift of h.symm.

@[simp]

theorem Diffeomorph.coe_tangent {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] (h : Diffeomorph I J M N ↑⊤) : ⇑h.tangent = tangentMap I J ⇑h

The underlying function of the tangent lift is Mathlib's tangentMap.

@[simp]

theorem Diffeomorph.tangent_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] (h : Diffeomorph I J M N ↑⊤) : h.tangent.symm = h.symm.tangent

The inverse of a tangent lift is the tangent lift of the inverse diffeomorphism.

theorem Diffeomorph.tangent_symm_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] (h : Diffeomorph I J M N ↑⊤) (x : M) (w : TangentSpace J (h x)) : h.tangent.symm ⟨h x, w⟩ = ⟨x, (mfderiv% ⇑h x).inverse w⟩

The inverse tangent lift sends (h x, w) to (x, (dh_x)⁻¹ w).

@[simp]

theorem Diffeomorph.tangent_refl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] : (Diffeomorph.refl I M ↑⊤).tangent = Diffeomorph.refl I.tangent (TangentBundle I M) ↑⊤

The tangent lift of the identity diffeomorphism is the identity diffeomorphism of the tangent bundle.

@[simp]

theorem Diffeomorph.tangent_trans {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {H'' : Type u_7} [TopologicalSpace H''] {K : ModelWithCorners 𝕜 G H''} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {P : Type u_10} [TopologicalSpace P] [ChartedSpace H'' P] [IsManifold K 1 P] (h : Diffeomorph I J M N ↑⊤) (g : Diffeomorph J K N P ↑⊤) : (h.trans g).tangent = h.tangent.trans g.tangent

Tangent lift commutes with composition of smooth diffeomorphisms.

theorem Diffeomorph.tangent_curveVelocityLift {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners 𝕜 F H'} {M : Type u_8} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_9} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] (h : Diffeomorph I J M N ↑⊤) {γ : 𝕜 → M} {t : 𝕜} (hγ : MDiffAt γ t) : h.tangent (TauCeti.Manifold.curveVelocityLift I γ t) = TauCeti.Manifold.curveVelocityLift J (⇑h ∘ γ) t

A tangent lift carries the velocity lift of a differentiable curve to the velocity lift of the image curve. This is the bundled tangent-map form of the chain rule.