The Frobenius tower of an object

The tensor powers of a single object in a rigid symmetric ℂ-linear category, with the symmetric-group action permuting the factors and the categorical trace, form a Frobenius tower. Everything the tower asks for has been assembled: the representations are permAlg, vanishing propagates by permAlg_compat, the traces are scalarTrace, the tensor-power maps are powHom, and the Frobenius identity comes from the cycle-type formula for the trace of a permutation against a tensor power.

The Frobenius identity

theorem RS.frobenius_powHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) (X : A) (P : SchurPackage) (μ : YoungDiagram) (g : CategoryTheory.End X) : (scalarTrace hu (tensorPow A X μ.card)) ((permAlg X μ.card) (P.e μ) * powHom X g μ.card) = ↑(P.dim μ) * diagramSchur μ fun (m : ℕ) => (scalarTrace hu X) (g ^ m)

The Frobenius trace identity for the tensor powers of an object: the trace of a Young idempotent against a tensor power is the block dimension times the Schur specialization of the power traces. Expanding the idempotent turns the left side into a character-weighted sum of permutation traces, and the cycle-type formula turns each of those into the cycle product the classical Frobenius formula sums.

The tower

noncomputable def RS.objectFrobeniusTower {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) (X : A) (P : SchurPackage) (A₀ : ℝ) (hb : ∀ (n : ℕ), ↑(Module.finrank ℂ (CategoryTheory.End (tensorPow A X n))) ≤ A₀ ^ n) : FrobeniusTower P (fun (n : ℕ) => CategoryTheory.End (tensorPow A X n)) A₀ (CategoryTheory.End X)

The Frobenius tower of an object: the tensor powers of X, with the symmetric-group action permuting the factors, the tensor powers of an endomorphism, and the categorical trace read as a complex number.

Equations

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

The theorems of the appendix, for an object

theorem RS.scalarTrace_eq_zero_of_isNilpotent {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) (X : A) [∀ (n : ℕ), Module.Finite ℂ (CategoryTheory.End (tensorPow A X n))] (A₀ : ℝ) (hb : ∀ (n : ℕ), ↑(Module.finrank ℂ (CategoryTheory.End (tensorPow A X n))) ≤ A₀ ^ n) {g : CategoryTheory.End X} (hg : IsNilpotent g) : (scalarTrace hu X) g = 0

The nilpotent-trace theorem for an object: in a rigid symmetric ℂ-linear category with scalar unit endomorphisms, if the tensor powers of X have finite-dimensional endomorphism algebras of exponentially bounded dimension, then every nilpotent endomorphism of X has vanishing categorical trace.

theorem RS.traceZeta_rational_of_object {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) (X : A) [∀ (n : ℕ), Module.Finite ℂ (CategoryTheory.End (tensorPow A X n))] (A₀ : ℝ) (hb : ∀ (n : ℕ), ↑(Module.finrank ℂ (CategoryTheory.End (tensorPow A X n))) ≤ A₀ ^ n) (g : CategoryTheory.End X) {s : ℕ} (hs : 2 * Real.exp 1 * √A₀ < ↑s) : ∃ (Pp : Polynomial ℂ) (Qp : Polynomial ℂ), Pp.coeff 0 = 1 ∧ Qp.coeff 0 = 1 ∧ Pp.natDegree ≤ s - 1 ∧ Qp.natDegree ≤ s - 1 ∧ IsCoprime Pp Qp ∧ (traceZeta fun (m : ℕ) => (scalarTrace hu X) (g ^ m)) * ↑Qp = ↑Pp

The trace-zeta theorem for an object (the accompanying paper, Corollary A.2): for an object whose tensor powers have endomorphism dimensions bounded by A₀ ^ n, and for every integer s > 2e√A₀, the trace zeta function of every endomorphism is P/Q with P and Q coprime, of constant term 1, and of degree at most s − 1.

theorem RS.traceZeta_superSpectrum_of_object {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) (X : A) [∀ (n : ℕ), Module.Finite ℂ (CategoryTheory.End (tensorPow A X n))] (A₀ : ℝ) (hb : ∀ (n : ℕ), ↑(Module.finrank ℂ (CategoryTheory.End (tensorPow A X n))) ≤ A₀ ^ n) (g : CategoryTheory.End X) {s : ℕ} (hs : 2 * Real.exp 1 * √A₀ < ↑s) : ∃ (alpha : Multiset ℂ) (beta : Multiset ℂ), alpha.card ≤ s - 1 ∧ beta.card ≤ s - 1 ∧ (∀ x ∈ alpha, x ≠ 0) ∧ (∀ x ∈ beta, x ≠ 0) ∧ (∀ x ∈ alpha, x ∉ beta) ∧ ∀ (m : ℕ), 1 ≤ m → (scalarTrace hu X) (g ^ m) = (Multiset.map (fun (x : ℂ) => x ^ m) alpha).sum - (Multiset.map (fun (x : ℂ) => x ^ m) beta).sum

The reduced super-spectrum form of Corollary A.2 for an object: for every integer s > 2e√A₀ the power traces are a difference of power sums of two disjoint multisets of nonzero complex numbers, each of size at most s − 1.