At exceptional , has finite length and Jordan--H\ddot{o}lder uniqueness
ProvedSymplecticFreeModules.exceptionalFiniteLengthThroughout, 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 describes what happens at the exceptional parameters, where simplicity fails. Let
and let be arbitrary. Then is still as well behaved as a nonsimple module can be: ascending and descending chains of invariant subspaces both stabilize, so the module is Noetherian and Artinian; it admits a finite composition series, that is a finite chain of invariant subspaces with no invariant subspace strictly between consecutive terms; and any two such composition series have the same length and isomorphic composition factors up to permutation, which is the Jordan–Hölder property.
The point is that the exceptional locus does not produce pathological infinite-length modules. Each decomposes into finitely many well-defined simple pieces, so the classification of the family extends to a description of the exceptional members in terms of their composition factors.
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces
namespace SymplecticFreeModules
open scoped TensorProduct
theorem exceptionalFiniteLength (l : ℕ) (hl : 2 ≤ l)
(P : GeneratorPresentation l) (hP : IsAbelianNilradicalSystem P)
(tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l))
(htau : IsTauFamily P tau) :
HasExceptionalFiniteLength tau := by sorry
end SymplecticFreeModules