is a weight module iff is constant
ProvedSymplecticFreeModules.weightCriterionThroughout, is the symplectic Lie algebra with , realized concretely as matrices. Inside a maximal parabolic subalgebra sits the abelian nilradical spanned by the symmetric matrix units , and is the polynomial algebra on the corresponding variables, which is a copy of .
The paper builds a two-parameter family of -module structures on , indexed by a scalar and a polynomial , written . Its defining property is that the generators act by the displayed explicit differential operators and that each acts by multiplication by the variable , so that is free of rank one over .
This theorem identifies which members of the family are weight modules and pins down the highest-weight-type structure in that case. Two assertions are made.
First, for every and ,
A nonconstant polynomial parameter therefore produces a module that is genuinely not a weight module, which is the reason such families fall outside the classical highest-weight theory.
Second, when is constant the constant polynomial is a lowest-weight cyclic generator of weight : it is annihilated by the diagonal negative-root vector and by the strictly lower generators with , the successive differences act on it by zero, the top Cartan generator acts by the scalar , and no proper invariant subspace contains it.
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces
namespace SymplecticFreeModules
open scoped TensorProduct
theorem weightCriterion (l : ℕ) (hl : 2 ≤ l)
(P : GeneratorPresentation l) (hP : IsAbelianNilradicalSystem P)
(tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l))
(htau : IsTauFamily P tau) :
(∀ c phi, IsWeightRepresentation P (tau c phi) ↔ IsConstant phi) ∧
(∀ c phi, IsConstant phi → HasLowestWeightGenerator P (tau c phi) c) := by
sorry
end SymplecticFreeModules