Symplectomorphisms preserving a primitive commute with the Liouville flow

Let σ be a two-form on M with primitive θ, σ = -dθ. Its Liouville vector field Z, with L_Z σ = σ, is determined by ι_Z σ = -θ when σ is nondegenerate. A symplectomorphism which also preserves the primitive θ must therefore preserve Z, and so commute with its flow.

This file proves the statement for an arbitrary one-form α in place of -θ, for a vector field Z with ι_Z σ = α: if a diffeomorphism ψ : M → M₂ satisfies ψ^*σ₂ = σ and ψ^*α₂ = α with σ₂ nondegenerate, then dψ (Z x) = Z₂ (ψ x) whenever ι_{Z₂} σ₂ = α₂ (Diffeomorph.mfderiv_apply_eq_of_interior_eq). Indeed both vectors pair under σ₂ with dψ v to α v, and the differential of ψ is onto. Neither closedness of the forms nor finite dimensionality is needed. With α = -θ this is the naturality of Liouville vector fields; with α = df it is the naturality of Hamiltonian vector fields under symplectomorphisms preserving the Hamiltonian.

By naturality of flows, ψ then conjugates the maximal flows of Z and Z₂, which for M₂ = M says that ψ commutes with the local flow of Z (Diffeomorph.apply_flowOf_of_interior_eq).

Main results

• Diffeomorph.mfderiv_apply_eq_of_interior_eq: a symplectomorphism preserving the one-forms carries the vector field dual to one to the vector field dual to the other.
• Diffeomorph.apply_flowOf_of_interior_eq: such a symplectomorphism conjugates their maximal flows; in particular symplectomorphisms preserving a primitive commute with the local Liouville flow.

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Chapter 3 (Liouville vector fields and exact symplectomorphisms).
• A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Section 3 (symplectomorphisms of cotangent bundles).

theorem Diffeomorph.mfderiv_apply_eq_of_interior_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E₂ : Type u_4} {H₂ : Type u_5} {M₂ : Type u_6} [NormedAddCommGroup E₂] [NormedSpace ℝ E₂] [TopologicalSpace H₂] {I₂ : ModelWithCorners ℝ E₂ H₂} [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I₂ (↑⊤) M₂] {σ : TauCeti.SmoothTwoForm I M} {σ₂ : TauCeti.SmoothTwoForm I₂ M₂} {α : TauCeti.RoughForm I M ℝ 1} {α₂ : TauCeti.RoughForm I₂ M₂ ℝ 1} {Z : (x : M) → TangentSpace I x} {Z₂ : (y : M₂) → TangentSpace I₂ y} (ψ : Diffeomorph I I₂ M M₂ ↑⊤) (hσ₂ : σ₂.IsNondegenerate) (hσ : (TauCeti.SmoothForm.mpullback ⇑ψ ⋯) σ₂ = σ) (hα : TauCeti.mpullback I I₂ (⇑ψ) α₂ = α) (hZ : TauCeti.RoughForm.interior Z ↑σ = α) (hZ₂ : TauCeti.RoughForm.interior Z₂ ↑σ₂ = α₂) (x : M) : (mfderiv% ⇑ψ x) (Z x) = Z₂ (ψ x)

Naturality of the vector field dual to a one-form. Let ψ : M → M₂ be a diffeomorphism with ψ^*σ₂ = σ and ψ^*α₂ = α, where σ₂ is nondegenerate. If ι_Z σ = α and ι_{Z₂} σ₂ = α₂, then dψ_x (Z x) = Z₂ (ψ x) for every x. For α = -θ with σ = -dθ, this says that a symplectomorphism preserving the primitives carries the Liouville field of θ to that of θ₂.

theorem Diffeomorph.apply_flowOf_of_interior_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {E₂ : Type u_4} {H₂ : Type u_5} {M₂ : Type u_6} [NormedAddCommGroup E₂] [NormedSpace ℝ E₂] [TopologicalSpace H₂] {I₂ : ModelWithCorners ℝ E₂ H₂} [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I₂ (↑⊤) M₂] {σ : TauCeti.SmoothTwoForm I M} {σ₂ : TauCeti.SmoothTwoForm I₂ M₂} {α : TauCeti.RoughForm I M ℝ 1} {α₂ : TauCeti.RoughForm I₂ M₂ ℝ 1} {Z : (x : M) → TangentSpace I x} {Z₂ : (y : M₂) → TangentSpace I₂ y} [T2Space M₂] [BoundarylessManifold I₂ M₂] (ψ : Diffeomorph I I₂ M M₂ ↑⊤) (hσ₂ : σ₂.IsNondegenerate) (hσ : (TauCeti.SmoothForm.mpullback ⇑ψ ⋯) σ₂ = σ) (hα : TauCeti.mpullback I I₂ (⇑ψ) α₂ = α) (hZ : TauCeti.RoughForm.interior Z ↑σ = α) (hZ₂ : TauCeti.RoughForm.interior Z₂ ↑σ₂ = α₂) (hZ₂' : ContMDiff I₂ I₂.tangent 1 fun (y : M₂) => ⟨y, Z₂ y⟩) (t : ℝ) (x : M) : ψ (TauCeti.flowOf Z t x) = TauCeti.flowOf Z₂ t (ψ x)

Symplectomorphisms preserving a primitive commute with the Liouville flow. Let ψ : M → M₂ be a diffeomorphism with ψ^*σ₂ = σ and ψ^*α₂ = α, where σ₂ is nondegenerate, and let ι_Z σ = α and ι_{Z₂} σ₂ = α₂ with Z₂ of class C^1. Then ψ conjugates the maximal flows: ψ (flowOf Z t x) = flowOf Z₂ t (ψ x). For M₂ = M and α = -θ with σ = -dθ, a symplectomorphism preserving θ commutes with the local flow of the Liouville field of θ.