Diagonal degree action gives the exact Laurent weight spaces

Proved

SymplecticFreeModules.canonicalDegreeWeightStructure

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

lie-algebrasrepresentation-theory

Let $l$ be a natural number and let $M$ be any complex vector space. Put $\Lambda=\mathbb Z^{2l}$ and let $A=\mathbb C[\Lambda]$ be its Laurent group algebra. Suppose $\sigma$ is a representation of the canonical Hamiltonian bracket on $M\otimes A$ , and $\beta\in\mathbb C^{2l}$ . Assume only the displayed degree action

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

for every coordinate $i$ , exponent $s\in\Lambda$ and vector $v\in M$ . Then the tensor module is spanned by simultaneous degree-weight vectors. Moreover, for every $s\in\Lambda$ , its simultaneous eigenspace of weight $s+\beta$ is exactly

\{v\otimes x^s:v\in M\}.

No simplicity, nontriviality, dimension restriction on $M$ , or formula for the other Hamiltonian generators is required. The result isolates the linear-algebra content of the weight assertions in the canonical Shen--Larsson application.

Preamble

import Definitions.Def_frame_2026_symplectic_free_modules_interfaces

open scoped TensorProduct

Formal statement

namespace SymplecticFreeModules

theorem canonicalDegreeWeightStructure {l : ℕ} {M : Type*} [AddCommGroup M] [Module ℂ M]
    (σ : CanonicalHamiltonianRepresentation l (M ⊗[ℂ] Laurent l))
    (beta : (Fin l ⊕ Fin l) → ℂ)
    (hd : ∀ i s v, σ (canonicalD i) (v ⊗ₜ[ℂ] laurentMonomial s) =
      (((s i : ℂ) + beta i) • v) ⊗ₜ[ℂ] laurentMonomial s) :
    IsCanonicalHamiltonianWeightRepresentation σ ∧
      HasCanonicalExactDegreeWeightSpaces σ beta := by sorry

end SymplecticFreeModules

Source

Structural consequence of the degree-derivation clause of HasCanonicalShenLarssonAction and the two weight definitions in https://prove2.me/theorems/11f584f1-dcb8-4e17-8e63-99c778b2b7c0 . Supports Chen--Tan, Journal of Algebra 697 (2026), Theorem 5.2, https://doi.org/10.1016/j.jalgebra.2026.02.022 .

View graph