Splitting a tensor power into two blocks

The tensor power X ^ ⊗ (p + q) is isomorphic to X ^ ⊗ p ⊗ X ^ ⊗ q by reassociation alone (splitPow), and the structure carried by a tensor power respects the splitting: a block sum of permutations acts as the two permutations acting on the two blocks (permMor_blockSum), and the factorwise endomorphism power splits factorwise (powHom_splitPow). These are the identities that let the trace of a permutation-and-endomorphism word be computed block by block.

The splitting isomorphism

noncomputable def RS.splitPow {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) (p q : ℕ) : tensorPow A X (p + q) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow A X p) (tensorPow A X q)

The block splitting: X ^ ⊗ (p + q) ≅ X ^ ⊗ p ⊗ X ^ ⊗ q, by recursion on the upper block. At q = 0 it is the right unitor's inverse; each further factor is carried across by the associator, so the isomorphism is built from unitors and associators alone.

Equations

• RS.splitPow X x✝ 0 = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (RS.tensorPow A X x✝)).symm
• RS.splitPow X x✝ q.succ = CategoryTheory.MonoidalCategory.whiskerRightIso (RS.splitPow X x✝ q) X ≪≫ CategoryTheory.MonoidalCategoryStruct.associator (RS.tensorPow A X x✝) (RS.tensorPow A X q) X

@[simp]

theorem RS.splitPow_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) (p : ℕ) : splitPow X p 0 = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (tensorPow A X p)).symm

The empty upper block splits off along the right unitor.

theorem RS.splitPow_succ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) (p q : ℕ) : splitPow X p (q + 1) = CategoryTheory.MonoidalCategory.whiskerRightIso (splitPow X p q) X ≪≫ CategoryTheory.MonoidalCategoryStruct.associator (tensorPow A X p) (tensorPow A X q) X

The recursion equation: one more factor is carried across by the associator.

The block sum of two permutations

def RS.blockSum {p q : ℕ} (σ : Equiv.Perm (Fin p)) (τ : Equiv.Perm (Fin q)) : Equiv.Perm (Fin (p + q))

The block sum of two permutations: σ acts on the lower p slots and τ on the upper q, with no interaction between the blocks.

Equations

• RS.blockSum σ τ = finSumFinEquiv.permCongr (Equiv.sumCongr σ τ)

theorem RS.blockSum_castAdd {p q : ℕ} (σ : Equiv.Perm (Fin p)) (τ : Equiv.Perm (Fin q)) (i : Fin p) : (blockSum σ τ) (Fin.castAdd q i) = Fin.castAdd q (σ i)

The block sum acts on the lower block by σ.

theorem RS.blockSum_natAdd {p q : ℕ} (σ : Equiv.Perm (Fin p)) (τ : Equiv.Perm (Fin q)) (j : Fin q) : (blockSum σ τ) (Fin.natAdd p j) = Fin.natAdd p (τ j)

The block sum acts on the upper block by τ.

theorem RS.blockSum_of_zero {p : ℕ} (σ : Equiv.Perm (Fin p)) (τ : Equiv.Perm (Fin 0)) : blockSum σ τ = σ

Against an empty upper block the block sum is σ alone.

theorem RS.topImage_blockSum {p q : ℕ} (σ : Equiv.Perm (Fin p)) (τ : Equiv.Perm (Fin (q + 1))) : topImage (blockSum σ τ) = Fin.natAdd p (topImage τ)

The block sum sends the top slot within the upper block: its image is topImage τ, shifted past the lower block.

theorem RS.restPerm_blockSum {p q : ℕ} (σ : Equiv.Perm (Fin p)) (τ : Equiv.Perm (Fin (q + 1))) : restPerm (blockSum σ τ) = blockSum σ (restPerm τ)

Restriction respects the block sum: peeling the top slot off the upper block commutes with summing the blocks.

The braiding respects the splitting

theorem RS.swapTop_comp_splitPow {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) [CategoryTheory.SymmetricCategory A] (p q : ℕ) : CategoryTheory.CategoryStruct.comp (swapTop X (p + q)) (splitPow X p (q + 1 + 1)).hom = CategoryTheory.CategoryStruct.comp (splitPow X p (q + 1 + 1)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow A X p) (swapTop X q))

The braiding respects the splitting: braiding the last two factors of a tensor power is braiding them inside the upper block.

Transferring a splitting to one more factor

Bubbling respects the splitting

theorem RS.insertTop_comp_splitPow {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) [CategoryTheory.SymmetricCategory A] (p k q : ℕ) : k ≤ q → CategoryTheory.CategoryStruct.comp (insertTop X (p + q) k) (splitPow X p (q + 1)).hom = CategoryTheory.CategoryStruct.comp (splitPow X p (q + 1)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow A X p) (insertTop X q k))

Bubbling respects the splitting: bubbling the top factor down at most q slots never reaches the lower block, so it is bubbling inside the upper block.

Tensor powers respect the splitting

theorem RS.powHom_comp_splitPow {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) (g : CategoryTheory.End X) (p q : ℕ) : CategoryTheory.CategoryStruct.comp (powHom X g (p + q)) (splitPow X p q).hom = CategoryTheory.CategoryStruct.comp (splitPow X p q).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (powHom X g p) (powHom X g q))

The tensor power of an endomorphism respects the splitting.

The action respects the splitting

theorem RS.permMor_comp_splitPow {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] (X : A) [CategoryTheory.SymmetricCategory A] {p : ℕ} (σ : Equiv.Perm (Fin p)) (q : ℕ) (τ : Equiv.Perm (Fin q)) : CategoryTheory.CategoryStruct.comp (permMor X (p + q) (blockSum σ τ)) (splitPow X p q).hom = CategoryTheory.CategoryStruct.comp (splitPow X p q).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (permMor X p σ) (permMor X q τ))

The action respects the splitting: a block sum of permutations acts as the two permutations acting on the two blocks.