Polynomial symplectic-module and Hamiltonian-module interfaces

Definition

frame_2026_symplectic_free_modules_interfaces

by ShouqiaoWang · Aug 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

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

This bundle defines a concrete presentation of the complex symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$ , its abelian maximal-parabolic nilradical, multivariate polynomial carriers, Lie representations, and the two-parameter candidate action $\tau(C,\Phi)$ . It formalizes the explicit generator formulas, freeness of rank one over the nilradical, isomorphism and weight-module criteria, the exceptional simplicity set, Noetherian/Artinian finite-length behavior, and a canonical Hamiltonian Lie-algebra application with exact degree-weight spaces. These are proof obligations about actual linear maps and brackets, not arbitrary semantic predicates.

Definition code

import Mathlib

/-!
# Interfaces for polynomial modules over the symplectic Lie algebra

The candidate differential operators are defined concretely on a multivariate
polynomial ring.  A `LieRepresentation` is a Lie homomorphism into linear
endomorphisms.  Crucially, no representation satisfying the candidate formulas
is installed in this file: its existence is part of the theorem target.
-/

namespace SymplecticFreeModules

open scoped TensorProduct

/-- Unordered pairs index the variables `T_{i,j}=T_{j,i}`. -/
def SymmetricIndex (l : ℕ) :=
  {ij : Fin l × Fin l // ij.1 ≤ ij.2}

/-- The ordered representative of the unordered pair `{i,j}`. -/
def symmetricIndex {l : ℕ} (i j : Fin l) : SymmetricIndex l :=
  if h : i ≤ j then ⟨(i, j), h⟩ else ⟨(j, i), le_of_not_ge h⟩

/-- The polynomial algebra in the symmetric variables `T_{i,j}`. -/
abbrev Poly (l : ℕ) := MvPolynomial (SymmetricIndex l) ℂ

/-- The variable `T_{i,j}`, with the indices automatically symmetrized. -/
noncomputable def T {l : ℕ} (i j : Fin l) : Poly l :=
  MvPolynomial.X (symmetricIndex i j)

/-- Formal partial differentiation with respect to `T_{i,j}`. -/
noncomputable def partialDeriv {l : ℕ} (i j : Fin l) :
    Derivation ℂ (Poly l) (Poly l) :=
  MvPolynomial.pderiv (symmetricIndex i j)

/-- The paper's operator `\widetilde X_{i,j}`. -/
noncomputable def xTilde {l : ℕ} (i j : Fin l) (q : Poly l) : Poly l :=
  ∑ k : Fin l,
    MvPolynomial.C (if k = i then (2 : ℂ) else 1) *
      T k i * partialDeriv k j q

/-- The paper's operator `\widetilde Y_{i,j}`, with its parameter displayed. -/
noncomputable def yTilde {l : ℕ} (c : ℂ) (i j : Fin l)
    (q : Poly l) : Poly l :=
  MvPolynomial.C (2 * c) * partialDeriv i j q +
    ∑ k : Fin l, xTilde k i (partialDeriv k j q)

/-- The proposed action of `X_{i,j}` in `tau(c,phi)`. -/
noncomputable def xCandidate {l : ℕ} (c : ℂ) (phi : Poly l)
    (i j : Fin l) (q : Poly l) : Poly l :=
  xTilde i j q +
    (xTilde i j phi + if i = j then MvPolynomial.C c else 0) * q

/-- The proposed multiplication action of `T_{i,j}`. -/
noncomputable def tCandidate {l : ℕ} (i j : Fin l) (q : Poly l) : Poly l :=
  T i j * q

/-- The proposed action of the diagonal negative-root vector `Y_{i,i}`. -/
noncomputable def yDiagonalCandidate {l : ℕ} (c : ℂ) (phi : Poly l)
    (i : Fin l) (q : Poly l) : Poly l :=
  -(1 / 2 : ℂ) •
    (yTilde c i i phi * q + yTilde c i i q +
      ∑ k : Fin l,
        xTilde k i phi * (partialDeriv k i phi * q + 2 • partialDeriv k i q))

/-- Mathlib's concrete `sp_{2l}(C)`, indexed by two copies of `Fin l`. -/
abbrev Sp (l : ℕ) := LieAlgebra.Symplectic.sp (Fin l) ℂ

/-- The matrix called `X_{i,j}` in the paper. -/
def xMatrix {l : ℕ} (i j : Fin l) :
    Matrix (Fin l ⊕ Fin l) (Fin l ⊕ Fin l) ℂ :=
  Matrix.single (Sum.inl i) (Sum.inl j) 1 -
    Matrix.single (Sum.inr j) (Sum.inr i) 1

/-- The matrix called `Y_{i,i}` in the paper. -/
def yDiagonalMatrix {l : ℕ} (i : Fin l) :
    Matrix (Fin l ⊕ Fin l) (Fin l ⊕ Fin l) ℂ :=
  Matrix.single (Sum.inr i) (Sum.inl i) 1

/-- The symmetric upper-right matrix called `T_{i,j}` in the paper. -/
def tMatrix {l : ℕ} (i j : Fin l) :
    Matrix (Fin l ⊕ Fin l) (Fin l ⊕ Fin l) ℂ :=
  if i = j then Matrix.single (Sum.inl i) (Sum.inr i) 1
  else
    Matrix.single (Sum.inl i) (Sum.inr j) 1 +
      Matrix.single (Sum.inl j) (Sum.inr i) 1

/--
Named generators in the concrete symplectic Lie algebra.  The value fields pin
them to the paper's matrices and do not assert that the candidate operators
form a representation.
-/
structure GeneratorPresentation (l : ℕ) where
  Xgen : Fin l → Fin l → Sp l
  YdiagGen : Fin l → Sp l
  Tgen : Fin l → Fin l → Sp l
  Xgen_value : ∀ i j, (Xgen i j : Matrix (Fin l ⊕ Fin l) (Fin l ⊕ Fin l) ℂ) =
    xMatrix i j
  YdiagGen_value : ∀ i, (YdiagGen i : Matrix (Fin l ⊕ Fin l) (Fin l ⊕ Fin l) ℂ) =
    yDiagonalMatrix i
  Tgen_value : ∀ i j, (Tgen i j : Matrix (Fin l ⊕ Fin l) (Fin l ⊕ Fin l) ℂ) =
    tMatrix i j

/-- The displayed `T_{i,j}` form the expected independent abelian system. -/
def IsAbelianNilradicalSystem {l : ℕ} (P : GeneratorPresentation l) : Prop :=
  (∀ i j k m, ⁅P.Tgen i j, P.Tgen k m⁆ = 0) ∧
  LinearIndependent ℂ
    (fun ij : SymmetricIndex l ↦ P.Tgen ij.1.1 ij.1.2)

/-- A representation of a complex Lie algebra as linear endomorphisms. -/
abbrev LieRepresentation (L M : Type*) [LieRing L] [LieAlgebra ℂ L]
    [AddCommGroup M] [Module ℂ M] :=
  L →ₗ⁅ℂ⁆ Module.End ℂ M

/-- The representation has exactly the generator actions displayed in the paper. -/
def HasGeneratorAction {l : ℕ} (P : GeneratorPresentation l)
    (rho : LieRepresentation (Sp l) (Poly l)) (c : ℂ) (phi : Poly l) : Prop :=
  (∀ i j q, rho (P.Xgen i j) q = xCandidate c phi i j q) ∧
  (∀ i j q, rho (P.Tgen i j) q = tCandidate i j q) ∧
  (∀ i q, rho (P.YdiagGen i) q = yDiagonalCandidate c phi i q)

/-- Intertwining equivalence of two Lie representations. -/
def LieRepEquivalent {L M N : Type*} [LieRing L] [LieAlgebra ℂ L]
    [AddCommGroup M] [Module ℂ M] [AddCommGroup N] [Module ℂ N]
    (rho : LieRepresentation L M) (sigma : LieRepresentation L N) : Prop :=
  ∃ e : M ≃ₗ[ℂ] N, ∀ x m, e (rho x m) = sigma x (e m)

/--
Concrete rank-one freeness over the abelian nilradical: after choosing the
free generator, every `T_{i,j}` acts as multiplication by its polynomial
variable.  This is equivalent to rank-one freeness over `U(n)` here.
-/
def IsFreeRankOneOverNilradical {l : ℕ} (P : GeneratorPresentation l)
    {M : Type*} [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation (Sp l) M) : Prop :=
  ∃ e : Poly l ≃ₗ[ℂ] M,
    ∀ i j q, e (T i j * q) = rho (P.Tgen i j) (e q)

/-- A subspace invariant under a Lie representation. -/
def IsInvariant {L M : Type*} [LieRing L] [LieAlgebra ℂ L]
    [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) (S : Submodule ℂ M) : Prop :=
  ∀ x m, m ∈ S → rho x m ∈ S

/-- Simplicity expressed without installing a new module typeclass. -/
def IsSimpleRepresentation {L M : Type*} [LieRing L] [LieAlgebra ℂ L]
    [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) : Prop :=
  Nontrivial M ∧ ∀ S : Submodule ℂ M,
    IsInvariant rho S → S = ⊥ ∨ S = ⊤

/-- A simultaneous weight vector for the diagonal Cartan generators. -/
def IsWeightVector {l : ℕ} (P : GeneratorPresentation l)
    {M : Type*} [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation (Sp l) M) (v : M) : Prop :=
  ∃ lambda : Fin l → ℂ, ∀ i, rho (P.Xgen i i) v = lambda i • v

/-- The module is spanned by its simultaneous weight vectors. -/
def IsWeightRepresentation {l : ℕ} (P : GeneratorPresentation l)
    {M : Type*} [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation (Sp l) M) : Prop :=
  Submodule.span ℂ {v : M | IsWeightVector P rho v} = ⊤

/--
For a constant parameter `phi`, the polynomial `1` is the lowest-weight
cyclic generator of weight `c Λ_l`, written only with the concrete generators.
-/
def HasLowestWeightGenerator {l : ℕ} (P : GeneratorPresentation l)
    (rho : LieRepresentation (Sp l) (Poly l)) (c : ℂ) : Prop :=
  ∃ last : Fin l,
    last.1 + 1 = l ∧
    rho (P.YdiagGen last) 1 = 0 ∧
    rho (P.Xgen last last) 1 = c • (1 : Poly l) ∧
    (∀ i j : Fin l, i.1 + 1 = j.1 →
      rho (P.Xgen i i - P.Xgen j j) 1 = 0) ∧
    (∀ i j : Fin l, j.1 + 1 = i.1 → rho (P.Xgen i j) 1 = 0) ∧
    (∀ S : Submodule ℂ (Poly l),
      IsInvariant rho S → (1 : Poly l) ∈ S → S = ⊤)

/-- A multivariate polynomial is constant. -/
def IsConstant {l : ℕ} (phi : Poly l) : Prop :=
  ∃ c : ℂ, phi = MvPolynomial.C c

/-- The exceptional simplicity parameters `(l+1)/2 - n/2`, `n >= 1`. -/
def IsExceptional (l : ℕ) (c : ℂ) : Prop :=
  ∃ n : ℕ, 0 < n ∧
    c = (((l + 1 : ℕ) : ℂ) / 2 - (n : ℂ) / 2)

/-- Ascending chains of invariant subspaces stabilize. -/
def IsNoetherianRepresentation {L M : Type*} [LieRing L] [LieAlgebra ℂ L]
    [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) : Prop :=
  ∀ S : ℕ → Submodule ℂ M,
    (∀ n, IsInvariant rho (S n)) →
    Monotone S → ∃ n₀, ∀ n, n₀ ≤ n → S n = S n₀

/-- Descending chains of invariant subspaces stabilize. -/
def IsArtinianRepresentation {L M : Type*} [LieRing L] [LieAlgebra ℂ L]
    [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) : Prop :=
  ∀ S : ℕ → Submodule ℂ M,
    (∀ n, IsInvariant rho (S n)) →
    Antitone S → ∃ n₀, ∀ n, n₀ ≤ n → S n = S n₀

/-- No invariant subspace lies strictly between `S` and `T`. -/
def IsCompositionStep {L M : Type*} [LieRing L] [LieAlgebra ℂ L]
    [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) (S T : Submodule ℂ M) : Prop :=
  IsInvariant rho S ∧ IsInvariant rho T ∧ S < T ∧
    ∀ U : Submodule ℂ M,
      IsInvariant rho U → S ≤ U → U ≤ T → U = S ∨ U = T

/-- A finite composition series with a specified length and chain. -/
def IsFiniteCompositionSeries {L M : Type*} [LieRing L] [LieAlgebra ℂ L]
    [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) (s : ℕ) (S : ℕ → Submodule ℂ M) : Prop :=
  0 < s ∧ S 0 = ⊥ ∧ S s = ⊤ ∧
    ∀ i, i < s → IsCompositionStep rho (S i) (S (i + 1))

/-- A finite composition series, encoded by its successive invariant subspaces. -/
def HasFiniteCompositionSeries {L M : Type*} [LieRing L] [LieAlgebra ℂ L]
    [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) : Prop :=
  ∃ s : ℕ, ∃ S : ℕ → Submodule ℂ M, IsFiniteCompositionSeries rho s S

/-- Restriction of a Lie action to an invariant subspace. -/
noncomputable def invariantRestrictedAction {L M : Type*}
    [LieRing L] [LieAlgebra ℂ L] [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) (T : Submodule ℂ M)
    (hT : IsInvariant rho T) (x : L) : Module.End ℂ T where
  toFun t := ⟨rho x t.1, hT x t.1 t.2⟩
  map_add' a b := by
    ext
    exact (rho x).map_add a.1 b.1
  map_smul' c a := by
    ext
    exact (rho x).map_smul c a.1

/-- The induced action on the concrete subquotient `T/S`. -/
noncomputable def compositionFactorAction {L M : Type*}
    [LieRing L] [LieAlgebra ℂ L] [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) (S T : Submodule ℂ M)
    (hS : IsInvariant rho S) (hT : IsInvariant rho T) (x : L) :
    Module.End ℂ (T ⧸ S.comap T.subtype) :=
  (S.comap T.subtype).mapQ (S.comap T.subtype)
    (invariantRestrictedAction rho T hT x) (by
      intro t ht
      exact hS x t.1 ht)

/-- Two composition factors are isomorphic as genuine quotient
representations. -/
def CompositionFactorsEquivalent {L M : Type*}
    [LieRing L] [LieAlgebra ℂ L] [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M)
    (S T U V : Submodule ℂ M) : Prop :=
  S ≤ T ∧ U ≤ V ∧
    ∃ (hS : IsInvariant rho S) (hT : IsInvariant rho T)
      (hU : IsInvariant rho U) (hV : IsInvariant rho V)
      (e : (T ⧸ S.comap T.subtype) ≃ₗ[ℂ]
        (V ⧸ U.comap V.subtype)),
      ∀ x q,
        e (compositionFactorAction rho S T hS hT x q) =
          compositionFactorAction rho U V hU hV x (e q)

/-- Jordan--Hölder uniqueness: any two finite composition series have the
same simple factors up to a permutation and representation isomorphism. -/
def HasJordanHolderUniqueness {L M : Type*}
    [LieRing L] [LieAlgebra ℂ L] [AddCommGroup M] [Module ℂ M]
    (rho : LieRepresentation L M) : Prop :=
  ∀ (s t : ℕ) (S T : ℕ → Submodule ℂ M),
    IsFiniteCompositionSeries rho s S →
    IsFiniteCompositionSeries rho t T →
      ∃ permutation : Fin s ≃ Fin t,
        ∀ i : Fin s,
          CompositionFactorsEquivalent rho
            (S i.1) (S (i.1 + 1))
            (T (permutation i).1) (T ((permutation i).1 + 1))

/-- Exponent vectors for Laurent monomials in `2l` variables. -/
abbrev Exponent (l : ℕ) := (Fin l ⊕ Fin l) → ℤ

/-- Laurent polynomials as the group algebra of the exponent lattice. -/
abbrev Laurent (l : ℕ) := AddMonoidAlgebra ℂ (Exponent l)

/-- The exponent vector `\widetilde r`. -/
def tildeExponent {l : ℕ} (r : Exponent l) : Exponent l
  | Sum.inl i => r (Sum.inr i)
  | Sum.inr i => -r (Sum.inl i)

/-- A Laurent monomial `x^r`. -/
noncomputable def laurentMonomial {l : ℕ} (r : Exponent l) : Laurent l :=
  AddMonoidAlgebra.single r 1

/-- The complex bilinear dot product, coercing the first integer vector. -/
noncomputable def exponentDot {l : ℕ} (r : Exponent l)
    (a : (Fin l ⊕ Fin l) → ℂ) : ℂ :=
  ∑ i : Fin l ⊕ Fin l, (r i : ℂ) * a i

/-- The outer-product matrix `r \widetilde r^t`. -/
def outerMatrix {l : ℕ} (r : Exponent l) :
    Matrix (Fin l ⊕ Fin l) (Fin l ⊕ Fin l) ℂ :=
  fun i j ↦ (r i : ℂ) * (tildeExponent r j : ℂ)

/-!
## The canonical Hamiltonian Lie algebra, without an arbitrary quotient

The definitions below build the vector-space carrier and its bracket directly
from the basis used in the paper.  Establishing bilinearity and Jacobi for this
explicit bracket is part of the theorem target, rather than an input axiom.
-/

/-- Nonzero lattice exponents indexing the Hamiltonian generators
`\widetilde h_r`; the paper declares `\widetilde h_0 = 0`. -/
abbrev NonzeroExponent (l : ℕ) := {r : Exponent l // r ≠ 0}

/-- Basis labels: Hamiltonian monomial derivations and the degree derivations. -/
abbrev HamiltonianBasis (l : ℕ) := NonzeroExponent l ⊕ (Fin l ⊕ Fin l)

/-- The concrete vector-space carrier of `\mathcal H_{2l}`. -/
abbrev CanonicalHamiltonian (l : ℕ) := HamiltonianBasis l →₀ ℂ

/-- The basis vector `\widetilde h_r`, with `\widetilde h_0` definitionally zero. -/
noncomputable def canonicalH {l : ℕ} (r : Exponent l) : CanonicalHamiltonian l :=
  if hr : r = 0 then 0
  else Finsupp.single (Sum.inl ⟨r, hr⟩) 1

/-- The basis vector `d_i`. -/
noncomputable def canonicalD {l : ℕ} (i : Fin l ⊕ Fin l) :
    CanonicalHamiltonian l :=
  Finsupp.single (Sum.inr i) 1

/-- Bracket of two displayed basis vectors of the Hamiltonian algebra. -/
noncomputable def canonicalBasisBracket {l : ℕ}
    (a b : HamiltonianBasis l) : CanonicalHamiltonian l :=
  match a, b with
  | Sum.inl r, Sum.inl s =>
      exponentDot (tildeExponent (r : Exponent l))
          (fun i ↦ ((s : Exponent l) i : ℂ)) •
        canonicalH ((r : Exponent l) + (s : Exponent l))
  | Sum.inr i, Sum.inl r => ((r : Exponent l) i : ℂ) • canonicalH r
  | Sum.inl r, Sum.inr i => -((r : Exponent l) i : ℂ) • canonicalH r
  | Sum.inr _, Sum.inr _ => 0

/-- The bilinear extension of the displayed basis bracket. -/
noncomputable def canonicalHamiltonianBracket {l : ℕ}
    (x y : CanonicalHamiltonian l) : CanonicalHamiltonian l :=
  x.sum fun a ca ↦ y.sum fun b cb ↦ (ca * cb) • canonicalBasisBracket a b

/--
The explicit bracket really is a complex Lie bracket.  This is a transparent
list of the laws, not a caller-selected `LieRing` instance.
-/
def IsCanonicalHamiltonianLieBracket (l : ℕ) : Prop :=
  ( ∀ x y z : CanonicalHamiltonian l,
      canonicalHamiltonianBracket (x + y) z =
        canonicalHamiltonianBracket x z + canonicalHamiltonianBracket y z) ∧
  ( ∀ x y z : CanonicalHamiltonian l,
      canonicalHamiltonianBracket x (y + z) =
        canonicalHamiltonianBracket x y + canonicalHamiltonianBracket x z) ∧
  ( ∀ (a : ℂ) (x y : CanonicalHamiltonian l),
      canonicalHamiltonianBracket (a • x) y =
        a • canonicalHamiltonianBracket x y) ∧
  ( ∀ (a : ℂ) (x y : CanonicalHamiltonian l),
      canonicalHamiltonianBracket x (a • y) =
        a • canonicalHamiltonianBracket x y) ∧
  ( ∀ x : CanonicalHamiltonian l, canonicalHamiltonianBracket x x = 0) ∧
  ( ∀ x y z : CanonicalHamiltonian l,
      canonicalHamiltonianBracket x (canonicalHamiltonianBracket y z) +
        canonicalHamiltonianBracket y (canonicalHamiltonianBracket z x) +
        canonicalHamiltonianBracket z (canonicalHamiltonianBracket x y) = 0)

/-- A representation of the explicit Hamiltonian bracket. -/
structure CanonicalHamiltonianRepresentation (l : ℕ) (M : Type*)
    [AddCommGroup M] [Module ℂ M] where
  toLinearMap : CanonicalHamiltonian l →ₗ[ℂ] Module.End ℂ M
  map_bracket : ∀ x y,
    toLinearMap (canonicalHamiltonianBracket x y) =
      ⁅toLinearMap x, toLinearMap y⁆

noncomputable instance {l : ℕ} {M : Type*} [AddCommGroup M] [Module ℂ M] :
    CoeFun (CanonicalHamiltonianRepresentation l M)
      (fun _ ↦ CanonicalHamiltonian l → M → M) :=
  ⟨fun ρ x m ↦ ρ.toLinearMap x m⟩

/-- Invariant subspaces for a representation of the explicit bracket. -/
def IsCanonicalInvariant {l : ℕ} {M : Type*}
    [AddCommGroup M] [Module ℂ M]
    (ρ : CanonicalHamiltonianRepresentation l M) (S : Submodule ℂ M) : Prop :=
  ∀ x m, m ∈ S → ρ x m ∈ S

/-- Simplicity for a representation of the explicit Hamiltonian algebra. -/
def IsSimpleCanonicalRepresentation {l : ℕ} {M : Type*}
    [AddCommGroup M] [Module ℂ M]
    (ρ : CanonicalHamiltonianRepresentation l M) : Prop :=
  Nontrivial M ∧ ∀ S : Submodule ℂ M,
    IsCanonicalInvariant ρ S → S = ⊥ ∨ S = ⊤

/-- The concrete Shen--Larsson action on Laurent pure tensors. -/
def HasCanonicalShenLarssonAction {l : ℕ} {M : Type*}
    [AddCommGroup M] [Module ℂ M]
    (ρ : LieRepresentation (Sp l) M)
    (alpha beta : (Fin l ⊕ Fin l) → ℂ)
    (σ : CanonicalHamiltonianRepresentation l (M ⊗[ℂ] Laurent l)) : Prop :=
  ∃ outer : Exponent l → Sp l,
    (∀ r, (outer r : Matrix (Fin l ⊕ Fin l) (Fin l ⊕ Fin l) ℂ) =
      outerMatrix r) ∧
    (∀ r s v,
      σ (canonicalH r) (v ⊗ₜ[ℂ] laurentMonomial s) =
        ((exponentDot (tildeExponent r)
            (fun i ↦ (s i : ℂ) + alpha i)) • v + ρ (outer r) v) ⊗ₜ[ℂ]
          laurentMonomial (r + s)) ∧
    (∀ i s v,
      σ (canonicalD i) (v ⊗ₜ[ℂ] laurentMonomial s) =
        (((s i : ℂ) + beta i) • v) ⊗ₜ[ℂ] laurentMonomial s)

/-- Simultaneous weight vectors for the concrete degree derivations. -/
def IsCanonicalHamiltonianWeightVector {l : ℕ} {M : Type*}
    [AddCommGroup M] [Module ℂ M]
    (σ : CanonicalHamiltonianRepresentation l M) (v : M) : Prop :=
  ∃ lambda : (Fin l ⊕ Fin l) → ℂ,
    ∀ i, σ (canonicalD i) v = lambda i • v

/-- The module is spanned by simultaneous degree-weight vectors. -/
def IsCanonicalHamiltonianWeightRepresentation {l : ℕ} {M : Type*}
    [AddCommGroup M] [Module ℂ M]
    (σ : CanonicalHamiltonianRepresentation l M) : Prop :=
  Submodule.span ℂ {v : M | IsCanonicalHamiltonianWeightVector σ v} = ⊤

/-- The weight `s + beta` space is exactly `M ⊗ C x^s`. -/
def HasCanonicalExactDegreeWeightSpaces {l : ℕ} {M : Type*}
    [AddCommGroup M] [Module ℂ M]
    (σ : CanonicalHamiltonianRepresentation l (M ⊗[ℂ] Laurent l))
    (beta : (Fin l ⊕ Fin l) → ℂ) : Prop :=
  ∀ s : Exponent l,
    {w : M ⊗[ℂ] Laurent l |
      ∀ i, σ (canonicalD i) w = ((s i : ℂ) + beta i) • w} =
    Set.range (fun v : M ↦ v ⊗ₜ[ℂ] laurentMonomial s)

/-! ## The common proposition families used by the open goal -/

/-- A family consists of genuine Lie representations satisfying (3.11). -/
def IsTauFamily {l : ℕ} (P : GeneratorPresentation l)
    (tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l)) : Prop :=
  ∀ c phi, HasGeneratorAction P (tau c phi) c phi ∧
    IsFreeRankOneOverNilradical P (tau c phi)

/-- The classification, parameter uniqueness, weight, and simplicity conclusions. -/
def HasCoreClassification {l : ℕ} (P : GeneratorPresentation l)
    (tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l)) : Prop :=
  (∀ (M : Type) [AddCommGroup M] [Module ℂ M]
      (rho : LieRepresentation (Sp l) M),
      IsFreeRankOneOverNilradical P rho →
        ∃ c phi, LieRepEquivalent rho (tau c phi)) ∧
  (∀ c₁ phi₁ c₂ phi₂,
      LieRepEquivalent (tau c₁ phi₁) (tau c₂ phi₂) ↔
        c₁ = c₂ ∧ IsConstant (phi₁ - phi₂)) ∧
  (∀ c phi, IsWeightRepresentation P (tau c phi) ↔ IsConstant phi) ∧
  (∀ c phi, IsConstant phi →
      HasLowestWeightGenerator P (tau c phi) c) ∧
  (∀ c phi,
      IsSimpleRepresentation (tau c phi) ↔ ¬ IsExceptional l c)

/-- The exceptional-parameter finite-length and Jordan--Hölder conclusion. -/
def HasExceptionalFiniteLength {l : ℕ}
    (tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l)) : Prop :=
  ∀ c phi, IsExceptional l c →
    IsNoetherianRepresentation (tau c phi) ∧
      IsArtinianRepresentation (tau c phi) ∧
      HasFiniteCompositionSeries (tau c phi) ∧
      HasJordanHolderUniqueness (tau c phi)

/-- The Shen--Larsson application for the explicit Hamiltonian bracket. -/
def HasCanonicalHamiltonianApplication {l : ℕ}
    (tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l)) : Prop :=
  IsCanonicalHamiltonianLieBracket l ∧
  ∀ c phi, ¬ IsExceptional l c →
    ∀ alpha beta : (Fin l ⊕ Fin l) → ℂ,
      ∃ sigma : CanonicalHamiltonianRepresentation l
          (Poly l ⊗[ℂ] Laurent l),
        HasCanonicalShenLarssonAction (tau c phi) alpha beta sigma ∧
          IsSimpleCanonicalRepresentation sigma ∧
          IsCanonicalHamiltonianWeightRepresentation sigma ∧
          HasCanonicalExactDegreeWeightSpaces sigma beta


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, Theorems 1.1–1.3 on pp. 343–344; formal Theorems 3.7, 3.8, 4.7, 4.9, and 5.2: https://doi.org/10.1016/j.jalgebra.2026.02.022

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

Definitions.SymplecticFreeModulesInterfaces / definition bundle

SymplecticFreeModules.SymmetricIndex, symmetricIndex, Poly, T, and partialDeriv. For $l\in\mathbb N$ , polynomial variables are indexed by pairs $(i,j)\in\operatorname{Fin}(l)^2$ satisfying $i\le j$ . The function $\{i,j\}$ orders an arbitrary pair into that subtype. The algebra $\operatorname{Poly}_l$ is the multivariate polynomial algebra over $\mathbb C$ in those variables, $T_{ij}$ is the variable indexed by the ordered pair $\{i,j\}$ , and $\partial_{ij}$ is formal polynomial differentiation with respect to that same symmetrized variable. Thus $T_{ij}=T_{ji}$ and $\partial_{ij}=\partial_{ji}$ . At $l=0$ , the index type is empty.

SymplecticFreeModules.xTilde. For $i,j\in\operatorname{Fin}(l)$ and $q\in\operatorname{Poly}_l$ ,

\widetilde X_{ij}(q)= \sum_{k\in\operatorname{Fin}(l)} c_{ki}T_{ki}\partial_{kj}q, \qquad c_{ki}=\begin{cases}2,&k=i,\\1,&k\ne i.\end{cases}

SymplecticFreeModules.yTilde. For $c\in\mathbb C$ ,

\widetilde Y_{ij}^{\,c}(q) =2c\,\partial_{ij}q+ \sum_k\widetilde X_{ki}(\partial_{kj}q).

SymplecticFreeModules.xCandidate. The candidate action assigned to $X_{ij}$ at parameters $c,\phi$ is

q\longmapsto \widetilde X_{ij}(q)+ \bigl(\widetilde X_{ij}(\phi)+\mathbf 1_{i=j}c\bigr)q,

where scalars are inserted as constant polynomials.

SymplecticFreeModules.tCandidate. The candidate action assigned to $T_{ij}$ is multiplication $q\mapsto T_{ij}q$ .

SymplecticFreeModules.yDiagonalCandidate. The candidate action assigned to the diagonal negative-root generator is

q\longmapsto-\frac12\left( \widetilde Y_{ii}^{\,c}(\phi)q+\widetilde Y_{ii}^{\,c}(q) +\sum_k\widetilde X_{ki}(\phi) \bigl((\partial_{ki}\phi)q+2\partial_{ki}q\bigr) \right).

SymplecticFreeModules.Sp. This is Mathlib’s concrete complex symplectic Lie algebra on two copies of $\operatorname{Fin}(l)$ , realized as matrices satisfying its symplectic condition.

SymplecticFreeModules.xMatrix. The displayed $X_{ij}$ matrix is the matrix unit from the first-copy index $i$ to first-copy index $j$ , minus the matrix unit from second-copy index $j$ to second-copy index $i$ .

SymplecticFreeModules.yDiagonalMatrix. The displayed $Y_{ii}$ matrix has its sole nonzero entry $1$ from first-copy $i$ to second-copy $i$ .

SymplecticFreeModules.tMatrix. The displayed $T_{ij}$ matrix has one upper-right entry when $i=j$ , and for $i\ne j$ is the sum of the two symmetrically placed upper-right matrix units.

SymplecticFreeModules.GeneratorPresentation. A presentation chooses elements $X_{ij},Y_{ii},T_{ij}$ of the concrete symplectic Lie algebra for all relevant indices and includes proofs that their underlying matrices are exactly the three matrices above. It does not itself assert the candidate polynomial formulas or any commutator relations.

SymplecticFreeModules.IsAbelianNilradicalSystem. This says that every two displayed $T_{ij}$ and $T_{km}$ have zero Lie bracket and that the family indexed once per unordered pair, $(i,j)$ with $i\le j$ , is complex-linearly independent. At $l=0$ , the commutator quantifiers are empty and the empty family is linearly independent.

SymplecticFreeModules.LieRepresentation. For a complex Lie algebra $L$ and complex module $M$ , this is a genuine complex-linear Lie homomorphism $L\to\operatorname{End}_{\mathbb C}(M)$ , so preservation of Lie brackets is part of its type.

SymplecticFreeModules.HasGeneratorAction. For a presentation $P$ , representation $\rho$ on $\operatorname{Poly}_l$ , and parameters $c,\phi$ , this requires, for every polynomial $q$ , exact equality of $\rho(X_{ij})q$ , $\rho(T_{ij})q$ , and $\rho(Y_{ii})q$ with the three explicit candidate operators above. It specifies only diagonal $Y$ -generators directly; $\rho$ is nevertheless a representation of the entire symplectic Lie algebra.

SymplecticFreeModules.LieRepEquivalent. Two representations $\rho$ on $M$ and $\sigma$ on $N$ are equivalent when there exists a complex-linear equivalence $e:M\cong N$ satisfying $e(\rho(x)m)=\sigma(x)e(m)$ for every Lie element $x$ and every $m$ .

SymplecticFreeModules.IsFreeRankOneOverNilradical. A representation $\rho$ on a complex module $M$ has this property when there exists a complex-linear equivalence $e:\operatorname{Poly}_l\cong M$ such that

e(T_{ij}q)=\rho(P.T_{ij})e(q)

for every $i,j,q$ . The witness is required only to be a linear equivalence plus these generator multiplication identities; the definition does not separately install a module-over- $\operatorname{Poly}_l$ structure.

SymplecticFreeModules.IsInvariant. A complex submodule $S\le M$ is invariant under $\rho$ when $\rho(x)m\in S$ for every Lie element $x$ and every $m\in S$ .

SymplecticFreeModules.IsSimpleRepresentation. A representation is simple when its carrier $M$ is nontrivial and every invariant complex submodule is either $0$ or all of $M$ .

SymplecticFreeModules.IsWeightVector. A vector $v\in M$ is a weight vector when there exists $\lambda:\operatorname{Fin}(l)\to\mathbb C$ such that $\rho(X_{ii})v=\lambda_i v$ for every $i$ . The zero vector is included, since suitable eigenvalue equations hold for it.

SymplecticFreeModules.IsWeightRepresentation. This says that the complex-linear span of all simultaneous weight vectors for the diagonal $X_{ii}$ is the whole carrier.

SymplecticFreeModules.HasLowestWeightGenerator. For a representation on $\operatorname{Poly}_l$ and $c\in\mathbb C$ , this says that there exists a last index $a\in\operatorname{Fin}(l)$ with $a+1=l$ , and the polynomial $1$ satisfies

\rho(Y_{aa})1=0,\qquad \rho(X_{aa})1=c\,1.

For every adjacent $i+1=j$ , $\rho(X_{ii}-X_{jj})1=0$ ; for every reverse-adjacent $j+1=i$ , $\rho(X_{ij})1=0$ . Finally, every invariant submodule containing $1$ is the whole polynomial module. At $l=0$ , no last index exists, so this predicate is false; the main theorem assumes $l\ge2$ .

SymplecticFreeModules.IsConstant. A polynomial $\phi$ is constant exactly when there exists $c\in\mathbb C$ with $\phi=C(c)$ .

SymplecticFreeModules.IsExceptional. A complex number $c$ is exceptional at rank $l$ when there exists a positive natural number $n$ such that

c=\frac{l+1}{2}-\frac n2

inside $\mathbb C$ . The existential natural number is unbounded.

SymplecticFreeModules.IsNoetherianRepresentation. Every monotone ascending sequence $S_0\le S_1\le\cdots$ of invariant complex submodules must have an index $n_0$ such that $S_n=S_{n_0}$ for all $n\ge n_0$ .

SymplecticFreeModules.IsArtinianRepresentation. Every antitone descending sequence of invariant complex submodules must stabilize in the same eventual-equality sense.

SymplecticFreeModules.IsCompositionStep. A pair $S,T$ is a composition step when both are invariant, $S<T$ strictly, and every invariant $U$ with $S\le U\le T$ equals $S$ or $T$ .

SymplecticFreeModules.IsFiniteCompositionSeries. A specified natural length $s$ and sequence $S_n$ form a finite composition series when $s>0$ , $S_0=0$ , $S_s=M$ , and $S_i<S_{i+1}$ is a composition step for every $i<s$ . No condition is placed on $S_n$ for $n>s$ .

SymplecticFreeModules.HasFiniteCompositionSeries. This asserts the existence of some positive length $s$ and some sequence of submodules forming the preceding series.

SymplecticFreeModules.invariantRestrictedAction. Given an invariant submodule $T$ , this is the linear endomorphism of $T$ induced by restricting $\rho(x)$ ; invariance supplies the proof that the image remains in $T$ .

SymplecticFreeModules.compositionFactorAction. Given invariant $S,T$ , this is the induced action on the concrete quotient $T/(S\cap T)$ , represented as $T$ modulo the pullback of $S$ along $T\hookrightarrow M$ . In later use $S\le T$ , so this is $T/S$ .

SymplecticFreeModules.CompositionFactorsEquivalent. For $S,T,U,V$ , this requires $S\le T$ and $U\le V$ , existential witnesses that all four submodules are invariant, and a complex-linear equivalence $T/S\cong V/U$ intertwining the induced quotient action for every Lie element and quotient vector.

SymplecticFreeModules.HasJordanHolderUniqueness. For every two finite composition series of lengths $s,t$ , there must exist an equivalence $\operatorname{Fin}(s)\cong\operatorname{Fin}(t)$ such that each successive quotient in the first series is representation-equivalent to the correspondingly permuted quotient in the second. If there are no finite composition series, this predicate alone is vacuous; the exceptional finite-length predicate separately requires existence of one.

SymplecticFreeModules.Exponent and Laurent. An exponent is an integer vector indexed by the disjoint union of two copies of $\operatorname{Fin}(l)$ . The Laurent algebra is the complex group algebra of this additive exponent lattice, represented as an additive-monoid algebra.

SymplecticFreeModules.tildeExponent. For $r=(r_{\rm left},r_{\rm right})$ , the tilde exponent has left coordinates $r_{\rm right}$ and right coordinates $-r_{\rm left}$ .

SymplecticFreeModules.laurentMonomial. The monomial $x^r$ is the group-algebra basis element supported at exponent $r$ with coefficient $1$ .

SymplecticFreeModules.exponentDot. For integer exponent $r$ and complex coordinate family $a$ , this is $\sum_i r_i a_i$ .

SymplecticFreeModules.outerMatrix. This is the complex matrix with entries $r_i\widetilde r_j$ .

SymplecticFreeModules.NonzeroExponent, HamiltonianBasis, and CanonicalHamiltonian. Nonzero exponents are exponent vectors equipped with a proof that they are not zero. Hamiltonian basis labels are either such a nonzero exponent or one of the $2l$ coordinate labels. The canonical Hamiltonian carrier is the complex vector space of finitely supported coefficient functions on those labels.

SymplecticFreeModules.canonicalH. For every exponent $r$ , $\widetilde h_r$ is definitionally $0$ when $r=0$ , and otherwise is the basis vector labelled by $r$ .

SymplecticFreeModules.canonicalD. For every coordinate label $i$ , $d_i$ is its corresponding basis vector.

SymplecticFreeModules.canonicalBasisBracket. On displayed basis vectors the operation is

[\widetilde h_r,\widetilde h_s] =\langle\widetilde r,s\rangle\widetilde h_{r+s},\quad [d_i,\widetilde h_r]=r_i\widetilde h_r,\quad [\widetilde h_r,d_i]=-r_i\widetilde h_r,\quad [d_i,d_j]=0.

When $r+s=0$ , the first result uses the definition $\widetilde h_0=0$ .

SymplecticFreeModules.canonicalHamiltonianBracket. This is the double finite-support sum extending the preceding basis operation with coefficient $c_ad_b$ . It is an explicitly defined operation before any Lie laws are established.

SymplecticFreeModules.IsCanonicalHamiltonianLieBracket. This proposition requires additivity in each argument, complex homogeneity in each argument, $[x,x]=0$ for every $x$ , and the Jacobi identity

[x,[y,z]]+[y,[z,x]]+[z,[x,y]]=0

for all elements of the explicit carrier. These are proof obligations, not an assumed Lie-ring instance.

SymplecticFreeModules.CanonicalHamiltonianRepresentation and its evaluation coercion. Such a representation is a complex-linear map from the explicit Hamiltonian carrier to complex-linear endomorphisms of $M$ satisfying

\sigma([x,y])=[\sigma(x),\sigma(y)]

for every $x,y$ , where the right side is the endomorphism commutator. It is made callable as $\sigma(x)m$ . The structure can be formed syntactically independently of the separate proposition asserting all bracket laws.

SymplecticFreeModules.IsCanonicalInvariant. A complex submodule is canonically invariant when it is closed under $\sigma(x)$ for every explicit Hamiltonian element $x$ .

SymplecticFreeModules.IsSimpleCanonicalRepresentation. This requires a nontrivial carrier and says every canonically invariant complex submodule is zero or the whole carrier.

SymplecticFreeModules.HasCanonicalShenLarssonAction. Given a symplectic representation $\rho$ on $M$ , coordinate parameters $\alpha,\beta\in\mathbb C^{2l}$ , and an explicit-Hamiltonian representation $\sigma$ on $M\otimes_{\mathbb C}\operatorname{Laurent}_l$ , this says there exists a map $R:r\mapsto R_r\in\mathfrak{sp}_{2l}(\mathbb C)$ whose underlying matrix is exactly $(r_i\widetilde r_j)_{ij}$ , and for every exponents $r,s$ and $v\in M$ ,

\sigma(\widetilde h_r)(v\otimes x^s) =\left( \langle\widetilde r,s+\alpha\rangle v+\rho(R_r)v \right)\otimes x^{r+s}.

For every coordinate $i$ ,

\sigma(d_i)(v\otimes x^s)=(s_i+\beta_i)v\otimes x^s.

The formulas include $r=0$ , for which $\widetilde h_0=0$ .

SymplecticFreeModules.IsCanonicalHamiltonianWeightVector. A vector $v$ is a simultaneous degree-weight vector when there exists $\lambda\in\mathbb C^{2l}$ such that $\sigma(d_i)v=\lambda_i v$ for every $i$ . The zero vector is included.

SymplecticFreeModules.IsCanonicalHamiltonianWeightRepresentation. This says the span of all such simultaneous degree-weight vectors is the whole carrier.

SymplecticFreeModules.HasCanonicalExactDegreeWeightSpaces. For every exponent $s$ , the set of all tensors $w$ satisfying

\sigma(d_i)w=(s_i+\beta_i)w\quad\text{for every }i

must equal exactly the range of $v\mapsto v\otimes x^s$ . This is equality of sets, not merely an inclusion or spanning assertion.

SymplecticFreeModules.IsTauFamily. A family $\tau(c,\phi)$ must, for every $c\in\mathbb C$ and $\phi\in\operatorname{Poly}_l$ , be a genuine symplectic-Lie-algebra representation on $\operatorname{Poly}_l$ , act on all displayed $X,T,Y_{\rm diag}$ generators by the exact candidate differential/multiplication formulas, and be free rank one over the displayed $T$ -system through some complex-linear equivalence from $\operatorname{Poly}_l$ . The freeness equivalence may depend on $c,\phi$ .

SymplecticFreeModules.HasCoreClassification. This is the conjunction of five claims about one presentation $P$ and one family $\tau$ . First, for every small-universe type $M$ carrying a complex module structure and every symplectic representation $\rho$ on it, freeness rank one over the displayed $T$ -system implies that some $c,\phi$ make $\rho$ representation-equivalent to $\tau(c,\phi)$ . Second,

\tau(c_1,\phi_1)\cong\tau(c_2,\phi_2) \quad\Longleftrightarrow\quad c_1=c_2\ \text{and}\ \phi_1-\phi_2\text{ is constant}.

Third, $\tau(c,\phi)$ is spanned by simultaneous $X_{ii}$ -weight vectors exactly when $\phi$ is constant. Fourth, when $\phi$ is constant, the polynomial $1$ satisfies the explicit lowest-weight, adjacent-generator, and invariant-cyclic conditions with weight $c$ . Fifth,

\tau(c,\phi)\text{ is simple} \quad\Longleftrightarrow\quad c\ne\frac{l+1-n}{2}\ \text{for every positive }n\in\mathbb N.

The simplicity criterion is independent of $\phi$ .

SymplecticFreeModules.HasExceptionalFiniteLength. For every $c,\phi$ , if $c=(l+1-n)/2$ for some positive natural $n$ , then $\tau(c,\phi)$ is both Noetherian and Artinian with respect to invariant submodules, has at least one finite composition series, and any two such series have the same quotient representations up to a permutation. No conclusion is imposed here at nonexceptional $c$ , and no explicit list or multiplicity of factors is supplied.

SymplecticFreeModules.HasCanonicalHamiltonianApplication. This first requires the explicitly defined Hamiltonian bracket itself to satisfy both complex bilinearity laws, alternation, and Jacobi. Then, for every $c,\phi$ with $c$ nonexceptional and every two arbitrary coordinate functions $\alpha,\beta\in\mathbb C^{2l}$ , it requires the existence of an explicit-Hamiltonian representation $\sigma$ on

\operatorname{Poly}_l\otimes_{\mathbb C}\operatorname{Laurent}_l

that obeys the exact Shen–Larsson pure-tensor formulas using the symplectic representation $\tau(c,\phi)$ , is simple, is spanned by simultaneous degree-weight vectors, and has for every exponent $s$ exactly the degree-weight space $\{v\otimes x^s:v\in\operatorname{Poly}_l\}$ at weight $s+\beta$ . The representation $\sigma$ may depend on $c,\phi,\alpha,\beta$ .

Human review

Endorsed by Shuze Chen · Aug 27, 2026
Endorsed by ShouqiaoWang · Aug 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph