Symplectic vector fields and their de Rham classes #
Let σ be a smooth two-form on a manifold M. A smooth vector field X is a symplectic vector
field when its contraction ι_X σ is a closed one-form
(TauCeti.SmoothTwoForm.symplecticVectorFields). When σ is closed, Cartan's formula
L_X σ = ι_X dσ + d(ι_X σ) = d(ι_X σ) shows that these are exactly the smooth vector fields with
L_X σ = 0, the infinitesimal symmetries of σ
(TauCeti.SmoothTwoForm.mem_symplecticVectorFields_iff_mlieDerivForm_eq_zero).
Sending a symplectic vector field to the de Rham class of its contraction gives a linear map
X ↦ [ι_X σ] to the first de Rham cohomology H¹_dR(M)
(TauCeti.SmoothTwoForm.interiorClass). For a nondegenerate σ on a finite-dimensional
manifold, a smooth function f has the smooth Hamiltonian vector field X_f, with
ι_{X_f} σ = df.
The sequence below uses f ↦ -X_f
(TauCeti.SmoothTwoForm.IsNondegenerate.negHamiltonianₗ, defined on smooth 0-forms). This sign
follows the identity X_{{f, g}} = -[X_f, X_g], valid for closed σ with the bracket
{f, g} = df(X_g), under which f ↦ -X_f respects Lie brackets
(TauCeti.SmoothTwoForm.IsNondegenerate.hamiltonianVectorField_poissonBracket); brackets
themselves are not treated in this file. These maps
form the exact sequence
0 → H⁰_dR(M) → C^∞(M) → {symplectic vector fields} → H¹_dR(M) → 0.
Here the first term is the space closedForms I M 0 of locally constant smooth functions, which
TauCeti.deRhamCohomology.mk identifies with H⁰_dR(M).
- At
C^∞(M):-X_f = 0exactly whendf = 0, so the kernel off ↦ -X_fis the space of closed0-forms (TauCeti.SmoothTwoForm.IsNondegenerate.ker_negHamiltonianₗ). - At the symplectic vector fields:
[ι_X σ] = 0exactly whenι_X σ = dffor a smoothf, that is whenXis the Hamiltonian vector field off(TauCeti.SmoothTwoForm.IsNondegenerate.exact_negHamiltonianₗ_interiorClassandTauCeti.SmoothTwoForm.interiorClass_eq_zero_iff). - At
H¹_dR(M): every closed one-formαis the contraction of the smooth vector field(σ♭)⁻¹ α, so every class is reached (TauCeti.SmoothTwoForm.IsNondegenerate.interiorClass_surjective).
No closedness of σ is needed for the exactness results. Closedness enters this file only through
the comparison with the Lie derivative; it is also needed for the bracket compatibility above,
which is not treated here.
Main declarations #
TauCeti.SmoothTwoForm.symplecticVectorFields: the smooth vector fields with closed contraction.TauCeti.SmoothTwoForm.mem_symplecticVectorFields_iff_mlieDerivForm_eq_zero: for closedσ, these are the smooth vector fields withL_X σ = 0.TauCeti.SmoothTwoForm.mem_symplecticVectorFields_of_isHamiltonianVectorField: Hamiltonian vector fields are symplectic.TauCeti.SmoothTwoForm.interiorClass: the class[ι_X σ] ∈ H¹_dR(M).TauCeti.SmoothTwoForm.interiorClass_eq_zero_iff: the class vanishes exactly for Hamiltonian vector fields.TauCeti.SmoothTwoForm.IsNondegenerate.negHamiltonianₗ: the mapf ↦ -X_f.TauCeti.SmoothTwoForm.IsNondegenerate.exact_subtype_negHamiltonianₗ,TauCeti.SmoothTwoForm.IsNondegenerate.exact_negHamiltonianₗ_interiorClass,TauCeti.SmoothTwoForm.IsNondegenerate.interiorClass_surjective: exactness of the sequence.
References #
- D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017,
Section 3.1 (symplectic and Hamiltonian vector fields, and the exact sequence
0 → ℝ → C^∞(M) → symplectic vector fields → H¹(M; ℝ) → 0for connectedM). - A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Section 18 (Hamiltonian and symplectic vector fields).
Symplectic vector fields #
The symplectic vector fields of a two-form σ: the smooth vector fields X whose
contraction ι_X σ is a closed one-form. For a closed σ these are the smooth vector fields with
L_X σ = 0 (TauCeti.SmoothTwoForm.mem_symplecticVectorFields_iff_mlieDerivForm_eq_zero).
Instances For
A smooth vector field is symplectic exactly when its contraction is closed.
For a closed two-form, a smooth vector field is symplectic exactly when its Lie derivative
annihilates the form, L_X σ = 0.
A smooth vector field is Hamiltonian for a smooth 0-form precisely when its contraction
is the exterior derivative of that form.
Hamiltonian vector fields are symplectic: if ι_X σ = df for a smooth function f, then
ι_X σ is closed.
The de Rham class of a symplectic vector field: the class [ι_X σ] ∈ H¹_dR(M) of its
closed contraction.
Instances For
The class of a symplectic vector field is the class of its contraction.
A symplectic vector field has zero de Rham class precisely when its contraction is the
exterior derivative of a smooth 0-form.
A symplectic vector field has zero class [ι_X σ] exactly when it is the Hamiltonian vector
field of a smooth function.
The exact sequence of a nondegenerate form #
The map f ↦ -X_f from smooth functions, as smooth 0-forms, to symplectic vector fields.
When σ is moreover closed, the convention {f, g} = df(X_g) gives X_{{f, g}} = -[X_f, X_g],
and the sign makes this map compatible with the Lie brackets.
Instances For
The vector field of f ↦ -X_f is the negated Hamiltonian vector field of the function.
The contraction of -X_f is -df.
Exactness at the smooth functions: -X_f = 0 exactly when f is a closed 0-form, that
is, locally constant.
Exactness at the smooth functions, as exactness of the inclusion of closed 0-forms
followed by f ↦ -X_f.
Exactness at the symplectic vector fields: the symplectic vector fields with zero class
[ι_X σ] are exactly the fields -X_f.
Exactness at H¹_dR(M): every first de Rham class is the class [ι_X σ] of a symplectic
vector field, namely of X = (σ♭)⁻¹ α for a closed representative α.