The Liouville form on a linear cotangent space

The normed linear cotangent space V × V', formed using the continuous dual, carries the tautological, or Liouville, one-form

λ_(q,p)(δq,δp) = p(δq).

This file constructs that differential form and proves the sign convention already used by TauCeti.cotangentSymplecticForm:

strongDualCotangentSymplecticForm = -dλ.

Thus the canonical symplectic form on the linear cotangent model is exact. This is the linear (vector-space) model for the exact cotangent-bundle geometry used in Lagrangian Floer homology; nothing in this file assumes finite dimension. The construction follows McDuff--Salamon, Introduction to Symplectic Topology, Section 3.2.

Main declarations

• TauCeti.cotangentLiouvilleFormCLM: the Liouville form as a continuous linear map of the base point, which is what makes it smooth.
• TauCeti.cotangentLiouvilleForm: the tautological one-form on V × StrongDual ℝ V.
• TauCeti.cotangentLiouvilleForm_apply: its evaluation formula.
• TauCeti.contDiff_cotangentLiouvilleForm: smoothness of the form-valued map, from which TauCeti.differentiable_cotangentLiouvilleForm and TauCeti.differentiableAt_cotangentLiouvilleForm follow.
• TauCeti.extDeriv_cotangentLiouvilleForm_apply: the coordinate formula for the exterior derivative.
• TauCeti.neg_extDeriv_cotangentLiouvilleForm: the exactness identity ω = -dλ, as an equality of alternating two-forms, and TauCeti.neg_extDeriv_cotangentLiouvilleForm_apply, its evaluation on a pair of tangent vectors.
• ContinuousLinearEquiv.cotangentLiouvilleForm_cotangent: the cotangent lift of a continuous linear equivalence preserves the Liouville forms.

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

The Liouville form read as a continuous linear map of the base point: (q, p) is sent to the one-form (δq, δp) ↦ p(δq), which depends linearly and continuously on (q, p). This packaging is what gives the smoothness of TauCeti.cotangentLiouvilleForm.

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

The tautological one-form on the linear cotangent space. At (q, p), it evaluates a tangent vector (δq, δp) by p(δq).

theorem TauCeti.cotangentLiouvilleForm_eq_coe {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : cotangentLiouvilleForm = ⇑cotangentLiouvilleFormCLM

The Liouville form is the underlying function of the continuous linear map TauCeti.cotangentLiouvilleFormCLM.

@[simp]

theorem TauCeti.cotangentLiouvilleForm_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) (v : Fin 1 → V × StrongDual ℝ V) : (cotangentLiouvilleForm x) v = x.2 (v 0).1

The Liouville form evaluates by pairing the covector at the base point with the horizontal component of the tangent vector.

theorem TauCeti.contDiff_cotangentLiouvilleForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : WithTop ℕ∞} : ContDiff ℝ n cotangentLiouvilleForm

The Liouville one-form is smooth as a form-valued function of its base point, being a continuous linear function of that point.

theorem TauCeti.differentiable_cotangentLiouvilleForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : Differentiable ℝ cotangentLiouvilleForm

The Liouville one-form is differentiable as a form-valued function of its base point.

theorem TauCeti.differentiableAt_cotangentLiouvilleForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) : DifferentiableAt ℝ cotangentLiouvilleForm x

The Liouville one-form is differentiable at every base point.

@[simp]

theorem TauCeti.extDeriv_cotangentLiouvilleForm_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) (v : Fin 2 → V × StrongDual ℝ V) : (extDeriv cotangentLiouvilleForm x) v = (v 0).2 (v 1).1 - (v 1).2 (v 0).1

Coordinate formula for the exterior derivative of the Liouville form, evaluated on two tangent vectors: dλ_x(v, w) = δp_v(δq_w) - δp_w(δq_v).

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

The canonical cotangent symplectic form is minus the exterior derivative of the Liouville form, with the identity stated in the direction of the convention ω = -dλ.

theorem TauCeti.neg_extDeriv_cotangentLiouvilleForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V × StrongDual ℝ V) : -(extDeriv cotangentLiouvilleForm x).toAlternatingMap = LinearMap.IsAlt.toAlternatingMap ⋯

Exactness of the canonical cotangent symplectic form. At every base point, minus the exterior derivative of the Liouville form is TauCeti.strongDualCotangentSymplecticForm, as an equality of alternating two-forms on the tangent space. This is the convention ω = -dλ.

theorem ContinuousLinearEquiv.cotangentLiouvilleForm_cotangent {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : V ≃L[ℝ] W) (x : V × StrongDual ℝ V) (v : Fin 1 → V × StrongDual ℝ V) : ((TauCeti.cotangentLiouvilleForm (g.cotangent x)) fun (i : Fin 1) => g.cotangent (v i)) = (TauCeti.cotangentLiouvilleForm x) v

The cotangent lift of a continuous linear equivalence preserves the Liouville forms: λ_(g · x)(g · v) = λ_x(v).