Fibrewise translation and dilation of a cotangent bundle

This file records how two families of fibre-preserving diffeomorphisms of the cotangent bundle T*M = TauCeti.CotangentBundle I M act on its Liouville form λ and on its canonical symplectic form ω = -dλ. Both cover the identity of M, and both are instances of general vector-bundle constructions.

• The fibre translation by a smooth one-form α on M, τ_α(p) = p + α_x for a covector p over x: this is TauCeti.vectorBundleTranslateDiffeomorph for the section of T*M defined by α. It satisfies τ_α^*λ = λ + π^*α and τ_α^*ω = ω - π^*dα, where π : T*M → M is the bundle projection. Hence τ_α preserves ω exactly when α is closed (TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_symplecticForm_eq_self_iff).
• The fibre dilation by a nonzero real number c, p ↦ c • p: this is TauCeti.vectorBundleScalarDiffeomorph for the constant function c. It satisfies (c •)^*λ = c • λ and (c •)^*ω = c • ω. For c = -1 this is the fibre negation, which reverses both λ and ω; for c = e^t it is the time-t map of the radial Liouville flow.

Composing a fibre translation with a cotangent lift gives the affine symplectomorphisms of cotangent bundles. For a diffeomorphism h : M → N and a one-form α on N, the cotangent lift of h followed by τ_α pulls λ_N back to λ_M + π^*(h^*α) (Diffeomorph.mpullback_cotangent_trans_vectorBundleTranslateDiffeomorph_liouvilleForm), hence pulls ω_N back to ω_M when α is closed (Diffeomorph.mpullback_cotangent_trans_vectorBundleTranslateDiffeomorph_symplecticForm).

The cotangent projection pulls forms back injectively, because it has the zero section as a smooth right inverse (TauCeti.SmoothForm.mpullback_proj_injective); this turns the identity τ_α^*ω = ω - π^*dα into the closedness criterion. These maps are the global versions of the linear-model maps TauCeti.cotangentFiberNeg and TauCeti.cotangentFiberTranslate; the latter translates by -σ, following the magnetic convention, whereas τ_α translates by +α.

Main declarations

• TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_liouvilleForm and TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_symplecticForm.
• TauCeti.CotangentBundle.mpullback_vectorBundleScalarDiffeomorph_liouvilleForm and TauCeti.CotangentBundle.mpullback_vectorBundleScalarDiffeomorph_symplecticForm.
• Diffeomorph.mpullback_cotangent_trans_vectorBundleTranslateDiffeomorph_liouvilleForm and Diffeomorph.mpullback_cotangent_trans_vectorBundleTranslateDiffeomorph_symplecticForm: a cotangent lift followed by a fibre translation.

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.

Action on the Liouville form

theorem TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_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] [IsManifold I 2 M] (α : SmoothForm I M ℝ 1) : (SmoothForm.mpullback ⇑(vectorBundleTranslateDiffeomorph ⇑(SmoothForm.degreeOneEquiv α) ⋯) ⋯) (liouvilleForm I M) = liouvilleForm I M + (SmoothForm.mpullback Bundle.TotalSpace.proj ⋯) α

Fibre translation shifts the Liouville form. Translating the fibres of the cotangent bundle by a one-form α pulls the Liouville form back to λ + π^*α.

theorem TauCeti.CotangentBundle.mpullback_vectorBundleScalarDiffeomorph_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] [IsManifold I 2 M] {c : ℝ} (hc : c ≠ 0) : (SmoothForm.mpullback ⇑(vectorBundleScalarDiffeomorph (fun (x : M) => c) ⋯ ⋯) ⋯) (liouvilleForm I M) = c • liouvilleForm I M

Fibre dilation rescales the Liouville form. Multiplying the fibres of the cotangent bundle by a nonzero real number c pulls the Liouville form back to c • λ.

Action on the canonical symplectic form

theorem TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_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] [IsManifold I (↑⊤) M] (α : SmoothForm I M ℝ 1) : (SmoothForm.mpullback ⇑(vectorBundleTranslateDiffeomorph ⇑(SmoothForm.degreeOneEquiv α) ⋯) ⋯) (symplecticForm I M) = symplecticForm I M - (SmoothForm.mpullback Bundle.TotalSpace.proj ⋯) ((mextDerivₗ I 1) α)

Fibre translation shifts the canonical symplectic form. Translating the fibres of the cotangent bundle by a one-form α pulls the canonical symplectic form back to ω - π^*dα.

theorem TauCeti.CotangentBundle.mpullback_vectorBundleScalarDiffeomorph_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] [IsManifold I (↑⊤) M] {c : ℝ} (hc : c ≠ 0) : (SmoothForm.mpullback ⇑(vectorBundleScalarDiffeomorph (fun (x : M) => c) ⋯ ⋯) ⋯) (symplecticForm I M) = c • symplecticForm I M

Fibre dilation rescales the canonical symplectic form. Multiplying the fibres of the cotangent bundle by a nonzero real number c pulls the canonical symplectic form back to c • ω. In particular the fibre negation reverses ω.

theorem TauCeti.CotangentBundle.mpullback_vectorBundleTranslateDiffeomorph_symplecticForm_eq_self_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] [IsManifold I (↑⊤) M] (α : SmoothForm I M ℝ 1) : (SmoothForm.mpullback ⇑(vectorBundleTranslateDiffeomorph ⇑(SmoothForm.degreeOneEquiv α) ⋯) ⋯) (symplecticForm I M) = symplecticForm I M ↔ α.IsClosed

Fibre translation by a closed one-form is symplectic. Translating the fibres of the cotangent bundle by a one-form α preserves the canonical symplectic form exactly when α is closed.

Cotangent lifts followed by fibre translations

theorem Diffeomorph.mpullback_cotangent_trans_vectorBundleTranslateDiffeomorph_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 J N ℝ 1) : (TauCeti.SmoothForm.mpullback ⇑(h.cotangent.trans (TauCeti.vectorBundleTranslateDiffeomorph ⇑(TauCeti.SmoothForm.degreeOneEquiv α) ⋯)) ⋯) (TauCeti.CotangentBundle.liouvilleForm J N) = TauCeti.CotangentBundle.liouvilleForm I M + (TauCeti.SmoothForm.mpullback Bundle.TotalSpace.proj ⋯) ((TauCeti.SmoothForm.mpullback ⇑h ⋯) α)

A cotangent lift followed by a fibre translation shifts the Liouville form. For a smooth diffeomorphism h : M → N and a one-form α on N, the cotangent lift of h followed by the translation of the fibres of T*N by α pulls the Liouville form of T*N back to λ_M + π^*(h^*α).

theorem Diffeomorph.mpullback_cotangent_trans_vectorBundleTranslateDiffeomorph_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 J N ℝ 1} (hα : α.IsClosed) : (TauCeti.SmoothForm.mpullback ⇑(h.cotangent.trans (TauCeti.vectorBundleTranslateDiffeomorph ⇑(TauCeti.SmoothForm.degreeOneEquiv α) ⋯)) ⋯) (TauCeti.CotangentBundle.symplecticForm J N) = TauCeti.CotangentBundle.symplecticForm I M

A cotangent lift followed by a closed fibre translation is symplectic. For a smooth diffeomorphism h : M → N and a closed one-form α on N, the cotangent lift of h followed by the translation of the fibres of T*N by α pulls the canonical symplectic form of T*N back to that of T*M.