The block trace factorization

The trace of a block permutation against the block-diagonal power factors into cycle traces of the block endomorphism — the engine of the Frobenius identity at every ambient arity.

The S_k-level cycle normal form transports through the block-permutation homomorphism for free; the tensor-splitting slices carry finCongr casts because n·(a+b) = n·a + n·b is propositional, managed by the arity-cast transport endCast.

Trace cyclicity

Arity-cast transport

noncomputable def RS.endCast {R : ℕ} (f : EdgeRankParameter R) {a b : ℕ} (h : a = b) (x : skeinEnd f a) : skeinEnd f b

Transport of a strand endomorphism along an arity equality: conjugation by the boundary cast.

Equations

• RS.endCast f h x = h ▸ x

theorem RS.skeinTrace_endCast {R : ℕ} (f : EdgeRankParameter R) {a b : ℕ} (h : a = b) (x : skeinEnd f a) : skeinTrace f b (endCast f h x) = skeinTrace f a x

Cast transport preserves the trace.

theorem RS.endCast_mul {R : ℕ} (f : EdgeRankParameter R) {a b : ℕ} (h : a = b) (x y : skeinEnd f a) : endCast f h (x * y) = endCast f h x * endCast f h y

Cast transport is multiplicative.

Block tensor calculus

Braiding commutativity at block arities

Swap commutativity at block level

The block cycle trace

theorem RS.skeinTrace_blockCycle {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) (g : skeinEnd f n) (c : ℕ) : skeinTrace f (n * (c + 1)) (permClass f (n * (c + 1)) (blockPerm n (finRotate (c + 1))) * blockPow f n g (c + 1)) = skeinTrace f n (g ^ (c + 1))

The block cycle trace: closing the block rotation against c diagonal blocks is the trace of the c-th power, via the block splice.

theorem RS.blockPerm_mul_blockPow_comm {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) {k : ℕ} (σ : Equiv.Perm (Fin k)) (g : skeinEnd f n) : permClass f (n * k) (blockPerm n σ) * blockPow f n g k = blockPow f n g k * permClass f (n * k) (blockPerm n σ)

Block permutations commute with the block-diagonal power.

theorem RS.skeinTrace_blockCycles_mul_pow {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) (l : List ℕ) (hl : ∀ c ∈ l, 1 ≤ c) (g : skeinEnd f n) : skeinTrace f (n * l.sum) (permClass f (n * l.sum) (blockPerm n (blockCycles l)) * blockPow f n g l.sum) = (List.map (fun (c : ℕ) => skeinTrace f n (g ^ c)) l).prod

Block factorization over the block-cycle normal form.

theorem RS.skeinTrace_blockPerm_mul_pow {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) {k : ℕ} (π : Equiv.Perm (Fin k)) (g : skeinEnd f n) : skeinTrace f (n * k) (permClass f (n * k) (blockPerm n π) * blockPow f n g k) = (Multiset.map (fun (c : ℕ) => skeinTrace f n (g ^ c)) π.cycleType).prod * skeinTrace f n (g ^ 1) ^ (k - π.cycleType.sum)

The block trace factorization: the trace of a block permutation against the block-diagonal power is the cycle-type product of block power traces, fixed points included.