Proposition 3.6(1), p. 12 — closure of the hemi-bracket
ProvedCatSymplectic.Hemistrict.proposition_3_6_1hamiltonian-vector-fieldshemi-bracketmultisymplectic-geometryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1
For Hamiltonian one-forms , the hemi-bracket is Hamiltonian and its vector field is their vector-field bracket:
This supplies closure and identifies the field of a nested bracket.
Formalization Note This is the case on a finite-dimensional real normed space. The paper's is Ω in Lean.
Preamble
import Mathlib import Definitions.Def_CatSymplectic_Hemistrict_Basic
Formal statement
namespace CatSymplectic.Hemistrict
theorem proposition_3_6_1 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] (Ω : Form E 3) (hΩ : IsNPlectic 2 Ω)
(F G : hamSubmodule Ω) :
hemi Ω F G ∈ hamSubmodule Ω ∧
IsHamVF Ω (hemi Ω F G)
(VectorField.lieBracket ℝ (hamVF Ω F) (hamVF Ω G)) ∧
hamVF Ω (hemi Ω F G) =
VectorField.lieBracket ℝ (hamVF Ω F) (hamVF Ω G) := by sorry
end CatSymplectic.Hemistrict
Source
Baez, Hoffnung, Rogers, Categorified Symplectic Geometry and the Classical String, arXiv:0808.0246v1, pp. 11–12, Proposition 3.6 part 1, equation (6)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.