Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

τ(c,φ)\tau(c,\varphi)τ(c,φ) is a weight module iff φ\varphiφ is constant

Proved
SymplecticFreeModules.weightCriterion

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

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

Throughout, sp2l(C)\mathfrak{sp}_{2l}(\mathbb{C})sp2l​(C) is the symplectic Lie algebra with l≥2l \ge 2l≥2, realized concretely as 2l×2l2l\times 2l2l×2l matrices. Inside a maximal parabolic subalgebra sits the abelian nilradical n\mathfrak{n}n spanned by the symmetric matrix units Ti,j=Tj,iT_{i,j}=T_{j,i}Ti,j​=Tj,i​, and A=C[Ti,j:i≤j]A = \mathbb{C}[T_{i,j} : i \le j]A=C[Ti,j​:i≤j] is the polynomial algebra on the corresponding variables, which is a copy of U(n)U(\mathfrak{n})U(n).

The paper builds a two-parameter family of sp2l(C)\mathfrak{sp}_{2l}(\mathbb{C})sp2l​(C)-module structures on AAA, indexed by a scalar c∈Cc \in \mathbb{C}c∈C and a polynomial φ∈A\varphi \in Aφ∈A, written τ(c,φ)\tau(c,\varphi)τ(c,φ). Its defining property is that the generators act by the displayed explicit differential operators and that each Ti,jT_{i,j}Ti,j​ acts by multiplication by the variable Ti,jT_{i,j}Ti,j​, so that τ(c,φ)\tau(c,\varphi)τ(c,φ) is free of rank one over U(n)U(\mathfrak{n})U(n).

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 ccc and φ\varphiφ,

τ(c,φ) is spanned by simultaneous eigenvectors of the Cartan generators⟺φ is constant.\tau(c,\varphi) \text{ is spanned by simultaneous eigenvectors of the Cartan generators} \quad\Longleftrightarrow\quad \varphi \text{ is constant}.τ(c,φ) is spanned by simultaneous eigenvectors of the Cartan generators⟺φ is constant.

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 φ\varphiφ is constant the constant polynomial 1∈A1 \in A1∈A is a lowest-weight cyclic generator of weight cΛlc\Lambda_lcΛl​: it is annihilated by the diagonal negative-root vector Yl,lY_{l,l}Yl,l​ and by the strictly lower generators Xi,jX_{i,j}Xi,j​ with j+1=ij+1=ij+1=i, the successive differences Xi,i−Xj,jX_{i,i}-X_{j,j}Xi,i​−Xj,j​ act on it by zero, the top Cartan generator acts by the scalar ccc, and no proper invariant subspace contains it.

Preamble
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces
Formal statement
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
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, https://doi.org/10.1016/j.jalgebra.2026.02.022, Theorem 1.1 on pp. 343-344 (weight-module criterion and lowest-weight generator of weight c*Lambda_l). This child isolates the third and fourth clauses of `HasCoreClassification` in the mission goal statement.

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