The block cycle trace

Closing a block rotation against c + 1 diagonal copies of g gives the trace of g ^ (c + 1): the rotation carries each copy onto the next, and after c + 1 turns the copies have composed.

The rotation by one block is blockPerm n (finRotate (c+1)), which is blockRot (n*c) n; the splice partialCloseBlockSplice peels one block off it, first at fragments and then at trace values. An induction on the number of blocks then turns the tensor of a tuple into the tuple's cyclic composite, which for a constant tuple is a power.

The rotation by one block

theorem RS.blockPerm_finRotate_eq_blockRot (n c : ℕ) : blockPerm n (finRotate (c + 1)) = blockRot (n * c) n

blockPerm n (finRotate (c+1)) equals blockRot (n*c) n: both rotate strands by n modulo n*(c+1).

Trace and interchange for the block tensor

theorem RS.skeinTrace_blockTensorEnd {R : ℕ} (f : EdgeRankParameter R) {a b : ℕ} (u : skeinEnd f a) (v : skeinEnd f b) : skeinTrace f (a + b) (blockTensorEnd f u v) = skeinTrace f a u * skeinTrace f b v

Trace of a block tensor product.

theorem RS.blockTensorEnd_mul {R : ℕ} (f : EdgeRankParameter R) {a b : ℕ} (u₁ u₂ : skeinEnd f a) (v₁ v₂ : skeinEnd f b) : blockTensorEnd f u₁ v₁ * blockTensorEnd f u₂ v₂ = blockTensorEnd f (u₁ * u₂) (v₁ * v₂)

Interchange law for blockTensorEnd multiplication.

The rotation step at fragments

The rotation step at trace values

theorem RS.skeinTrace_block_rot_step {R : ℕ} (f : EdgeRankParameter R) (K n : ℕ) (A : skeinEnd f (K + n)) (g : skeinEnd f n) : skeinTrace f (K + n + n) (permClass f (K + n + n) (blockRot (K + n) n) * blockTensorEnd f A g) = skeinTrace f (K + n) (permClass f (K + n) (blockRot K n) * (blockTensorEnd f 1 g * A))

The block rotation step: the trace at K+n+n strands of (blockRot * tensor) equals the trace at K+n strands of (blockRot * pad * accumulated).

The block tuple tensor and the block cycle composite

noncomputable def RS.blockTupleTensor {R : ℕ} (f : EdgeRankParameter R) (n k : ℕ) : (Fin k → skeinEnd f n) → skeinEnd f (n * k)

The block tuple tensor: tensor product of a tuple of n-strand endomorphisms, as an endomorphism of the n*k-strand object.

Equations

• RS.blockTupleTensor f n 0 x_2 = 1
• RS.blockTupleTensor f n k.succ G = RS.blockTensorEnd f (RS.blockTupleTensor f n k fun (i : Fin k) => G i.castSucc) (G (Fin.last k))

noncomputable def RS.blockCycleComp {R : ℕ} (f : EdgeRankParameter R) (n k : ℕ) : (Fin k → skeinEnd f n) → skeinEnd f n

The block cycle composite: G(k-1) * ⋯ * G(0) in the n-strand endomorphism algebra.

Equations

• RS.blockCycleComp f n 0 x_2 = 1
• RS.blockCycleComp f n k.succ G = G (Fin.last k) * RS.blockCycleComp f n k fun (i : Fin k) => G i.castSucc

Padding and updating the tuple

theorem RS.blockPadLeft_mul_blockTupleTensor {R : ℕ} (f : EdgeRankParameter R) (K n : ℕ) (H : Fin (K + 1) → skeinEnd f n) (g : skeinEnd f n) : blockTensorEnd f 1 g * blockTupleTensor f n (K + 1) H = blockTupleTensor f n (K + 1) (Function.update H (Fin.last K) (g * H (Fin.last K)))

The padded product updates the last tuple entry.

theorem RS.blockCycleComp_update_last {R : ℕ} (f : EdgeRankParameter R) (K n : ℕ) (H : Fin (K + 1) → skeinEnd f n) (g : skeinEnd f n) : blockCycleComp f n (K + 1) (Function.update H (Fin.last K) (g * H (Fin.last K))) = g * blockCycleComp f n (K + 1) H

The cycle composite of a last-entry update: the padding factor peels off.

The cycle induction

theorem RS.skeinTrace_block_cycle {R : ℕ} (f : EdgeRankParameter R) (n k : ℕ) (G : Fin (k + 1) → skeinEnd f n) : skeinTrace f (n * (k + 1)) (permClass f (n * (k + 1)) (blockPerm n (finRotate (k + 1))) * blockTupleTensor f n (k + 1) G) = skeinTrace f n (blockCycleComp f n (k + 1) G)

The block cycle-trace lemma: the trace of a block rotation composed with a block tuple tensor is the trace of the block cycle composite.

Constant tuples

theorem RS.blockCycleComp_const {R : ℕ} (f : EdgeRankParameter R) (n k : ℕ) (g : skeinEnd f n) : (blockCycleComp f n k fun (x : Fin k) => g) = g ^ k

The block cycle composite of a constant tuple is the power.

theorem RS.blockTupleTensor_const {R : ℕ} (f : EdgeRankParameter R) (n k : ℕ) (g : skeinEnd f n) : (blockTupleTensor f n k fun (x : Fin k) => g) = blockPow f n g k

The block tuple tensor of a constant tuple is the block power.

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+1 diagonal blocks yields the trace of the (c+1)-th power.