Prove2Me

Existence and simplicity of the canonical Shen--Larsson action

Open
SymplecticFreeModules.canonicalSimpleShenLarssonExists

by Wenqian · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

lie-algebrasrepresentation-theory

Let l≥2l\ge2, let PP be an abelian-nilradical generator system, and let τ(c,φ)\tau(c,\varphi) be one fixed family satisfying the source's generator-action and rank-one-freeness conditions. For every nonexceptional parameter cc, every polynomial φ\varphi, and every pair of parameter vectors α,β∈C2l\alpha,\beta\in\mathbb C^{2l}, there exists a simple representation σ\sigma on Poly⁡(l)⊗Laurent⁡(l)\operatorname{Poly}(l)\otimes\operatorname{Laurent}(l) with the canonical Shen--Larsson formulas

σ(hr)(v⊗xs)=(⟨r~,s+α⟩v+τ(c,φ)(rr~t)v)⊗xr+s,\sigma(h_r)(v\otimes x^s)=\big(\langle\widetilde r,s+\alpha\rangle v+\tau(c,\varphi)(r\widetilde r^t)v\big)\otimes x^{r+s}, σ(di)(v⊗xs)=(si+βi)v⊗xs.\sigma(d_i)(v\otimes x^s)=(s_i+\beta_i)v\otimes x^s.

The action predicate also supplies the symplectic-algebra element whose underlying matrix is rr~tr\widetilde r^t. Simplicity means that the tensor module is nontrivial and has no invariant complex subspaces other than zero and the whole space. This is the existence-and-simplicity part of the existing canonical Hamiltonian application; the bracket laws and weight-space consequences are separate dependencies.

Preamble
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces

open scoped TensorProduct
Formal statement
namespace SymplecticFreeModules

theorem canonicalSimpleShenLarssonExists (l : ℕ) (hl : 2 ≤ l)
    (P : GeneratorPresentation l) (hP : IsAbelianNilradicalSystem P)
    (tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l))
    (htau : IsTauFamily P tau)
    (c : ℂ) (phi : Poly l) (hc : ¬ 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 := by sorry

end SymplecticFreeModules
Source
Existence and simplicity clauses of Chen--Tan, Journal of Algebra 697 (2026), Theorem 5.2, https://doi.org/10.1016/j.jalgebra.2026.02.022 ; exact clauses of the existing target https://prove2.me/theorems/e477ef9d-0d27-4603-83e7-5aab6b3d9981 and definition HasCanonicalHamiltonianApplication.

View graph