The block tower

The symmetric group S_k acting by block permutations on n·k strands: the permutation representation, the block-diagonal tensor power, and the PermTower structure at the n-strand ambient — the scaffolding for nilpotent-trace vanishing at every arity.

The step arithmetic is definitional: n * (k + 1) ≡ n * k + n, so the recursive block constructions live at the same indices as the tensor structure.

Block permutations

noncomputable def RS.blockPerm (n : ℕ) {k : ℕ} (σ : Equiv.Perm (Fin k)) : Equiv.Perm (Fin (n * k))

The block permutation: σ : S_k acting on k contiguous blocks of n strands.

Equations

• RS.blockPerm n σ = (finCongr ⋯).permCongr (finProdFinEquiv.permCongr (Equiv.prodCongr σ (Equiv.refl (Fin n))))

theorem RS.blockPerm_one (n k : ℕ) : blockPerm n 1 = 1

Block permutation of the identity.

theorem RS.blockPerm_mul (n : ℕ) {k : ℕ} (σ τ : Equiv.Perm (Fin k)) : blockPerm n (σ * τ) = blockPerm n σ * blockPerm n τ

Block permutations are multiplicative.

noncomputable def RS.blockPermHom (n k : ℕ) : Equiv.Perm (Fin k) →* Equiv.Perm (Fin (n * k))

The block-permutation monoid homomorphism.

Equations

• RS.blockPermHom n k = { toFun := RS.blockPerm n, map_one' := ⋯, map_mul' := ⋯ }

theorem RS.blockPerm_val (n : ℕ) {k : ℕ} (σ : Equiv.Perm (Fin k)) (q : Fin k) (r : Fin n) : (blockPerm n σ) ⟨n * ↑q + ↑r, ⋯⟩ = ⟨n * ↑(σ q) + ↑r, ⋯⟩

The value of a block permutation on n·q + r.

The block representation

noncomputable def RS.blockRep {R : ℕ} (f : EdgeRankParameter R) (n k : ℕ) : SymGroupAlgebra k →ₐ[ℂ] skeinEnd f (n * k)

The block representation of the group algebra of S_k on n·k strands.

Equations

• RS.blockRep f n k = (MonoidAlgebra.lift ℂ (RS.skeinEnd f (n * k)) (Equiv.Perm (Fin k))) ((RS.permToEnd f (n * k)).comp (RS.blockPermHom n k))

theorem RS.blockRep_of {R : ℕ} (f : EdgeRankParameter R) (n k : ℕ) (σ : Equiv.Perm (Fin k)) : (blockRep f n k) ((MonoidAlgebra.of ℂ (Equiv.Perm (Fin k))) σ) = permClass f (n * k) (blockPerm n σ)

blockRep on a single permutation.

The block-diagonal power

noncomputable def RS.blockTensorEnd {R : ℕ} (f : EdgeRankParameter R) {a b : ℕ} (u : skeinEnd f a) (v : skeinEnd f b) : skeinEnd f (a + b)

The End-typed tensor at block arities.

Equations

• RS.blockTensorEnd f u v = CategoryTheory.MonoidalCategoryStruct.tensorHom u v

noncomputable def RS.blockPow {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) (g : skeinEnd f n) (k : ℕ) : skeinEnd f (n * k)

The block-diagonal tensor power: k copies of an n-strand endomorphism. The index arithmetic is definitional: n * (k + 1) ≡ n * k + n.

Equations

• RS.blockPow f n g 0 = 1
• RS.blockPow f n g k.succ = RS.blockTensorEnd f (RS.blockPow f n g k) g

The block permutation tower

theorem RS.blockEnd_finrank_le {R : ℕ} (f : EdgeRankParameter R) (n k : ℕ) : Module.finrank ℂ (skeinEnd f (n * k)) ≤ (R ^ n) ^ (2 * k)

The dimension bound at block arities: R ^ (2·n·k) = (R ^ n) ^ (2·k).

theorem RS.blockRep_compat {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) {j k : ℕ} (h : j ≤ k) (x : SymGroupAlgebra j) : (blockRep f n j) x = 0 → (blockRep f n k) ((symCast h) x) = 0

Vanishing propagates along the standard embeddings of block representations.

noncomputable def RS.blockPermTower {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) : PermTower (fun (k : ℕ) => skeinEnd f (n * k)) ((↑R ^ n) ^ 2)

The block permutation tower: S_k acting by block permutations on the n·k-strand endomorphism algebras, of growth (R ^ n) ^ 2.

Equations

• RS.blockPermTower f n = { rep := fun (k : ℕ) => RS.blockRep f n k, compat := ⋯, bound := ⋯ }