The scalar cycle-trace formula

The categorical cycle-trace formula read through the scalar unit. This is the common trace input to the factorial obstruction and to the Frobenius formula. Fixed points can be recorded separately from the nontrivial cycles.

theorem RS.scalarTrace_permMor_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) (g : CategoryTheory.End X) {n : ℕ} (π : Equiv.Perm (Fin n)) : (scalarTrace hu (tensorPow A X n)) (CategoryTheory.CategoryStruct.comp (permMor X n π) (powHom X g n)) = (Multiset.map (fun (c : ℕ) => (scalarTrace hu X) (g ^ c)) (fullCycleType π)).prod

The complex trace of a permutation against a tensor power is the product of the complex cycle traces over the full cycle type.

theorem RS.prod_fullCycleType {n : ℕ} (π : Equiv.Perm (Fin n)) (t : ℕ → ℂ) : (Multiset.map t (fullCycleType π)).prod = (Multiset.map t π.cycleType).prod * t 1 ^ (n - π.cycleType.sum)

The full cycle type splits the product into the cycle type and the fixed points.