Lie brackets of Hamiltonian vector fields

Let σ be a closed two-form on a manifold M, with the convention ι_X σ = df for a Hamiltonian vector field X of f. If X and Y are differentiable Hamiltonian vector fields of C² functions f and g, then

d(σ(X, Y)) = -ι_{[X, Y]} σ,

so the Lie bracket [X, Y] is a Hamiltonian vector field of -σ(X, Y) (TauCeti.SmoothTwoForm.IsHamiltonianVectorField.mvfderiv_eval₂ and TauCeti.SmoothTwoForm.IsHamiltonianVectorField.mlieBracket). No nondegeneracy is needed.

More generally, the Lie bracket of two symplectic vector fields X and Y, that is smooth vector fields with closed contractions ι_X σ and ι_Y σ, is a Hamiltonian vector field of σ(Y, X) (TauCeti.SmoothTwoForm.isHamiltonianVectorField_mlieBracket), although X and Y themselves need not be Hamiltonian.

For a nondegenerate closed form on a finite-dimensional manifold, where the Poisson bracket is {f, g} = σ(X_f, X_g) = df(X_g), this says

X_{{f, g}} = -[X_f, X_g]

(TauCeti.SmoothTwoForm.IsNondegenerate.hamiltonianVectorField_poissonBracket): the map f ↦ -X_f takes Poisson brackets to Lie brackets of vector fields. It gives the identity {f, {g, k}} = {{f, g}, k} - {{f, k}, g} and the Jacobi identity {f, {g, k}} + {g, {k, f}} + {k, {f, g}} = 0 for C² functions (TauCeti.SmoothTwoForm.IsNondegenerate.poissonBracket_poissonBracket and TauCeti.SmoothTwoForm.IsNondegenerate.poissonBracket_jacobi).

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.1 (Lie brackets of symplectic and Hamiltonian vector fields, and the Poisson bracket).
• A. Cannas da Silva, Lectures on Symplectic Geometry, Lecture Notes in Mathematics 1764, Springer, 2001, Section 18.3 (the Poisson bracket and its Jacobi identity).

theorem TauCeti.SmoothTwoForm.IsHamiltonianVectorField.mvfderiv_eval₂ {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {σ : SmoothTwoForm I M} {f g : M → ℝ} {X Y : (x : M) → TangentSpace I x} {x : M} [CompleteSpace E] (hσ : SmoothForm.IsClosed σ) (hX : σ.IsHamiltonianVectorField f X) (hY : σ.IsHamiltonianVectorField g Y) (hf : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 2 f x) (hg : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 2 g x) (hX' : (MDiffAt fun (y : M) => ⟨y, X y⟩) x) (hY' : (MDiffAt fun (y : M) => ⟨y, Y y⟩) x) (v : TangentSpace I x) : ((d% fun (y : M) => SmoothBundleForm.eval₂ σ y (X y) (Y y)) x) v = -SmoothBundleForm.eval₂ σ x (VectorField.mlieBracket I X Y x) v

For a closed form σ and Hamiltonian vector fields X of f and Y of g, with f and g of class C² and X, Y differentiable at x, the differential of σ(X, Y) at x is -ι_{[X, Y]} σ.

theorem TauCeti.SmoothTwoForm.IsHamiltonianVectorField.mlieBracket {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {σ : SmoothTwoForm I M} {f g : M → ℝ} {X Y : (x : M) → TangentSpace I x} [CompleteSpace E] (hσ : SmoothForm.IsClosed σ) (hX : σ.IsHamiltonianVectorField f X) (hY : σ.IsHamiltonianVectorField g Y) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 g) (hX' : MDiff fun (y : M) => ⟨y, X y⟩) (hY' : MDiff fun (y : M) => ⟨y, Y y⟩) : σ.IsHamiltonianVectorField (fun (y : M) => -SmoothBundleForm.eval₂ σ y (X y) (Y y)) (VectorField.mlieBracket I X Y)

The Lie bracket of Hamiltonian vector fields is Hamiltonian. For a closed form σ and differentiable Hamiltonian vector fields X of f and Y of g, with f and g of class C², the bracket [X, Y] is a Hamiltonian vector field of -σ(X, Y).

theorem TauCeti.SmoothTwoForm.isHamiltonianVectorField_mlieBracket {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {σ : SmoothTwoForm I M} (hσ : SmoothForm.IsClosed σ) {X Y : ContMDiffSection I E (↑⊤) (TangentSpace I)} (hX : X ∈ σ.symplecticVectorFields) (hY : Y ∈ σ.symplecticVectorFields) : σ.IsHamiltonianVectorField (fun (x : M) => SmoothBundleForm.eval₂ σ x (Y x) (X x)) (VectorField.mlieBracket I ⇑X ⇑Y)

The bracket of symplectic vector fields is Hamiltonian. For a closed two-form σ and smooth vector fields X, Y with closed contractions, [X, Y] is a Hamiltonian vector field of σ(Y, X): ι_{[X, Y]} σ = d(σ(Y, X)).

theorem TauCeti.SmoothTwoForm.IsNondegenerate.hamiltonianVectorField_poissonBracket {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {σ : SmoothTwoForm I M} {f g : M → ℝ} [FiniteDimensional ℝ E] (h : σ.IsNondegenerate) (hσ : SmoothForm.IsClosed σ) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 g) : σ.hamiltonianVectorField (σ.poissonBracket f g) = -VectorField.mlieBracket I (σ.hamiltonianVectorField f) (σ.hamiltonianVectorField g)

For a nondegenerate closed form on a finite-dimensional manifold, the Hamiltonian vector field of the Poisson bracket of two C² functions is X_{{f, g}} = -[X_f, X_g].

theorem TauCeti.SmoothTwoForm.IsNondegenerate.poissonBracket_poissonBracket {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {σ : SmoothTwoForm I M} {f g : M → ℝ} [FiniteDimensional ℝ E] (h : σ.IsNondegenerate) (hσ : SmoothForm.IsClosed σ) {k : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 g) (hk : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 k) (x : M) : σ.poissonBracket f (σ.poissonBracket g k) x = σ.poissonBracket (σ.poissonBracket f g) k x - σ.poissonBracket (σ.poissonBracket f k) g x

For a nondegenerate closed form on a finite-dimensional manifold, the Poisson bracket of C² functions satisfies {f, {g, k}} = {{f, g}, k} - {{f, k}, g}.

theorem TauCeti.SmoothTwoForm.IsNondegenerate.poissonBracket_jacobi {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {σ : SmoothTwoForm I M} {f g : M → ℝ} [FiniteDimensional ℝ E] (h : σ.IsNondegenerate) (hσ : SmoothForm.IsClosed σ) {k : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f) (hg : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 g) (hk : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 k) (x : M) : σ.poissonBracket f (σ.poissonBracket g k) x + σ.poissonBracket g (σ.poissonBracket k f) x + σ.poissonBracket k (σ.poissonBracket f g) x = 0

The Jacobi identity for the Poisson bracket. For a nondegenerate closed form on a finite-dimensional manifold and C² functions f, g, k, {f, {g, k}} + {g, {k, f}} + {k, {f, g}} = 0.