proof of Theorem 4.3, p. 17 — third coherence diagram
ProvedCatSymplectic.Hemistrict.diagram_threecoherencelie-2-algebramultisymplectic-geometryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1
For Hamiltonian one-forms , the alternator and hemi-bracket satisfy
This is the nonzero content of the third coherence diagram of the hemistrict construction.
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 diagram_three {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] (Ω : Form E 3) (hΩ : IsNPlectic 2 Ω)
(F G H : hamSubmodule Ω) :
alt Ω (hemi Ω F G) H + alt Ω G (hemi Ω F H) =
hemiFn Ω F (alt Ω G H) := 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, third-diagram display
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.