The trace of a permutation against a tensor power

The trace of Φ(π) ∘ g ^ ⊗ n for an arbitrary permutation π: it is the product of tr (g ^ c) over the full cycle type of π, fixed points included.

The three ingredients are conjugation invariance, multiplicativity over a block sum, and the value on a single cycle. Every permutation is conjugate to a block sum of rotations whose block lengths are its full cycle type (exists_conj_blockCycles), so the three combine to give the general formula.

Conjugation invariance

theorem RS.catTrace_permMor_conj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.RigidCategory A] (X : A) (g : CategoryTheory.End X) (n : ℕ) (ρ π : Equiv.Perm (Fin n)) : catTrace (CategoryTheory.CategoryStruct.comp (permMor X n (ρ * π * ρ⁻¹)) (powHom X g n)) = catTrace (CategoryTheory.CategoryStruct.comp (permMor X n π) (powHom X g n))

The trace is a class function. Conjugating the permutation leaves the trace unchanged: the action is functorial and commutes with the tensor power, so the conjugating factors travel around the loop and cancel.

Multiplicativity over a block sum

theorem RS.catTrace_permMor_blockSum {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.RigidCategory A] (X : A) (g : CategoryTheory.End X) {p q : ℕ} (σ : Equiv.Perm (Fin p)) (τ : Equiv.Perm (Fin q)) : catTrace (CategoryTheory.CategoryStruct.comp (permMor X (p + q) (blockSum σ τ)) (powHom X g (p + q))) = catTrace (CategoryTheory.CategoryStruct.comp (permMor X p σ) (powHom X g p)) * catTrace (CategoryTheory.CategoryStruct.comp (permMor X q τ) (powHom X g q))

The trace is multiplicative over a block sum. A block sum of permutations acts blockwise on the splitting of the tensor power, as does the tensor power of the endomorphism, so the loop factors into the two blocks' loops.

A single cycle

theorem RS.catTrace_permMor_finRotate {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.RigidCategory A] (X : A) (g : CategoryTheory.End X) (m : ℕ) : catTrace (CategoryTheory.CategoryStruct.comp (permMor X (m + 1) (finRotate (m + 1))) (powHom X g (m + 1))) = catTrace (g ^ (m + 1))

The trace of a full rotation: the rotation of m + 1 slots against the tensor power of g traces to tr (g ^ (m + 1)).

A block sum of rotations

theorem RS.catTrace_blockCycles {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.RigidCategory A] (X : A) (g : CategoryTheory.End X) (l : List ℕ) : (∀ c ∈ l, 1 ≤ c) → catTrace (CategoryTheory.CategoryStruct.comp (permMor X l.sum (blockCycles l)) (powHom X g l.sum)) = (List.map (fun (c : ℕ) => catTrace (g ^ c)) l).prod

The trace of a block sum of rotations is the product of the cycle traces of its block lengths.

An arbitrary permutation

theorem RS.catTrace_permMor_powHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.RigidCategory A] (X : A) (g : CategoryTheory.End X) {n : ℕ} (π : Equiv.Perm (Fin n)) : catTrace (CategoryTheory.CategoryStruct.comp (permMor X n π) (powHom X g n)) = (Multiset.map (fun (c : ℕ) => catTrace (g ^ c)) (fullCycleType π)).prod

The trace of a permutation against a tensor power. It is the product of tr (g ^ c) over the full cycle type of the permutation, fixed points contributing tr g. Every permutation is conjugate to the block sum of rotations along its full cycle type, and the trace is a class function.