Defining equation of the carrier-level pair product

Through the projection onto the relative tensor product, the carrier-level pair product of the splitting data is computed by the graded multiplication of the carrier: the two module entries enter their components at the bottom stage and multiply into the degree-zero component two stages up. This is the defining equation of the pair product field of the splitting data of the Key Lemma.

theorem RS.modTensorπ_splitPairMul {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 (modTensorπ A M M') (splitPairMul A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (splitIns A M M' d) (splitIns' A M M' d)) CategoryTheory.MonObj.mul

Defining equation of the carrier-level pair product: through the projection of the relative tensor product, the pair product is the graded product of the two module entries.