The multiplication of the chain algebra

The symmetric multiplication descends through the module-tensor coequalizer of two symmetric powers, giving a module map of bundles; through the interchange, the tensor product of two chain stages multiplies into the chain stage of summed arity.

theorem RS.symMul_modTensor_cond {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (symPowMod A X m) (symPowMod A X n)) (symMul A X (m + 1) (n + 1)) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (symPowMod A X m) (symPowMod A X n)) (symMul A X (m + 1) (n + 1))

The two module-tensor legs of a pair of symmetric powers agree after the symmetric multiplication.

noncomputable def RS.symMulDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : modTensor A (symPowMod A X m) (symPowMod A X n) ⟶ symPow A X (m + 1 + n + 1)

The descended symmetric multiplication on the module tensor product of two symmetric powers.

Equations

• RS.symMulDesc A X m n = RS.modTensorDesc A (RS.symPowMod A X m) (RS.symPowMod A X n) (RS.symMul A X (m + 1) (n + 1)) ⋯

@[simp]

theorem RS.modTensorπ_symMulDesc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorπ A (symPowMod A X m) (symPowMod A X n)) (symMulDesc A X m n) = symMul A X (m + 1) (n + 1)

Defining equation of the descended multiplication.

@[simp]

theorem RS.modTensorπ_symMulDesc_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) {Z : D} (h : symPow A X (m + 1 + n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A (symPowMod A X m) (symPowMod A X n)) (CategoryTheory.CategoryStruct.comp (symMulDesc A X m n) h) = CategoryTheory.CategoryStruct.comp (symMul A X (m + 1) (n + 1)) h

Defining equation of the descended multiplication.

theorem RS.symMulDesc_act {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorAct A (symPowMod A X m) (symPowMod A X n)) (symMulDesc A X m n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (symMulDesc A X m n)) (symPowAct A X (m + 1 + n))

The descended multiplication intertwines the module actions.

noncomputable def RS.symMulMod {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : modTensorMod A (symPowMod A X m) (symPowMod A X n) ⟶ symPowMod A X (m + 1 + n)

The descended symmetric multiplication as a map of modules.

Equations

• RS.symMulMod A X m n = CategoryTheory.Mod.Hom.mk' (RS.symMulDesc A X m n) ⋯

noncomputable def RS.chainStage {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (k : ℕ) : D

One stage of the splitting chain: the module tensor product of matching symmetric powers of the dual pair.

Equations

• RS.chainStage A M M' k = RS.modTensor A (RS.symPowMod A M'.X k) (RS.symPowMod A M.X k)

noncomputable def RS.chainMul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ 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] (M M' : CategoryTheory.Mod D A) (m n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainStage A M M' m) (chainStage A M M' n) ⟶ chainStage A M M' (m + 1 + n)

The chain multiplication: two stages interchange and multiply into the stage of summed arity.

Equations

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

theorem RS.tensorHom_π_chainMul {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ 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] (M M' : CategoryTheory.Mod D A) (m n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ 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.MonoidalCategory.tensorμ (symPow A M'.X (m + 1)) (symPow A M.X (m + 1)) (symPow A M'.X (n + 1)) (symPow A M.X (n + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symMul A M'.X (m + 1) (n + 1)) (symMul A M.X (m + 1) (n + 1))) (modTensorπ A (symPowMod A M'.X (m + 1 + n)) (symPowMod A M.X (m + 1 + n))))

Defining equation of the chain multiplication: under the stage projections it is the raw crossing followed by the symmetric multiplications.