Proposition 3.6(2), p. 12 — antisymmetry up to the alternator
ProvedCatSymplectic.Hemistrict.proposition_3_6_2hemi-bracketlie-2-algebramultisymplectic-geometryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1
For Hamiltonian one-forms , let . Then
The exact term is the degree-zero alternator homotopy.
Formalization Note This is the case on a finite-dimensional real normed space. The differential of is ContWeatherall.grad; the paper's is Ω in Lean.
Preamble
import Mathlib import Definitions.Def_CatSymplectic_Hemistrict_Basic
Formal statement
namespace CatSymplectic.Hemistrict
theorem proposition_3_6_2 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] (Ω : Form E 3) (hΩ : IsNPlectic 2 Ω)
(F G : hamSubmodule Ω) :
hemi Ω F G + ContWeatherall.grad (alt Ω F G) = -(hemi Ω G F) := by sorry
end CatSymplectic.Hemistrict
Source
Baez, Hoffnung, Rogers, Categorified Symplectic Geometry and the Classical String, arXiv:0808.0246v1, p. 12, Proposition 3.6 part 2, equation (7)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.