The canonical symplectic form on a cotangent space

For a real vector space V, the product V × V* is the linear model of its cotangent bundle. It carries the canonical symplectic form

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

This file constructs that form directly from Mathlib's evaluation pairing, proves its nondegeneracy, and records the two canonical Lagrangian subspaces: the zero section V × {0} and a cotangent fiber {0} × V*. These are the pointwise linear-algebra inputs for cotangent bundles in exact Lagrangian Floer theory.

Main declarations

• TauCeti.cotangentSymplecticForm: the canonical symplectic form on V × Module.Dual ℝ V.
• TauCeti.cotangentSymplecticForm_apply: its evaluation formula.
• TauCeti.cotangentZeroSection: the linear zero section V × {0}.
• TauCeti.cotangentFiber: the linear cotangent fiber {0} × V*.
• TauCeti.SymplecticForm.isLagrangian_cotangentZeroSection: the zero section is Lagrangian.
• TauCeti.SymplecticForm.isLagrangian_cotangentFiber: the cotangent fiber is Lagrangian.

The sign convention is the standard one ω = -dλ, where the tautological one-form is λ_(q,p)(δq,δp) = p(δq).

noncomputable def TauCeti.cotangentSymplecticForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] : SymplecticForm (V × Module.Dual ℝ V)

The canonical symplectic form on the linear cotangent space V × V*, with formula ω((v, α), (w, β)) = β(v) - α(w).

@[simp]

theorem TauCeti.cotangentSymplecticForm_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] (x y : V × Module.Dual ℝ V) : (fun (v w : V × Module.Dual ℝ V) => (cotangentSymplecticForm.toBilinForm v) w) x y = y.2 x.1 - x.2 y.1

Evaluation of the canonical cotangent symplectic form.

def TauCeti.cotangentZeroSection {V : Type u_1} [AddCommGroup V] [Module ℝ V] : Submodule ℝ (V × Module.Dual ℝ V)

The zero section V × {0} in the linear cotangent space V × V*.

def TauCeti.cotangentFiber {V : Type u_1} [AddCommGroup V] [Module ℝ V] : Submodule ℝ (V × Module.Dual ℝ V)

The cotangent fiber {0} × V* in the linear cotangent space V × V*.

@[simp]

theorem TauCeti.mem_cotangentZeroSection_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {x : V × Module.Dual ℝ V} : x ∈ cotangentZeroSection ↔ x.2 = 0

@[simp]

theorem TauCeti.mem_cotangentFiber_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {x : V × Module.Dual ℝ V} : x ∈ cotangentFiber ↔ x.1 = 0

@[simp]

theorem TauCeti.SymplecticForm.orthogonal_cotangentZeroSection {V : Type u_1} [AddCommGroup V] [Module ℝ V] : cotangentSymplecticForm.orthogonal cotangentZeroSection = cotangentZeroSection

The symplectic orthogonal of the zero section is the zero section itself.

@[simp]

theorem TauCeti.SymplecticForm.orthogonal_cotangentFiber {V : Type u_1} [AddCommGroup V] [Module ℝ V] : cotangentSymplecticForm.orthogonal cotangentFiber = cotangentFiber

The symplectic orthogonal of a cotangent fiber is that fiber itself.

theorem TauCeti.SymplecticForm.isLagrangian_cotangentZeroSection {V : Type u_1} [AddCommGroup V] [Module ℝ V] : cotangentSymplecticForm.IsLagrangian cotangentZeroSection

The zero section is Lagrangian for the canonical cotangent symplectic form.

theorem TauCeti.SymplecticForm.isLagrangian_cotangentFiber {V : Type u_1} [AddCommGroup V] [Module ℝ V] : cotangentSymplecticForm.IsLagrangian cotangentFiber

The vertical subspace {0} × V* is Lagrangian for the canonical cotangent symplectic form.