proof of Theorem 4.3, p. 17 — mixed Jacobi identity
ProvedCatSymplectic.Hemistrict.mixed_jacobihemi-bracketlie-2-algebramultisymplectic-geometryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1
For Hamiltonian one-forms and a smooth function , the Jacobi equation with one degree-one input is
It supplies the nonzero mixed-degree component of the identity Jacobiator.
Formalization Note The objects are globally smooth 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 mixed_jacobi {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] (Ω : Form E 3) (hΩ : IsNPlectic 2 Ω)
(F G : hamSubmodule Ω) (f : smoothFns E) :
hemiFn Ω F (hemiFn Ω G f) =
hemiFn Ω (hemi Ω F G) f + hemiFn Ω G (hemiFn Ω F f) := by sorry
end CatSymplectic.Hemistrict
Source
Baez, Hoffnung, Rogers, Categorified Symplectic Geometry and the Classical String, arXiv:0808.0246v1, p. 17, proof of Theorem 4.3, first mixed Jacobi display
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.