The skein Frobenius identity

The bridge from permutation classes to bundle-map classes, and the one consequence the trace calculus needs: the class of a block-sum permutation is the tensor of the two block classes.

Both are fragment computations. A permutation fragment relabels the strand bundle by the permutation on the outgoing labels, which is exactly a bundle map; and conjugating a block sum by finSumFinEquiv is the tensor of the blocks. The trace factorization these feed is BlockFactor.lean, and the Frobenius identity itself BlockAssembly.lean.

Bridge: permutation classes are bundle-map classes

theorem RS.permClass_eq_bundleMapClass {R : ℕ} (f : EdgeRankParameter R) (n : ℕ) (σ : Equiv.Perm (Fin n)) : permClass f n σ = bundleMapClass f σ

Bridge lemma: permClass f n σ = bundleMapClass f σ.

The tensor of block classes

theorem RS.permClass_sumCongr {R : ℕ} (f : EdgeRankParameter R) (a b : ℕ) (σ : Equiv.Perm (Fin a)) (τ : Equiv.Perm (Fin b)) : permClass f (a + b) (finSumFinEquiv.permCongr (Equiv.sumCongr σ τ)) = CategoryTheory.MonoidalCategoryStruct.tensorHom (permClass f a σ) (permClass f b τ)

The permutation class of a block-sum permutation is the tensor of the block classes.