The plain diagonal shuffle and its equivariance

The diagonal shuffle (X ⊗ Y) ^ ⊗ n ≅ X ^ ⊗ n ⊗ Y ^ ⊗ n re-sorts a tensor power of a tensor product: the empty power is the inverse unitor, and each step of the recursion is the middle-four interchange tensorμ, inverted by tensorδ. The shuffle is equivariant for the symmetric-group actions: the diagonal action of a permutation on the (X ⊗ Y)-factors passes through it to the simultaneous action on the two plain powers.

The isomorphism and its intertwining are carried by the distribution isomorphism tensorPowDistrib of Deligne/MixedDiag.lean, whose top-braiding square reduces to the componentwise braidings through Mathlib's tensor_associativity, and whose functoriality follows the recursions of insertTop and permMor. This module presents the shuffle under its own name, with the defining recursion equations on both the forward and the inverse maps and the equivariance statements in the form the plain tensor-power calculus consumes.

noncomputable def RS.plainShuffle {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X Y : D) (n : ℕ) : tensorPow D (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow D X n) (tensorPow D Y n)

The plain diagonal shuffle (X ⊗ Y) ^ ⊗ n ≅ X ^ ⊗ n ⊗ Y ^ ⊗ n: the empty power is the inverse unitor, and each further step of the recursion is the middle-four interchange tensorμ, inverted by tensorδ. It is the distribution isomorphism tensorPowDistrib, under the shuffle's own name.

Equations

• RS.plainShuffle X Y n = RS.tensorPowDistrib X Y n

@[simp]

theorem RS.plainShuffle_zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X Y : D) : plainShuffle X Y 0 = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).symm

The empty shuffle is the inverse unitor.

@[simp]

theorem RS.plainShuffle_succ_hom {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X Y : D) (n : ℕ) : (plainShuffle X Y (n + 1)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (plainShuffle X Y n).hom (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) (CategoryTheory.MonoidalCategory.tensorμ (tensorPow D X n) (tensorPow D Y n) X Y)

The defining recursion of the shuffle, on the forward maps: the lower factors are shuffled and the newest (X ⊗ Y)-pair is routed to its two destinations by the interchange.

@[simp]

theorem RS.plainShuffle_succ_inv {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X Y : D) (n : ℕ) : (plainShuffle X Y (n + 1)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ (tensorPow D X n) (tensorPow D Y n) X Y) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (plainShuffle X Y n).inv (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

The defining recursion of the shuffle, on the inverse maps: the newest pair is split off by the inverse interchange and the lower factors are unshuffled.

theorem RS.plainShuffle_permMor {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (X Y : D) (n : ℕ) (σ : Equiv.Perm (Fin n)) : CategoryTheory.CategoryStruct.comp (permMor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n σ) (plainShuffle X Y n).hom = CategoryTheory.CategoryStruct.comp (plainShuffle X Y n).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (permMor X n σ) (permMor Y n σ))

Permutation equivariance of the plain shuffle: the diagonal action of a permutation on (X ⊗ Y) ^ ⊗ n passes through the shuffle to its simultaneous action on the two plain tensor powers.