Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

τ(c1,φ1)≅τ(c2,φ2)\tau(c_1,\varphi_1)\cong\tau(c_2,\varphi_2)τ(c1​,φ1​)≅τ(c2​,φ2​) iff c1=c2c_1=c_2c1​=c2​ and φ1−φ2\varphi_1-\varphi_2φ1​−φ2​ is constant

Proved
SymplecticFreeModules.parameterUniqueness

by Shuze Chen · Aug 27, 2026 · Mathlib c5ea003 (Lean v4.30.0)

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 determines exactly when two members of the family are isomorphic. For all scalars c1,c2c_1,c_2c1​,c2​ and polynomials φ1,φ2\varphi_1,\varphi_2φ1​,φ2​,

τ(c1,φ1)  ≅  τ(c2,φ2)⟺c1=c2  and  φ1−φ2  is constant.\tau(c_1,\varphi_1)\;\cong\;\tau(c_2,\varphi_2) \quad\Longleftrightarrow\quad c_1=c_2 \ \text{ and } \ \varphi_1-\varphi_2 \ \text{ is constant}.τ(c1​,φ1​)≅τ(c2​,φ2​)⟺c1​=c2​  and  φ1​−φ2​  is constant.

So the scalar ccc is a genuine invariant of the isomorphism class, while the polynomial parameter matters only modulo constants: shifting φ\varphiφ by a scalar changes the operators but not the module. Combined with exhaustiveness, this says that the isomorphism classes of modules free of rank one over U(n)U(\mathfrak{n})U(n) are parametrized precisely by the set of pairs (c,φ mod C)(c, \varphi \bmod \mathbb{C})(c,φmodC).

Preamble
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces
Formal statement
namespace SymplecticFreeModules

open scoped TensorProduct

theorem parameterUniqueness (l : ℕ) (hl : 2 ≤ l)
    (P : GeneratorPresentation l) (hP : IsAbelianNilradicalSystem P)
    (tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l))
    (htau : IsTauFamily P tau) :
    ∀ c₁ phi₁ c₂ phi₂,
      LieRepEquivalent (tau c₁ phi₁) (tau c₂ phi₂) ↔
        c₁ = c₂ ∧ IsConstant (phi₁ - phi₂) := 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 and its formal counterpart Theorem 3.8 (isomorphism criterion for the parameters). This child isolates the second clause 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