The canonical symplectic form on a continuous-dual cotangent space

For a real normed space V, the continuous-dual cotangent model V × StrongDual ℝ V carries the canonical symplectic form

ω((v, α), (w, β)) = β(v) - α(w).

The form is obtained by restricting TauCeti.cotangentSymplecticForm along the coercion of the continuous dual into the algebraic dual, which is why the two models agree by construction; only nondegeneracy is new, and it comes from Hahn--Banach rather than from a basis. In finite dimension the two models are moreover identified as symplectic vector spaces.

A continuous linear equivalence g : V ≃L[ℝ] W lifts to the symplectomorphism (q, p) ↦ (g q, p ∘ g⁻¹) of the continuous-dual cotangent models, compatibly with identities, composition and inverses.

Main declarations

• TauCeti.strongDualCotangentSymplecticForm: the canonical symplectic form on V × StrongDual ℝ V.
• TauCeti.strongDualCotangentZeroSection: the zero section of V × StrongDual ℝ V.
• TauCeti.strongDualCotangentEquiv: the finite-dimensional identification with V × Module.Dual ℝ V.
• TauCeti.isSymplectomorphism_strongDualCotangentEquiv: that identification is a symplectomorphism.
• ContinuousLinearEquiv.cotangent: the cotangent lift (q, p) ↦ (g q, p ∘ g⁻¹) of a continuous linear equivalence g : V ≃L[ℝ] W.
• ContinuousLinearEquiv.isSymplectomorphism_cotangent: the cotangent lift is a symplectomorphism.

noncomputable def TauCeti.strongDualCotangentSymplecticForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : SymplecticForm (V × StrongDual ℝ V)

The canonical symplectic form on the normed linear cotangent space V × StrongDual ℝ V.

@[simp]

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

The canonical symplectic form on the continuous-dual model has the usual evaluation formula.

def TauCeti.strongDualCotangentZeroSection {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : Submodule ℝ (V × StrongDual ℝ V)

The zero section in the normed linear cotangent space V × StrongDual ℝ V.

@[simp]

theorem TauCeti.mem_strongDualCotangentZeroSection_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (z : V × StrongDual ℝ V) : z ∈ strongDualCotangentZeroSection ↔ z.2 = 0

A point of the normed cotangent space lies in the zero section exactly when its covector coordinate vanishes.

noncomputable def TauCeti.strongDualCotangentEquiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] : (V × StrongDual ℝ V) ≃ₗ[ℝ] V × Module.Dual ℝ V

Identify the normed linear cotangent space, formed with the continuous dual, with the algebraic linear cotangent space.

@[simp]

theorem TauCeti.strongDualCotangentEquiv_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (x : V × StrongDual ℝ V) : strongDualCotangentEquiv x = (x.1, ↑x.2)

The identification of cotangent models forgets the continuity of the covector.

@[simp]

theorem TauCeti.strongDualCotangentEquiv_symm_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (x : V × Module.Dual ℝ V) : strongDualCotangentEquiv.symm x = (x.1, LinearMap.toContinuousLinearMap x.2)

The inverse identification of cotangent models promotes a covector to a continuous one.

theorem TauCeti.isSymplectomorphism_strongDualCotangentEquiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] : strongDualCotangentSymplecticForm.IsSymplectomorphism cotangentSymplecticForm strongDualCotangentEquiv

The finite-dimensional identification of cotangent models is a symplectomorphism from the continuous-dual model to the algebraic one.

noncomputable def ContinuousLinearEquiv.cotangent {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : V ≃L[ℝ] W) : (V × StrongDual ℝ V) ≃L[ℝ] W × StrongDual ℝ W

The cotangent lift (q, p) ↦ (g q, p ∘ g⁻¹) of a continuous linear equivalence g : V ≃L[ℝ] W, as a continuous linear equivalence of the linear cotangent spaces V × StrongDual ℝ V and W × StrongDual ℝ W.

@[simp]

theorem ContinuousLinearEquiv.cotangent_apply_fst {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : V ≃L[ℝ] W) (x : V × StrongDual ℝ V) : (g.cotangent x).1 = g x.1

@[simp]

theorem ContinuousLinearEquiv.cotangent_apply_snd_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : V ≃L[ℝ] W) (x : V × StrongDual ℝ V) (w : W) : (g.cotangent x).2 w = x.2 (g.symm w)

@[simp]

theorem ContinuousLinearEquiv.cotangent_refl {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : (ContinuousLinearEquiv.refl ℝ V).cotangent = ContinuousLinearEquiv.refl ℝ (V × StrongDual ℝ V)

The cotangent lift of the identity is the identity.

@[simp]

theorem ContinuousLinearEquiv.cotangent_trans {V : Type u_1} {W : Type u_2} {X : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedAddCommGroup X] [NormedSpace ℝ X] (g : V ≃L[ℝ] W) (h : W ≃L[ℝ] X) : (g.trans h).cotangent = g.cotangent.trans h.cotangent

The cotangent lift of a composite is the composite of the cotangent lifts.

@[simp]

theorem ContinuousLinearEquiv.cotangent_symm {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : V ≃L[ℝ] W) : g.cotangent.symm = g.symm.cotangent

The inverse of the cotangent lift is the cotangent lift of the inverse.

theorem ContinuousLinearEquiv.strongDualCotangentSymplecticForm_cotangent {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : V ≃L[ℝ] W) (x y : V × StrongDual ℝ V) : (fun (v w : W × StrongDual ℝ W) => (TauCeti.strongDualCotangentSymplecticForm.toBilinForm v) w) (g.cotangent x) (g.cotangent y) = (fun (v w : V × StrongDual ℝ V) => (TauCeti.strongDualCotangentSymplecticForm.toBilinForm v) w) x y

The cotangent lift of a continuous linear equivalence preserves the canonical symplectic forms.

theorem ContinuousLinearEquiv.isSymplectomorphism_cotangent {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (g : V ≃L[ℝ] W) : TauCeti.strongDualCotangentSymplecticForm.IsSymplectomorphism TauCeti.strongDualCotangentSymplecticForm ↑g.cotangent

The cotangent lift of a continuous linear equivalence is a symplectomorphism of the linear cotangent spaces.