iff and is constant
ProvedSymplecticFreeModules.parameterUniquenessThroughout, 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 determines exactly when two members of the family are isomorphic. For all scalars and polynomials ,
So the scalar is a genuine invariant of the isomorphism class, while the polynomial parameter matters only modulo constants: shifting 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 are parametrized precisely by the set of pairs .
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces
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