The trace of a cycle against a tensor power

The trace of the insertion cycle against the tensor power of an endomorphism: bubbling the top factor down k slots and letting g act on every factor traces to tr(g ^ (k + 1)) times tr g on each of the untouched factors.

The argument descends one arity at a time. Tracing out the top factor turns the bubbling at arity n + 1 into the bubbling at arity n preceded by one more copy of g on the new top factor — the partial trace of the braiding is the identity — and the full trace is unchanged by the descent (catTrace_ptr). Carrying an arbitrary endomorphism on the top factor through the induction is what makes the accumulated copies of g bookkeepable.

The trace of a tensor power

theorem RS.catTrace_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 : ℕ) : catTrace (powHom X g n) = catTrace g ^ n

The trace of a tensor power of an endomorphism is the power of its trace.

Bubbling one slot down

The cycle trace

theorem RS.catTrace_insertTop_powHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.RigidCategory A] (X : A) (g : CategoryTheory.End X) (k n : ℕ) : k ≤ n → ∀ (h : CategoryTheory.End X), catTrace (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow A X n) h) (CategoryTheory.CategoryStruct.comp (insertTop X n k) (powHom X g (n + 1)))) = catTrace g ^ (n - k) * catTrace (CategoryTheory.CategoryStruct.comp h (g ^ (k + 1)))

The trace of the insertion cycle against a tensor power. Bubbling the top factor down k slots and letting g act on every factor, with a further endomorphism h on the top factor, traces to tr (h ∘ g ^ (k + 1)) times one copy of tr g for each factor the bubbling does not reach.

theorem RS.catTrace_insertTop {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.RigidCategory A] (X : A) (g : CategoryTheory.End X) {k n : ℕ} (hk : k ≤ n) : catTrace (CategoryTheory.CategoryStruct.comp (insertTop X n k) (powHom X g (n + 1))) = catTrace g ^ (n - k) * catTrace (g ^ (k + 1))

The trace of a cycle against a tensor power: bubbling the top factor down k slots and letting g act on every factor traces to tr (g ^ (k + 1)) times one copy of tr g for each factor the bubbling does not reach.