The pair product on the graded carrier

The descended pair product of the module entries lands two stages up the degree-zero line of the graded splitting algebra carrier. Through the component insertions, the transitions are absorbed and the copair element multiplies to the unit of the carrier — the section identity of the splitting data of the Key Lemma.

noncomputable def RS.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] (d : ModDualityDatum A M M') : modTensor A M M' ⟶ chainBGr A M M' d

The pair product on the carrier: the descended pair product of the entries, entering the degree-zero component two stages up.

Equations

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

theorem RS.copairUnit_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] (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (copairUnit A M M' d) (splitPairMul A M M' d) = chainBGrUnit A M M' d

The copair element multiplies to the unit on the carrier: the section identity of the splitting data.