p. 17 — degree-one hemi-bracket is a chain map
ProvedCatSymplectic.Hemistrict.hemi_chain_mapchain-complexhemi-bracketmultisymplectic-geometryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1
For Hamiltonian and smooth , the degree-one chain-map identities are
They make the bracket compatible with the complex differential on both degree-one summands.
Formalization Note The statement is on a finite-dimensional real normed space. The right hemi-bracket on a function and form is zero by definition. The paper's is Ω in Lean.
Preamble
import Mathlib import Definitions.Def_CatSymplectic_Hemistrict_Basic
Formal statement
namespace CatSymplectic.Hemistrict
theorem hemi_chain_map {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
[FiniteDimensional ℝ E] (Ω : Form E 3) (hΩ : IsNPlectic 2 Ω)
(F : hamSubmodule Ω) (f : smoothFns E) :
ContWeatherall.grad (hemiFn Ω F f) =
hemi Ω F (ContWeatherall.grad f) ∧
hemi Ω (ContWeatherall.grad f) F = 0 := by sorry
end CatSymplectic.Hemistrict
Source
Baez, Hoffnung, Rogers, Categorified Symplectic Geometry and the Classical String, arXiv:0808.0246v1, p. 17, paragraph preceding Theorem 4.3
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.