The base entry is multiplicative

The carrier entry of the base algebra respects the multiplication: multiplying in the base and entering the graded splitting algebra carrier agrees with entering twice and multiplying on the carrier. Together with unitality this is the monoid-morphism property of the base entry of the splitting data.

theorem RS.mul_chainBaseStage {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) (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (chainBaseStage A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (chainBaseStage A M M' d)) (modTensorAct A (symPowMod A M'.X 0) (symPowMod A M.X 0))

The base entry is multiplicative against the base action: multiplying in the base before entering the bottom stage is entering on the right tensor factor and acting.

theorem RS.splitOfBase_mul {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) [CategoryTheory.Limits.HasColimitsOfShape SmallNat D] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (splitOfBase A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (splitOfBase A M M' d) (splitOfBase A M M' d)) CategoryTheory.MonObj.mul

The base entry is multiplicative: the carrier entry of the base algebra respects the multiplication, the multiplicative half of the monoid-morphism property of the base entry.