Lie derivatives of differential forms along flows

Let Z be a C² vector field on a finite-dimensional manifold without boundary, with maximal flow φ (TauCeti.flowOf), and let α be a differential form. Wherever the flow through a point x is defined at time t, the pullbacks φₜ^* α at x form a curve in the alternating maps on T_x M, and its velocity is the pullback of the Lie derivative:

d/dt (φₜ^* α)ₓ = (φₜ^* L_Z α)ₓ

(TauCeti.hasDerivAt_mpullback_flowOf). Here L_Z α is TauCeti.mlieDerivForm, which is defined in charts with no reference to flows, so this is the flow characterization of the Lie derivative of forms. At t = 0 it reads d/dt|₀ (φₜ^* α)ₓ = (L_Z α)ₓ. No completeness is needed.

Integrating it along the open interval of times at which the flow through x is defined: if L_Z α = g • α for a continuous function g, then (φₜ^* α)ₓ = exp (∫₀ᵗ g (φₛ x) ds) • αₓ (TauCeti.mpullback_flowOf_apply_eq_exp_integral_smul). This is how the local flow of a contact Hamiltonian vector field rescales the contact form. For a closed form β with closed contraction ι_Z β, Cartan's formula gives L_Z β = 0, so (φₜ^* β)ₓ = βₓ wherever the flow through x is defined at time t (TauCeti.mpullback_flowOf_apply_of_mextDeriv_interior_eq_zero).

When Z is complete its maximal flow is the global flow ψ (TauCeti.globalFlow), and these statements hold at every time and point (TauCeti.hasDerivAt_mpullback_globalFlow, TauCeti.mpullback_globalFlow_apply_eq_exp_integral_smul). In particular, if L_Z α = c • α for a real number c, then ψₜ^* α = e^{ct} α for every time t (TauCeti.mpullback_globalFlow_eq_exp_smul). This is how a Liouville flow rescales the symplectic form and its primitive, which turns hypersurfaces of contact type and the boundary of a Liouville domain into one-parameter families with conjugate characteristic foliations. For a closed form with closed contraction ι_Z α, Cartan's formula gives L_Z α = 0, so the flow preserves the form (TauCeti.mpullback_globalFlow_of_mextDeriv_interior_eq_zero); this is why Hamiltonian flows are symplectic.

In the preferred chart at a point the flow is a jointly C² family of maps, and the statement reduces to its flat counterpart TauCeti.hasDerivAt_compContinuousLinearMap_fderiv. This reduction holds for every jointly C² family of maps ψᵤ which is the identity near y at a time t and moves the points near y with the velocity of a vector field V at time t: then d/du|_{u = t} (ψᵤ^* α)_y = (L_V α)_y (TauCeti.hasDerivAt_mpullback_of_eq_id). Time-dependent flows (TauCeti.Geometry.Manifold.DifferentialForm.Flow.TimeDependent) and smooth isotopies with their Eulerian velocity fields (TauCeti.Geometry.Manifold.DifferentialForm.Flow.Eulerian) are further instances.

Main results

• TauCeti.hasDerivAt_mpullback_of_eq_id: along a C² family of maps which is the identity near y at time t, the velocity of the pullbacks at y at time t is the Lie derivative.
• TauCeti.hasDerivAt_mpullback_of_eq_comp: for a family factoring as ψᵤ = χᵤ ∘ g, the velocity of the pullbacks by ψᵤ is the pullback by g of the velocity of those by χᵤ.
• TauCeti.mpullback_eq_of_forall_mlieDerivForm_eq_zero: pullbacks whose velocities are the pullbacks of vanishing Lie derivatives are independent of time.
• TauCeti.hasDerivAt_mpullback_flowOf_zero, TauCeti.hasDerivAt_mpullback_globalFlow_zero: the velocity of the pullbacks along the maximal or global flow at t = 0 is L_Z α.
• TauCeti.hasDerivAt_mpullback_flowOf: wherever the maximal flow is defined, the time derivative of φₜ^* α is φₜ^* L_Z α.
• TauCeti.mpullback_flowOf_apply_eq_exp_integral_smul: if L_Z α = g • α, then (φₜ^* α)ₓ = exp (∫₀ᵗ g (φₛ x) ds) • αₓ wherever the maximal flow is defined.
• TauCeti.mpullback_flowOf_apply_of_mextDeriv_interior_eq_zero: if β is closed and ι_Z β is closed, then (φₜ^* β)ₓ = βₓ wherever the maximal flow is defined.
• TauCeti.hasDerivAt_mpullback_globalFlow: the time derivative of ψₜ^* α is ψₜ^* L_Z α.
• TauCeti.mpullback_globalFlow_apply_eq_exp_integral_smul: if L_Z α = g • α, then (ψₜ^* α)ₓ = exp (∫₀ᵗ g (ψₛ x) ds) • αₓ.
• TauCeti.mpullback_globalFlow_eq_exp_smul: if L_Z α = c • α, then ψₜ^* α = e^{ct} α.
• TauCeti.mpullback_globalFlow_of_mextDeriv_interior_eq_zero: if α is closed and ι_Z α is closed, then ψₜ^* α = α.

References

• John M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer, 2012, Theorem 12.37 and Proposition 12.36.

Pullbacks along a family of maps

theorem TauCeti.hasDerivAt_mpullback_of_eq_id {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : RoughForm I M F k} {ψ : ℝ → M → M} {V : (x : M) → TangentSpace I x} {t : ℝ} (y : M) (hid : ∀ᶠ (x : M) in nhds y, ψ t x = x) (hsmooth : ContMDiffAt ((modelWithCornersSelf ℝ ℝ).prod I) I 2 (fun (p : ℝ × M) => ψ p.1 p.2) (t, y)) (hvel : ∀ᶠ (x : M) in nhds y, HasMFDerivAt% (fun (u : ℝ) => ψ u x) t (ContinuousLinearMap.smulRight 1 (V (ψ t x)))) (hα : (MDiffAt fun (z : M) => ⟨z, α z⟩) y) : HasDerivAt (fun (u : ℝ) => mpullback I I (ψ u) α y) (mlieDerivForm V α y) t

The Lie derivative is the velocity of pulled-back forms along a family of maps. Let ψᵤ be a family of maps of M which is the identity near y at time t, is jointly C² near (t, y), and moves the points near y at time t with the velocity of a vector field V. Then for a form α differentiable at y, d/du|_{u = t} (ψᵤ^* α)_y = (L_V α)_y.

theorem TauCeti.hasDerivAt_mpullback_of_eq_comp {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : RoughForm I M F k} {ψ χ : ℝ → M → M} {g : M → M} {β : RoughForm I M F k} {x : M} {t : ℝ} (hψ : ∀ᶠ (u : ℝ) in nhds t, ψ u =ᶠ[nhds x] χ u ∘ g) (hg : MDiffAt g x) (hχ : ∀ᶠ (u : ℝ) in nhds t, MDiffAt (χ u) (g x)) (h : HasDerivAt (fun (u : ℝ) => mpullback I I (χ u) α (g x)) (β (g x)) t) : HasDerivAt (fun (u : ℝ) => mpullback I I (ψ u) α x) (mpullback I I g β x) t

Moving the base point of pulled-back forms. Let the maps ψᵤ factor near time t and near x as χᵤ ∘ g through a map g differentiable at x, with each χᵤ differentiable at g x. If the pullbacks (χᵤ^* α)_{g x} have velocity β (g x) at time t, then the pullbacks (ψᵤ^* α)ₓ have velocity (g^* β)ₓ there.

theorem TauCeti.mpullback_eq_of_forall_mlieDerivForm_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {α : RoughForm I M F k} {ψ : ℝ → M → M} {V : ℝ → (x : M) → TangentSpace I x} (hd : ∀ (u : ℝ) (x : M), HasDerivAt (fun (u : ℝ) => mpullback I I (ψ u) α x) (mpullback I I (ψ u) (mlieDerivForm (V u) α) x) u) (hV : ∀ (u : ℝ), mlieDerivForm (V u) α = 0) (s t : ℝ) : mpullback I I (ψ s) α = mpullback I I (ψ t) α

Pullbacks with vanishing Lie derivatives are constant. If at every time u and point x the pullbacks (ψᵤ^* α)ₓ have velocity (ψᵤ^* L_{Vᵤ} α)ₓ, and every Lie derivative L_{Vᵤ} α vanishes, then ψₛ^* α = ψₜ^* α for all times s and t.

Maximal flows

theorem TauCeti.hasDerivAt_mpullback_flowOf_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {Z : (x : M) → TangentSpace I x} {α : RoughForm I M F k} (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) (y : M) (hα : (MDiffAt fun (z : M) => ⟨z, α z⟩) y) : HasDerivAt (fun (s : ℝ) => mpullback I I (flowOf Z s) α y) (mlieDerivForm Z α y) 0

The Lie derivative is the velocity of pulled-back forms at time zero. For a C² vector field Z with maximal flow φ and a form α differentiable at y, d/dt|₀ (φₜ^* α)_y = (L_Z α)_y. The field need not be complete.

theorem TauCeti.hasDerivAt_mpullback_flowOf {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {Z : (x : M) → TangentSpace I x} {α : RoughForm I M F k} (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {t : ℝ} {x : M} (hx : (t, x) ∈ flowDomain Z) (hα : (MDiffAt fun (z : M) => ⟨z, α z⟩) (flowOf Z t x)) : HasDerivAt (fun (s : ℝ) => mpullback I I (flowOf Z s) α x) (mpullback I I (flowOf Z t) (mlieDerivForm Z α) x) t

Lie derivatives along maximal flows. For a C² vector field Z with maximal flow φ, a time t at which the flow through x is defined, and a form α differentiable at φₜ x, the pullbacks (φₛ^* α)ₓ have velocity (φₜ^* L_Z α)ₓ at time t.

theorem TauCeti.mpullback_flowOf_apply_eq_exp_integral_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {Z : (x : M) → TangentSpace I x} {α : RoughForm I M F k} (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {g : M → ℝ} (hg : Continuous g) (hα : MDiff fun (z : M) => ⟨z, α z⟩) (hL : mlieDerivForm Z α = fun (y : M) => g y • α y) {t : ℝ} {x : M} (hx : (t, x) ∈ flowDomain Z) : mpullback I I (flowOf Z t) α x = Real.exp (∫ (s : ℝ) in 0..t, g (flowOf Z s x)) • α x

Rescaling along a maximal flow. If the Lie derivative of a differentiable form α along a C² vector field Z is g • α for a continuous function g, then wherever the maximal flow φ of Z through x is defined at time t, the time-t map pulls α back at x to exp (∫₀ᵗ g (φₛ x) ds) • α x.

theorem TauCeti.mpullback_flowOf_apply_of_mextDeriv_interior_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {Z : (x : M) → TangentSpace I x} (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {β : SmoothForm I M F (k + 1)} (hβ : β.IsClosed) (hZβ : mextDeriv (RoughForm.interior Z ↑β) = 0) {t : ℝ} {x : M} (hx : (t, x) ∈ flowDomain Z) : mpullback I I (flowOf Z t) (↑β) x = ↑β x

Maximal flows preserve closed forms with closed contraction. For a closed smooth form β whose contraction ι_Z β with a C² vector field Z is closed, the time-t map of the maximal flow φ of Z satisfies (φₜ^* β)ₓ = βₓ wherever the flow through x is defined at time t, because Cartan's formula gives L_Z β = d(ι_Z β) = 0. The field need not be complete.

Complete vector fields

theorem TauCeti.hasDerivAt_mpullback_globalFlow_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {Z : (x : M) → TangentSpace I x} {α : RoughForm I M F k} (hc : IsCompleteVectorField Z) (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) (y : M) (hα : (MDiffAt fun (z : M) => ⟨z, α z⟩) y) : HasDerivAt (fun (s : ℝ) => mpullback I I ((globalFlow Z ⋯ hc).toFun s) α y) (mlieDerivForm Z α y) 0

The Lie derivative is the velocity of pulled-back forms at time zero. For a complete C² vector field Z with flow ψ and a form α differentiable at y, d/dt|₀ (ψₜ^* α)_y = (L_Z α)_y.

theorem TauCeti.hasDerivAt_mpullback_globalFlow {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {Z : (x : M) → TangentSpace I x} {α : RoughForm I M F k} (hc : IsCompleteVectorField Z) (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) (x : M) (t : ℝ) (hα : (MDiffAt fun (z : M) => ⟨z, α z⟩) ((globalFlow Z ⋯ hc).toFun t x)) : HasDerivAt (fun (s : ℝ) => mpullback I I ((globalFlow Z ⋯ hc).toFun s) α x) (mpullback I I ((globalFlow Z ⋯ hc).toFun t) (mlieDerivForm Z α) x) t

Lie derivatives along flows. For a complete C² vector field Z with flow ψ and a form α differentiable at ψₜ x, the pullbacks (ψₛ^* α)ₓ have velocity (ψₜ^* L_Z α)ₓ at time t.

theorem TauCeti.mpullback_globalFlow_apply_eq_exp_integral_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {Z : (x : M) → TangentSpace I x} {α : RoughForm I M F k} (hc : IsCompleteVectorField Z) (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {g : M → ℝ} (hg : Continuous g) (hα : MDiff fun (z : M) => ⟨z, α z⟩) (hL : mlieDerivForm Z α = fun (y : M) => g y • α y) (t : ℝ) (x : M) : mpullback I I ((globalFlow Z ⋯ hc).toFun t) α x = Real.exp (∫ (s : ℝ) in 0..t, g ((globalFlow Z ⋯ hc).toFun s x)) • α x

Rescaling along a flow. If the Lie derivative of a differentiable form α along a complete C² vector field Z is g • α for a continuous function g, then the time-t map of the flow ψ of Z pulls α back at x to exp (∫₀ᵗ g (ψₛ x) ds) • α x.

theorem TauCeti.mpullback_globalFlow_eq_exp_smul {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {Z : (x : M) → TangentSpace I x} {α : RoughForm I M F k} (hc : IsCompleteVectorField Z) (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {c : ℝ} (hα : MDiff fun (z : M) => ⟨z, α z⟩) (hL : mlieDerivForm Z α = c • α) (t : ℝ) : mpullback I I ((globalFlow Z ⋯ hc).toFun t) α = Real.exp (c * t) • α

Exponential rescaling along a flow. If the Lie derivative of a differentiable form α along a complete C² vector field Z is c • α, then the time-t map of the flow of Z pulls α back to e^{ct} α.

theorem TauCeti.mpullback_globalFlow_of_mextDeriv_interior_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} {F : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I 2 M] [NormedAddCommGroup F] [NormedSpace ℝ F] {k : ℕ} {Z : (x : M) → TangentSpace I x} (hc : IsCompleteVectorField Z) (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {β : SmoothForm I M F (k + 1)} (hβ : β.IsClosed) (hZβ : mextDeriv (RoughForm.interior Z ↑β) = 0) (t : ℝ) : mpullback I I ((globalFlow Z ⋯ hc).toFun t) ↑β = ↑β

Flows preserve closed forms with closed contraction. For a closed smooth form β whose contraction ι_Z β with a complete C² vector field Z is closed, the flow ψ of Z satisfies ψₜ^* β = β for every time t, because Cartan's formula gives L_Z β = d(ι_Z β) = 0.