Prove2Me

Simplicity of the canonical Shen–Larsson action at nonexceptional parameters

Open
SymplecticFreeModules.canonicalShenLarssonSimplicity

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 a fixed family satisfying the prescribed generator-action and rank-one-freeness conditions. Fix a nonexceptional parameter cc, a polynomial φ\varphi, and vectors α,β∈C2l\alpha,\beta\in\mathbb C^{2l}. Suppose a representation σ\sigma on Poly⁡(l)⊗Laurent⁡(l)\operatorname{Poly}(l)\otimes\operatorname{Laurent}(l) has the canonical Shen–Larsson action

σ(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.

Then σ\sigma is simple: its module is nonzero, and every invariant complex subspace is either zero or the whole module. This statement isolates the simplicity assertion after construction of the action; all hypotheses on the original polynomial family and its parameter are retained.

Preamble
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces

open scoped TensorProduct
Formal statement
namespace SymplecticFreeModules

theorem canonicalShenLarssonSimplicity (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))
    (haction : HasCanonicalShenLarssonAction (tau c phi) alpha beta sigma) :
    IsSimpleCanonicalRepresentation sigma := by sorry

end SymplecticFreeModules
Source
Simplicity clause of the existing canonical Shen–Larsson application https://prove2.me/theorems/62f41608-35d7-45da-9f92-c7d499abc672 , itself extracted from https://prove2.me/theorems/e477ef9d-0d27-4603-83e7-5aab6b3d9981 . Cited source: Chen–Tan, Journal of Algebra 697 (2026), Theorem 5.2, https://doi.org/10.1016/j.jalgebra.2026.02.022 .

View graph