Differentiating a parametric pullback

For a differentiable vector field and a sufficiently smooth parametric family whose inverse spatial Jacobian is differentiable, the derivative at a base time of its pullback is the Lie bracket [V, W] of the family's parameter velocity V with the pulled-back field W, when the family agrees with the identity to first order at the point. This is the vector-space calculus statement underlying the infinitesimal adjoint action of a Lie group.

This supplies a prerequisite for Deliverable A, Layer 1 of TauCetiRoadmap/RepresentationTheory/LieGroups/README.md.

Main result

• VectorField.hasDerivAt_parametric_pullback: differentiating the parametric pullback gives the Lie bracket.
• VectorField.hasDerivAt_parametric_pullback_of_completeSpace: the Banach-space specialization.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The infinitesimal adjoint".
• Sébastien Gouëzel, Mathlib/Analysis/Calculus/VectorField.lean, definitions VectorField.pullback and VectorField.lieBracket.

theorem VectorField.hasDerivAt_parametric_pullback {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : 𝕜 × E → E} {W : E → E} {t₀ : 𝕜} {x : E} (hF : ContDiffAt 𝕜 (minSmoothness 𝕜 2) F (t₀, x)) (hF0 : F (t₀, x) = x) (hA0 : spatialFDeriv F x t₀ = ContinuousLinearMap.id 𝕜 E) (hInvDiff : DifferentiableAt 𝕜 (fun (t : 𝕜) => (spatialFDeriv F x t).inverse) t₀) (hW : DifferentiableAt 𝕜 W x) : HasDerivAt (fun (t : 𝕜) => pullback 𝕜 (fun (y : E) => F (t, y)) W x) (lieBracket 𝕜 (timeFDeriv F t₀) W x) t₀

Let F have the minimum smoothness needed for symmetric second derivatives at (t₀, x) and agree with the identity to first order at x when t = t₀. If the inverse spatial-Jacobian family is differentiable at t₀ and W is differentiable at x, then the derivative of the pullback of W along F is the Lie bracket [V, W], where V is the parameter velocity of F at t₀.

theorem VectorField.hasDerivAt_parametric_pullback_of_completeSpace {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : 𝕜 × E → E} {W : E → E} {t₀ : 𝕜} {x : E} (hF : ContDiffAt 𝕜 (minSmoothness 𝕜 2) F (t₀, x)) (hF0 : F (t₀, x) = x) (hA0 : spatialFDeriv F x t₀ = ContinuousLinearMap.id 𝕜 E) (hW : DifferentiableAt 𝕜 W x) : HasDerivAt (fun (t : 𝕜) => pullback 𝕜 (fun (y : E) => F (t, y)) W x) (lieBracket 𝕜 (timeFDeriv F t₀) W x) t₀

The Banach-space specialization of hasDerivAt_parametric_pullback, where differentiability of the inverse spatial-Jacobian family follows automatically from invertibility at the base point.