The module is a weight module exactly when the parameter is constant
ProvedSymplecticFreeModules.weightRepresentationIffConstantLet be the family of -modules on determined by the displayed generator actions. Then is a weight module — spanned by simultaneous eigenvectors of the diagonal generators — if and only if the parameter is a constant polynomial.
Role. This is the dichotomy that makes the family genuinely new. The classical modules parabolically induced from a character are weight modules, and they are exactly the members of the family with constant parameter; every nonconstant produces a module that is free of rank one over the nilradical yet carries no basis of weight vectors, so it lies outside the weight-module theory entirely. That the same two-parameter family contains both is what allows a single classification to cover the weight and non-weight cases at once.
The easy direction is a computation: for constant the diagonal operator acts on a monomial by the scalar , so the monomials are weight vectors and they span. The converse is the substantive one: a nonconstant contributes a multiplication operator that is not scalar on any monomial basis, and one has to rule out every other spanning set of eigenvectors, not merely the obvious one.
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces
namespace SymplecticFreeModules
open scoped TensorProduct
theorem weightRepresentationIffConstant (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 := by sorry
end SymplecticFreeModules