Construction of the canonical Shen–Larsson action for any symplectic module

Proved

SymplecticFreeModules.canonicalShenLarssonActionExists

by Wenqian · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

lie-algebrasrepresentation-theory

Let $l$ be any nonnegative integer, let $M$ be a complex vector space, and let $\rho:\mathfrak{sp}_{2l}(\mathbb C)\to\operatorname{End}_{\mathbb C}(M)$ be a Lie-algebra representation. Write $\Lambda=\mathbb Z^{2l}$ and $A=\mathbb C[\Lambda]$ , and fix $\alpha,\beta\in\mathbb C^{2l}$ . The canonical Hamiltonian bracket admits a representation $\sigma$ on $M\otimes A$ with

\sigma(h_r)(v\otimes x^s)=\big(\langle\widetilde r,s+\alpha\rangle v+\rho(r\widetilde r^t)v\big)\otimes x^{r+s},

\sigma(d_i)(v\otimes x^s)=(s_i+\beta_i)v\otimes x^s.

Here $\widetilde r$ exchanges the two coordinate blocks and negates the second block, and $h_0=0$ . The rank-one matrix $r\widetilde r^t$ belongs to the symplectic Lie algebra. No simplicity, nontriviality, or finite-dimensionality assumption on $M$ is required. This isolates the action-construction part of the canonical Shen–Larsson application.

Preamble

import Definitions.Def_frame_2026_symplectic_free_modules_interfaces

open scoped TensorProduct

Formal statement

namespace SymplecticFreeModules

theorem canonicalShenLarssonActionExists {l : ℕ} {M : Type*} [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation (Sp l) M)
    (alpha beta : (Fin l ⊕ Fin l) → ℂ) :
    ∃ sigma : CanonicalHamiltonianRepresentation l (M ⊗[ℂ] Laurent l),
      HasCanonicalShenLarssonAction rho alpha beta sigma := by sorry

end SymplecticFreeModules

Source

Direct structural consequence of the exact canonical bracket and action formulas in https://prove2.me/theorems/11f584f1-dcb8-4e17-8e63-99c778b2b7c0 ; the specialized application is https://prove2.me/theorems/62f41608-35d7-45da-9f92-c7d499abc672 . The general statement here is the action construction, with no simplicity claim.

View graph