Fibrewise negation and magnetic translation of a linear cotangent space

On the normed linear cotangent space V × V' (with V' the continuous dual), with Liouville form λ_(q,p)(δq, δp) = p(δq) and canonical symplectic form ω = -dλ (TauCeti.strongDualCotangentSymplecticForm), this file records how two fibrewise maps act on these forms. They are the linear models of the maps that compare sign conventions for cotangent bundles and that remove an exact magnetic term.

• The fibrewise negation ν(q, p) = (q, -p) (TauCeti.cotangentFiberNeg) covers the identity of V, satisfies ν^*λ = -λ and reverses ω. It therefore identifies the cotangent space with the symplectic form dλ = -ω of the opposite sign convention with the cotangent space with ω, and it carries the Liouville primitive λ of dλ to the primitive -λ of ω. Its Liouville vector field is the radial field Z(q, p) = (0, p), that is p ∂_p (TauCeti.cotangentLiouvilleField): ι_Z ω = -λ.
• The magnetic translation Ψ_σ(q, p) = (q, p - σ_q) by a one-form σ on V (TauCeti.cotangentFiberTranslate) also covers the identity of V, and it is a bijection with inverse Ψ_{-σ}. At every point where σ is differentiable, it satisfies the pointwise identities Ψ_σ^*λ = λ - π^*σ and Ψ_σ^*ω = ω + π^*dσ, where π is the projection to V. These need σ to be differentiable only at the base point, and the second is proved by direct computation, without the second derivative of σ. So for a smooth σ (for which Ψ_σ and Ψ_{-σ} are smooth), Ψ_σ is a symplectomorphism from the magnetic form ω + π^*dσ to ω, and for a smooth closed σ it preserves ω. This file records the pointwise identities; it does not bundle Ψ_σ as a symplectomorphism.

Conjugating a magnetic translation by ν changes the sign of the one-form (TauCeti.cotangentFiberNeg_cotangentFiberTranslate_cotangentFiberNeg).

Main declarations

• TauCeti.cotangentFiberNeg, with TauCeti.cotangentLiouvilleForm_cotangentFiberNeg and TauCeti.strongDualCotangentSymplecticForm_cotangentFiberNeg.
• TauCeti.cotangentLiouvilleField, with TauCeti.strongDualCotangentSymplecticForm_cotangentLiouvilleField and TauCeti.curryLeft_extDeriv_neg_cotangentLiouvilleForm.
• TauCeti.cotangentFiberTranslate, with its derivative TauCeti.fderiv_cotangentFiberTranslate, TauCeti.cotangentLiouvilleForm_cotangentFiberTranslate (Ψ_σ^*λ = λ - π^*σ) and TauCeti.strongDualCotangentSymplecticForm_fderiv_cotangentFiberTranslate (Ψ_σ^*ω = ω + π^*dσ).

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.2 (cotangent bundles and the Liouville form).
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953: the sign conventions for cotangent bundles and the magnetic cotangent bundles of Corollary D.

Fibrewise negation

noncomputable def TauCeti.cotangentFiberNeg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : (V × StrongDual ℝ V) ≃L[ℝ] V × StrongDual ℝ V

The fibrewise negation (q, p) ↦ (q, -p) of the linear cotangent space.

@[simp]

theorem TauCeti.cotangentFiberNeg_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) : cotangentFiberNeg x = (x.1, -x.2)

The fibrewise negation keeps the base point and negates the covector.

@[simp]

theorem TauCeti.cotangentFiberNeg_symm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : cotangentFiberNeg.symm = cotangentFiberNeg

The fibrewise negation is an involution.

theorem TauCeti.cotangentLiouvilleForm_cotangentFiberNeg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) : (cotangentLiouvilleForm (cotangentFiberNeg x)).compContinuousLinearMap ↑cotangentFiberNeg = -cotangentLiouvilleForm x

The fibrewise negation pulls the Liouville form back to its negative: ν^*λ = -λ. The derivative of ν at every point is ν itself (ContinuousLinearEquiv.fderiv).

theorem TauCeti.strongDualCotangentSymplecticForm_cotangentFiberNeg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (v w : V × StrongDual ℝ V) : (fun (v w : V × StrongDual ℝ V) => (strongDualCotangentSymplecticForm.toBilinForm v) w) (cotangentFiberNeg v) (cotangentFiberNeg w) = -(fun (v w : V × StrongDual ℝ V) => (strongDualCotangentSymplecticForm.toBilinForm v) w) v w

The fibrewise negation reverses the canonical symplectic form: ν^*ω = -ω.

The radial Liouville field

noncomputable def TauCeti.cotangentLiouvilleField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : V × StrongDual ℝ V →L[ℝ] V × StrongDual ℝ V

The radial vector field p ∂_p of the linear cotangent space, (q, p) ↦ (0, p), as a continuous linear map. It is the Liouville vector field of the primitive -λ of ω (strongDualCotangentSymplecticForm_cotangentLiouvilleField).

@[simp]

theorem TauCeti.cotangentLiouvilleField_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) : cotangentLiouvilleField x = (0, x.2)

The radial field at (q, p) is the vertical vector (0, p).

theorem TauCeti.strongDualCotangentSymplecticForm_cotangentLiouvilleField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x v : V × StrongDual ℝ V) : (fun (v w : V × StrongDual ℝ V) => (strongDualCotangentSymplecticForm.toBilinForm v) w) (cotangentLiouvilleField x) v = -(cotangentLiouvilleForm x) fun (x : Fin 1) => v

The radial field is the Liouville field of -λ for ω: ι_Z ω = -λ.

theorem TauCeti.cotangentLiouvilleField_cotangentFiberNeg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) : cotangentLiouvilleField (cotangentFiberNeg x) = cotangentFiberNeg (cotangentLiouvilleField x)

The fibrewise negation preserves the radial field.

theorem TauCeti.curryLeft_extDeriv_neg_cotangentLiouvilleForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) : (extDeriv (-cotangentLiouvilleForm) x).curryLeft (cotangentLiouvilleField x) = -cotangentLiouvilleForm x

The radial field p ∂_p satisfies ι_{p ∂_p} d(-λ) = -λ for the tautological form λ = p dq.

Magnetic translation

noncomputable def TauCeti.cotangentFiberTranslate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (σ : V → V [⋀^Fin 1]→L[ℝ] ℝ) (x : V × StrongDual ℝ V) : V × StrongDual ℝ V

The magnetic translation (q, p) ↦ (q, p - σ_q) of the linear cotangent space by a one-form σ on V. The covector σ_q is the one-form σ q read as a continuous linear map.

@[simp]

theorem TauCeti.cotangentFiberTranslate_fst {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (σ : V → V [⋀^Fin 1]→L[ℝ] ℝ) (x : V × StrongDual ℝ V) : (cotangentFiberTranslate σ x).1 = x.1

A magnetic translation covers the identity of V.

@[simp]

theorem TauCeti.cotangentFiberTranslate_snd_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (σ : V → V [⋀^Fin 1]→L[ℝ] ℝ) (x : V × StrongDual ℝ V) (v : V) : (cotangentFiberTranslate σ x).2 v = x.2 v - (σ x.1) fun (x : Fin 1) => v

A magnetic translation subtracts σ_q from the covector at q.

@[simp]

theorem TauCeti.cotangentFiberTranslate_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : cotangentFiberTranslate 0 = id

The magnetic translation by the zero one-form is the identity.

theorem TauCeti.cotangentFiberTranslate_add {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (σ τ : V → V [⋀^Fin 1]→L[ℝ] ℝ) (x : V × StrongDual ℝ V) : cotangentFiberTranslate (σ + τ) x = cotangentFiberTranslate σ (cotangentFiberTranslate τ x)

Magnetic translations compose by adding the one-forms.

theorem TauCeti.leftInverse_cotangentFiberTranslate_neg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (σ : V → V [⋀^Fin 1]→L[ℝ] ℝ) : Function.LeftInverse (cotangentFiberTranslate (-σ)) (cotangentFiberTranslate σ)

Translating by -σ undoes the translation by σ.

theorem TauCeti.rightInverse_cotangentFiberTranslate_neg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (σ : V → V [⋀^Fin 1]→L[ℝ] ℝ) : Function.RightInverse (cotangentFiberTranslate (-σ)) (cotangentFiberTranslate σ)

Translating by σ undoes the translation by -σ.

theorem TauCeti.cotangentFiberNeg_cotangentFiberTranslate_cotangentFiberNeg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (σ : V → V [⋀^Fin 1]→L[ℝ] ℝ) (x : V × StrongDual ℝ V) : cotangentFiberNeg (cotangentFiberTranslate σ (cotangentFiberNeg x)) = cotangentFiberTranslate (-σ) x

Conjugation by the fibrewise negation changes the sign of the one-form: ν ∘ Ψ_σ ∘ ν is the fibre translation (q, p) ↦ (q, p + σ_q).

theorem TauCeti.contDiff_cotangentFiberTranslate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : WithTop ℕ∞} {σ : V → V [⋀^Fin 1]→L[ℝ] ℝ} (hσ : ContDiff ℝ n σ) : ContDiff ℝ n (cotangentFiberTranslate σ)

The magnetic translation by a C^n one-form is C^n.

theorem TauCeti.hasFDerivAt_cotangentFiberTranslate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {σ : V → V [⋀^Fin 1]→L[ℝ] ℝ} {x : V × StrongDual ℝ V} (hσ : DifferentiableAt ℝ σ x.1) : HasFDerivAt (cotangentFiberTranslate σ) ((ContinuousLinearMap.fst ℝ V (StrongDual ℝ V)).prod (ContinuousLinearMap.snd ℝ V (StrongDual ℝ V) - ↑↑(ContinuousAlternatingMap.ofSubsingletonLIE 0).symm ∘SL fderiv ℝ σ x.1 ∘SL ContinuousLinearMap.fst ℝ V (StrongDual ℝ V))) x

The derivative of a magnetic translation: DΨ_σ (δq, δp) = (δq, δp - (Dσ δq)_q).

theorem TauCeti.fderiv_cotangentFiberTranslate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {σ : V → V [⋀^Fin 1]→L[ℝ] ℝ} {x : V × StrongDual ℝ V} (hσ : DifferentiableAt ℝ σ x.1) (v : V × StrongDual ℝ V) : (fderiv ℝ (cotangentFiberTranslate σ) x) v = (v.1, v.2 - (ContinuousAlternatingMap.ofSubsingletonLIE 0).symm ((fderiv ℝ σ x.1) v.1))

The derivative of a magnetic translation on a tangent vector.

theorem TauCeti.cotangentLiouvilleForm_cotangentFiberTranslate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {σ : V → V [⋀^Fin 1]→L[ℝ] ℝ} {x : V × StrongDual ℝ V} (hσ : DifferentiableAt ℝ σ x.1) : (cotangentLiouvilleForm (cotangentFiberTranslate σ x)).compContinuousLinearMap (fderiv ℝ (cotangentFiberTranslate σ) x) = cotangentLiouvilleForm x - (σ x.1).compContinuousLinearMap (ContinuousLinearMap.fst ℝ V (StrongDual ℝ V))

The magnetic translation pulls the Liouville form back to λ - π^*σ.

theorem TauCeti.strongDualCotangentSymplecticForm_fderiv_cotangentFiberTranslate {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {σ : V → V [⋀^Fin 1]→L[ℝ] ℝ} {x : V × StrongDual ℝ V} (hσ : DifferentiableAt ℝ σ x.1) (v w : V × StrongDual ℝ V) : (fun (v w : V × StrongDual ℝ V) => (strongDualCotangentSymplecticForm.toBilinForm v) w) ((fderiv ℝ (cotangentFiberTranslate σ) x) v) ((fderiv ℝ (cotangentFiberTranslate σ) x) w) = (fun (v w : V × StrongDual ℝ V) => (strongDualCotangentSymplecticForm.toBilinForm v) w) v w + (extDeriv σ x.1) ![v.1, w.1]

The magnetic translation pulls ω back to the magnetic form ω + π^*dσ. On tangent vectors v and w at x, ω(DΨ_σ v, DΨ_σ w) = ω(v, w) + dσ_q(δq_v, δq_w), where q = π x. Only the differentiability of σ at q is used.

theorem TauCeti.strongDualCotangentSymplecticForm_fderiv_cotangentFiberTranslate_of_extDeriv_eq_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {σ : V → V [⋀^Fin 1]→L[ℝ] ℝ} {x : V × StrongDual ℝ V} (hσ : DifferentiableAt ℝ σ x.1) (hdσ : extDeriv σ x.1 = 0) (v w : V × StrongDual ℝ V) : (fun (v w : V × StrongDual ℝ V) => (strongDualCotangentSymplecticForm.toBilinForm v) w) ((fderiv ℝ (cotangentFiberTranslate σ) x) v) ((fderiv ℝ (cotangentFiberTranslate σ) x) w) = (fun (v w : V × StrongDual ℝ V) => (strongDualCotangentSymplecticForm.toBilinForm v) w) v w

For a one-form σ that is closed at q = π x, the derivative of the magnetic translation at x preserves the canonical symplectic form.