The interchange is linear over the base

The action compatibility of the interchange: acting on the first tensor factor and interchanging is reassociating, interchanging, and acting on the nested module tensor product. Together with the functoriality of the module tensor product this makes the chain multiplication bilinear over the base, which is what the structure morphism of the splitting-chain algebra multiplies through.

theorem RS.interchange_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorAct A N₁ N₂) (modTensor A P₁ P₂)) (interchange A N₁ N₂ P₁ P₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (modTensor A N₁ N₂) (modTensor A P₁ P₂)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (interchange A N₁ N₂ P₁ P₂)) (modTensorAct A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂)))

The interchange is linear over the base: the action on the first factor interchanges to the action on the nested module tensor product.

theorem RS.interchange_comm {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (β_ (modTensor A N₁ N₂) (modTensor A P₁ P₂)).hom (interchange A P₁ P₂ N₁ N₂) = CategoryTheory.CategoryStruct.comp (interchange A N₁ N₂ P₁ P₂) (modTensorMap A (modTensorSwapMod A N₁ P₁) (modTensorSwapMod A N₂ P₂))

Commutativity of the interchange: the block braiding interchanges to the nested braidings, by the braiding law of the crossing.

theorem RS.interchange_actMid {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (N₁ N₂ P₁ P₂ : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A N₁ N₂) (modTensorAct A P₁ P₂)) (interchange A N₁ N₂ P₁ P₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (modTensor A N₁ N₂) A (modTensor A P₁ P₂)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ (modTensor A N₁ N₂) A).hom (modTensor A P₁ P₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (modTensor A N₁ N₂) (modTensor A P₁ P₂)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (interchange A N₁ N₂ P₁ P₂)) (modTensorAct A (modTensorMod A N₁ P₁) (modTensorMod A N₂ P₂)))))

The interchange is linear in the second factor: the middle action braids to the front and the first-factor linearity applies through commutativity.

theorem RS.chainMul_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (M M' : CategoryTheory.Mod D A) (m n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorAct A (symPowMod A M'.X m) (symPowMod A M.X m)) (modTensor A (symPowMod A M'.X n) (symPowMod A M.X n))) (chainMul A M M' m n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (modTensor A (symPowMod A M'.X m) (symPowMod A M.X m)) (modTensor A (symPowMod A M'.X n) (symPowMod A M.X n))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (chainMul A M M' m n)) (modTensorAct A (symPowMod A M'.X (m + 1 + n)) (symPowMod A M.X (m + 1 + n))))

The chain multiplication is linear over the base in the first stage: the interchange linearity composed with the functoriality of the module tensor product. Stated at the unwrapped module tensor products; the stage forms follow by definitional unfolding.

theorem RS.chainMul2_actLeft {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (M M' : CategoryTheory.Mod D A) (p q r s : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (modTensorAct A (symPowMod A M'.X p) (symPowMod A M.X q)) (modTensor A (symPowMod A M'.X r) (symPowMod A M.X s))) (chainMul2 A M M' p q r s) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (modTensor A (symPowMod A M'.X p) (symPowMod A M.X q)) (modTensor A (symPowMod A M'.X r) (symPowMod A M.X s))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (chainMul2 A M M' p q r s)) (modTensorAct A (symPowMod A M'.X (p + 1 + r)) (symPowMod A M.X (q + 1 + s))))

The two-index chain multiplication is linear over the base in the first stage: the interchange linearity composed with the functoriality of the module tensor product, at four independent symmetric-power arities. Stated at the unwrapped module tensor products; the two-index stage forms follow by definitional unfolding. The diagonal p = q, r = s is chainMul_actLeft.

theorem RS.chainMul2_actMid {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] (M M' : CategoryTheory.Mod D A) (p q r s : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (modTensor A (symPowMod A M'.X p) (symPowMod A M.X q)) (modTensorAct A (symPowMod A M'.X r) (symPowMod A M.X s))) (chainMul2 A M M' p q r s) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (modTensor A (symPowMod A M'.X p) (symPowMod A M.X q)) A (modTensor A (symPowMod A M'.X r) (symPowMod A M.X s))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ (modTensor A (symPowMod A M'.X p) (symPowMod A M.X q)) A).hom (modTensor A (symPowMod A M'.X r) (symPowMod A M.X s))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A (modTensor A (symPowMod A M'.X p) (symPowMod A M.X q)) (modTensor A (symPowMod A M'.X r) (symPowMod A M.X s))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (chainMul2 A M M' p q r s)) (modTensorAct A (symPowMod A M'.X (p + 1 + r)) (symPowMod A M.X (q + 1 + s))))))

The two-index chain multiplication is linear over the base in the second factor: the middle action braids to the front and the interchange linearity applies. Stated at the unwrapped module tensor products; the stage forms follow by definitional unfolding.