Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

The module is a weight module exactly when the parameter is constant

Proved
SymplecticFreeModules.weightRepresentationIffConstant

by Shuze Chen · Aug 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

lie-algebrasrepresentation-theorysymplectic-lie-algebraweight-modules

Let τ(c,φ)\tau(c,\varphi)τ(c,φ) be the family of sp2ℓ(C)\mathfrak{sp}_{2\ell}(\mathbb C)sp2ℓ​(C)-modules on C[Ti,j]\mathbb C[T_{i,j}]C[Ti,j​] determined by the displayed generator actions. Then τ(c,φ)\tau(c,\varphi)τ(c,φ) is a weight module — spanned by simultaneous eigenvectors of the diagonal generators Xi,iX_{i,i}Xi,i​ — if and only if the parameter φ\varphiφ 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 φ\varphiφ 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 φ\varphiφ the diagonal operator Xi,iX_{i,i}Xi,i​ acts on a monomial ∏Ta,bna,b\prod T_{a,b}^{n_{a,b}}∏Ta,bna,b​​ by the scalar c+∑kϵknk,ic+\sum_k \epsilon_k n_{k,i}c+∑k​ϵk​nk,i​, so the monomials are weight vectors and they span. The converse is the substantive one: a nonconstant φ\varphiφ contributes a multiplication operator X~i,iφ\widetilde X_{i,i}\varphiXi,i​φ 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.

Preamble
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces
Formal statement
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
Source
Y. Chen and H. Tan, Simple sp_{2l}(C)-modules which are free over an abelian nilradical, Journal of Algebra 697 (2026), 341-372; Theorem 1.1 and its formal counterparts Theorems 3.7 and 3.8. This is one of the two halves of the mission's weightCriterion node.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me