Theorems 1.1–1.3 — Symplectic polynomial modules and Hamiltonian application

Disproved

SymplecticFreeModules.symplecticFreeModulesMain

by ShouqiaoWang · Aug 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

hamiltonian-lie-algebraslie-algebraspolynomial-modulesrepresentation-theorysymplectic-lie-algebras

For every integer $\ell\ge2$ , prove that there is a concrete presentation of $\mathfrak{sp}_{2\ell}(\mathbb C)$ with its abelian maximal-parabolic nilradical and a single two-parameter family of polynomial representations

(C,\Phi)\longmapsto\tau(C,\Phi)

that realizes the source's explicit generator formulas and is free of rank one over the nilradical. For this same family, prove the complete isomorphism and weight-module classification, the simplicity criterion outside

\left\{\frac{\ell+1}{2}-\frac n2:n\in\mathbb Z_{>0}\right\},

the Noetherian, Artinian, and composition-factor conclusions at exceptional parameters, and the canonical Shen--Larsson Hamiltonian-module application, including its exact degree-weight spaces and simplicity properties. The existential witnesses are quantified only once, so every clause refers to the same presentation and the same representation family.

Preamble

import Definitions.Def_frame_2026_symplectic_free_modules_interfaces

Formal statement

namespace SymplecticFreeModules

open scoped TensorProduct

theorem symplecticFreeModulesMain
    (l : ℕ) (hl : 2 ≤ l) :
    ∃ P : GeneratorPresentation l,
      IsAbelianNilradicalSystem P ∧
        ∃ tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l),
          IsTauFamily P tau ∧
            HasCoreClassification P tau ∧
            HasExceptionalFiniteLength tau ∧
            HasCanonicalHamiltonianApplication tau := by sorry

end SymplecticFreeModules

Source

Yang Chen and Haijun Tan, Simple sp_{2l}(C)-modules which are free over an abelian nilradical, Journal of Algebra 697 (2026), 341–372, Theorems 1.1–1.3 on pp. 343–344; formal Theorems 3.7, 3.8, 4.7, 4.9, and 5.2: https://doi.org/10.1016/j.jalgebra.2026.02.022

View graph