The block Frobenius tower

The Frobenius character identity at every ambient arity: the trace of a Young idempotent (in the block representation of S_k) against the block-diagonal power is the dimension times the Schur specialization of the block power traces. The resulting FrobeniusTower gives the appendix's nilpotent-trace proof at every strand arity. The mainline semisimplicity proof uses the factorial argument in BlockFactorialTrace.

theorem RS.block_frobenius {R : ℕ} (f : EdgeRankParameter R) (P : SchurPackage) (n : ℕ) (μ : YoungDiagram) (g : skeinEnd f n) : skeinTrace f (n * μ.card) ((blockRep f n μ.card) (P.e μ) * blockPow f n g μ.card) = ↑(P.dim μ) * diagramSchur μ fun (c : ℕ) => skeinTrace f n (g ^ c)

The block Frobenius identity at ambient arity n.

noncomputable def RS.blockFrobeniusTower {R : ℕ} (f : EdgeRankParameter R) (P : SchurPackage) (n : ℕ) : FrobeniusTower P (fun (k : ℕ) => skeinEnd f (n * k)) ((↑R ^ n) ^ 2) (skeinEnd f n)

The block Frobenius tower at ambient arity n.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.skeinTrace_eq_zero_of_isNilpotent_all {R : ℕ} (f : EdgeRankParameter R) (P : SchurPackage) (n : ℕ) {g : skeinEnd f n} (hg : IsNilpotent g) : skeinTrace f n g = 0

Nilpotent-trace vanishing at every arity: every nilpotent strand endomorphism, at any arity, has vanishing skein trace.