The nilpotent-trace theorem

A FrobeniusTower is a PermTower together with an ambient algebra A, trace functionals, tensor-power maps, and the Frobenius trace identity τ (rep (e μ) * pow g) = dim μ · s_μ[tr (g^·)]. The main theorem: in such a tower every nilpotent element of A has trace zero.

The proof composes the pieces already on the page: hook confinement kills the idempotents of shapes outside a hook, the Frobenius identity turns each death into vanishing of the Schur specialization of the power-trace sequence, nilpotency makes that sequence eventually zero, and the hook-vanishing engine (powerSums_zero_of_hook_and_eventually_zero) then forces every power trace — in particular the trace itself — to vanish.

The skein construction discharges the tower fields: rep is the permutation action on strand bundles, pow the tensor power of an endomorphism, and frobenius the categorical Frobenius formula.

structure RS.FrobeniusTower (P : SchurPackage) (E : ℕ → Type u) [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] (A : ℝ) (Alg : Type u) [Ring Alg] [Algebra ℂ Alg] extends RS.PermTower E A : Type u

A PermTower with an ambient algebra, traces, tensor-power maps, and the Frobenius trace identity relative to a Schur package.

• rep (n : ℕ) : SymGroupAlgebra n →ₐ[ℂ] E n
• compat {m n : ℕ} (h : m ≤ n) (x : SymGroupAlgebra m) : (self.rep m) x = 0 → (self.rep n) ((symCast h) x) = 0
• bound (n : ℕ) : ↑(Module.finrank ℂ (E n)) ≤ A ^ n
• traceA : Alg →ₗ[ℂ] ℂ

  The trace on the ambient algebra.

• trace (n : ℕ) : E n →ₗ[ℂ] ℂ

  The traces on the tower algebras.

• pow (n : ℕ) : Alg → E n

  The tensor-power maps.

• frobenius (μ : YoungDiagram) (g : Alg) : (self.trace μ.card) ((self.rep μ.card) (P.e μ) * self.pow μ.card g) = ↑(P.dim μ) * diagramSchur μ fun (m : ℕ) => self.traceA (g ^ m)

  The Frobenius trace identity: the trace of a Young idempotent against a tensor power is the dimension times the Schur specialization of the power-trace sequence.

theorem RS.FrobeniusTower.schur_vanishing_of_confinement {P : SchurPackage} {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} {Alg : Type u} [Ring Alg] [Algebra ℂ Alg] (T : FrobeniusTower P E A Alg) (g : Alg) {s : ℕ} (hconf : ∀ (μ : YoungDiagram), T.Alive P μ → IsInHook (s - 1) (s - 1) μ) (μ : YoungDiagram) : ¬IsInHook (s - 1) (s - 1) μ → (diagramSchur μ fun (m : ℕ) => T.traceA (g ^ m)) = 0

Schur vanishing from hook confinement: if every shape alive in the tower lies in the (s − 1, s − 1) hook, the Schur specialization of the power-trace sequence vanishes on every shape outside it. The Frobenius identity turns a dead idempotent into a vanishing specialization, and the block dimension is nonzero.

theorem RS.FrobeniusTower.traceA_eq_zero_of_isNilpotent {P : SchurPackage} {E : ℕ → Type u} [(n : ℕ) → Ring (E n)] [(n : ℕ) → Algebra ℂ (E n)] {A : ℝ} {Alg : Type u} [Ring Alg] [Algebra ℂ Alg] [∀ (n : ℕ), Module.Finite ℂ (E n)] (T : FrobeniusTower P E A Alg) {g : Alg} (hg : IsNilpotent g) : T.traceA g = 0

The nilpotent-trace theorem: in a Frobenius tower with finite-dimensional levels, every nilpotent element of the ambient algebra has trace zero.