Polynomial symplectic-module and Hamiltonian-module interfaces

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

-- `Module.End ℂ M` is a Lie ring via the commutator; Mathlib no longer installs this globally.
attribute [local instance 100] LieRing.ofAssociativeRing

/-- 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