Cotangent lifts preserve the Liouville and canonical symplectic forms

Let h : M → N be a smooth diffeomorphism and T*h : T*M → T*N its cotangent lift (x, p) ↦ (h x, p ∘ (dh_x)⁻¹) (Diffeomorph.cotangent). The Liouville forms are natural:

(T*h)^* λ_N = λ_M (Diffeomorph.mpullback_cotangent_liouvilleForm).

Indeed T*h covers h, so dπ_N ∘ d(T*h) = dh ∘ dπ_M, and the lifted covector pairs with dh (dπ_M v) as the original covector pairs with dπ_M v. Since exterior differentiation commutes with pullback, the canonical symplectic forms ω = -dλ are preserved as well:

(T*h)^* ω_N = ω_M (Diffeomorph.mpullback_cotangent_symplecticForm).

So every diffeomorphism of the base gives an exact symplectomorphism of cotangent bundles. The base may have boundary or corners and need not be finite-dimensional. In particular, cotangent lifts carry exact Lagrangian maps for λ_M to exact Lagrangian maps for λ_N with the same primitive (Diffeomorph.isExactLagrangianMap_cotangent_comp_iff).

In particular, if a group G acts on M by smooth maps, its cotangent-lifted action on T*M (TauCeti.CotangentBundle.instMulAction) preserves λ and ω (TauCeti.CotangentBundle.mpullback_smul_liouvilleForm, TauCeti.CotangentBundle.mpullback_smul_symplecticForm): it is an action by exact symplectomorphisms.

References

• A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Section 2.
• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.2.

@[simp]

theorem Diffeomorph.mpullback_cotangent_liouvilleForm {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} {H' : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I 2 M] [IsManifold J 2 N] (h : Diffeomorph I J M N ↑⊤) : (TauCeti.SmoothForm.mpullback ⇑h.cotangent ⋯) (TauCeti.CotangentBundle.liouvilleForm J N) = TauCeti.CotangentBundle.liouvilleForm I M

Naturality of the Liouville form. The cotangent lift of a smooth diffeomorphism pulls the Liouville form of T*N back to the Liouville form of T*M.

@[simp]

theorem Diffeomorph.mpullback_cotangent_symplecticForm {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} {H' : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I (↑⊤) M] [IsManifold J (↑⊤) N] (h : Diffeomorph I J M N ↑⊤) : (TauCeti.SmoothForm.mpullback ⇑h.cotangent ⋯) (TauCeti.CotangentBundle.symplecticForm J N) = TauCeti.CotangentBundle.symplecticForm I M

Cotangent lifts are symplectic. The cotangent lift of a smooth diffeomorphism pulls the canonical symplectic form of T*N back to the canonical symplectic form of T*M.

theorem Diffeomorph.isExactLagrangianMap_cotangent_comp_iff {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} {H' : Type u_5} [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold I (↑⊤) M] [IsManifold J (↑⊤) N] {E'' : Type u_7} {H'' : Type u_8} [NormedAddCommGroup E''] [NormedSpace ℝ E''] [TopologicalSpace H''] {K : ModelWithCorners ℝ E'' H''} {P : Type u_9} [TopologicalSpace P] [ChartedSpace H'' P] (h : Diffeomorph I J M N ↑⊤) {f : P → TauCeti.CotangentBundle I M} {u : P → ℝ} : TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap K ⋯ (TauCeti.CotangentBundle.liouvilleForm J N) (⇑h.cotangent ∘ f) u ↔ TauCeti.SmoothTwoForm.IsNondegenerate.IsExactLagrangianMap K ⋯ (TauCeti.CotangentBundle.liouvilleForm I M) f u

Cotangent lifts preserve exact Lagrangian maps. For a smooth diffeomorphism h : M → N and a map f into T*M, the composite T*h ∘ f is an exact Lagrangian map for the Liouville form of T*N, with primitive u, exactly when f is one for the Liouville form of T*M, with the same primitive.

@[simp]

theorem TauCeti.CotangentBundle.mpullback_smul_liouvilleForm {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_4} [Group G] [MulAction G M] [ContMDiffConstSMul I (↑⊤) G M] [IsManifold I 2 M] (g : G) : (SmoothForm.mpullback (fun (z : CotangentBundle I M) => g • z) ⋯) (liouvilleForm I M) = liouvilleForm I M

The cotangent-lifted action preserves the Liouville form. For a group acting on M by smooth maps, each element acting on T*M by the cotangent-lifted action pulls the Liouville form back to itself.

@[simp]

theorem TauCeti.CotangentBundle.mpullback_smul_symplecticForm {E : Type u_1} {H : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {G : Type u_4} [Group G] [MulAction G M] [ContMDiffConstSMul I (↑⊤) G M] [IsManifold I (↑⊤) M] (g : G) : (SmoothForm.mpullback (fun (z : CotangentBundle I M) => g • z) ⋯) (symplecticForm I M) = symplecticForm I M

The cotangent-lifted action is symplectic. For a group acting on M by smooth maps, each element acting on T*M by the cotangent-lifted action pulls the canonical symplectic form back to itself.