Distribution of the permutation action over a tensor product

The distribution isomorphism (X ⊗ Y) ^ ⊗ n ≅ X ^ ⊗ n ⊗ Y ^ ⊗ n re-sorts the factors of a tensor power of a tensor product: stage by stage, the middle-four interchange (tensorμ) moves the newest pair of factors past the ones already sorted. The diagonal permutation action on the left matches the simultaneous action of the same permutation on the two sides.

The intertwining is proved for the top braiding first: braiding two compound factors distributes into the two plain braidings, which is the symmetric-category compatibility tensorμ_braid_swap conjugated through Mathlib's tensor_associativity. It then propagates along the recursions of insertTop and permMor exactly as the naturality lemmas of Deligne/PermNat.lean do, and linearises to the group algebra, whose diagonal double action is packaged as diagAlg.

The distribution isomorphism

noncomputable def RS.tensorμIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (P Q X Y : A) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q) (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj P X) (CategoryTheory.MonoidalCategoryStruct.tensorObj Q Y)

The middle-four interchange as an isomorphism: tensorμ and tensorδ are mutually inverse.

Equations

• RS.tensorμIso P Q X Y = { hom := CategoryTheory.MonoidalCategory.tensorμ P Q X Y, inv := CategoryTheory.MonoidalCategory.tensorδ P Q X Y, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

The distribution isomorphism (X ⊗ Y) ^ ⊗ n ≅ X ^ ⊗ n ⊗ Y ^ ⊗ n: at each stage the previous stage sorts all but the newest pair of factors, and the middle-four interchange routes that pair to its two destinations.

Equations

• One or more equations did not get rendered due to their size.
• RS.tensorPowDistrib X Y 0 = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)).symm

@[simp]

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

The distribution at arity zero is the inverse unitor.

The top braiding distributes

Braiding the top two compound factors of ((P ⊗ Q) ⊗ (X ⊗ Y)) ⊗ (X ⊗ Y) corresponds, through the two-stage interchange, to braiding the two top factors on each side at once. The computation is done at general objects, so that no tensor-power arity enters the rewriting: the two-stage interchange is re-associated into a single interchange against the paired factors (tensor_associativity), where the braiding of a tensor square distributes by the symmetric-category compatibility tensorμ_braid_swap.

theorem RS.tensorPowDistrib_swapTop {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (X Y : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (swapTop (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n) (tensorPowDistrib X Y (n + 2)).hom = CategoryTheory.CategoryStruct.comp (tensorPowDistrib X Y (n + 2)).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (swapTop X n) (swapTop Y n))

The distribution intertwines the top braiding: braiding the top two factors of (X ⊗ Y) ^ ⊗ (n + 2) corresponds to braiding the top two factors on each side simultaneously.

The insertion cycle and the full action

The intertwining propagates along the recursions of insertTop and permMor exactly as the naturality lemmas of PermNat.lean: each whiskered step passes through the distribution by naturality of the interchange, and each top braiding by the coherence above.

theorem RS.tensorPowDistrib_insertTop {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (X Y : A) (n k : ℕ) : CategoryTheory.CategoryStruct.comp (insertTop (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n k) (tensorPowDistrib X Y (n + 1)).hom = CategoryTheory.CategoryStruct.comp (tensorPowDistrib X Y (n + 1)).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (insertTop X n k) (insertTop Y n k))

The distribution intertwines the insertion cycle: bubbling the top compound factor down corresponds to bubbling the top factor on each side simultaneously. The proof follows the recursion of insertTop.

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

The distribution intertwines the permutation action: the diagonal action of σ on (X ⊗ Y) ^ ⊗ n corresponds to the simultaneous action of σ on the two sides. The proof is the recursion of permMor itself.

The diagonal double action

noncomputable def RS.diagPermHom {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (X Y : A) (n : ℕ) : Equiv.Perm (Fin n) →* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow A X n) (tensorPow A Y n))

The diagonal double action of a permutation on X ^ ⊗ n ⊗ Y ^ ⊗ n, as a monoid homomorphism: σ acts by its two actions tensored together.

Equations

• RS.diagPermHom X Y n = { toFun := fun (σ : Equiv.Perm (Fin n)) => CategoryTheory.MonoidalCategoryStruct.tensorHom (RS.permMor X n σ) (RS.permMor Y n σ), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem RS.diagPermHom_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] (X Y : A) (n : ℕ) (σ : Equiv.Perm (Fin n)) : (diagPermHom X Y n) σ = CategoryTheory.MonoidalCategoryStruct.tensorHom (permMor X n σ) (permMor Y n σ)

noncomputable def RS.diagAlg {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (X Y : A) (n : ℕ) : SymGroupAlgebra n →ₐ[ℂ] CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorObj (tensorPow A X n) (tensorPow A Y n))

The diagonal double action of the symmetric-group algebra on X ^ ⊗ n ⊗ Y ^ ⊗ n: the linear extension of σ ↦ permMor X n σ ⊗ₘ permMor Y n σ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RS.diagAlg_single {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (X Y : A) (n : ℕ) (σ : Equiv.Perm (Fin n)) : (diagAlg X Y n) (MonoidAlgebra.single σ 1) = CategoryTheory.MonoidalCategoryStruct.tensorHom (permMor X n σ) (permMor Y n σ)

The diagonal algebra map sends a group element to the tensor product of its two actions.

theorem RS.diagAlg_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (X Y : A) (n : ℕ) (x : SymGroupAlgebra n) : (diagAlg X Y n) x = x.coeff.sum fun (σ : Equiv.Perm (Fin n)) (c : ℂ) => c • CategoryTheory.MonoidalCategoryStruct.tensorHom (permMor X n σ) (permMor Y n σ)

The diagonal algebra map written out as a sum over the support: x acts by Σ_σ x_σ • (permMor X n σ ⊗ₘ permMor Y n σ).

theorem RS.tensorPowDistrib_permAlg {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] (X Y : A) {n : ℕ} (x : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp ((permAlg (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n) x) (tensorPowDistrib X Y n).hom = CategoryTheory.CategoryStruct.comp (tensorPowDistrib X Y n).hom ((diagAlg X Y n) x)

The distribution intertwines the group-algebra action: the diagonal action of any group-algebra element on (X ⊗ Y) ^ ⊗ n corresponds, through the distribution isomorphism, to its diagonal double action on X ^ ⊗ n ⊗ Y ^ ⊗ n. Both sides are ℂ-linear in the element, so the statement reduces to basis permutations, where it is tensorPowDistrib_permMor.