Assembly of the splitting-data entries on the graded carrier

The stage-level entries of the splitting algebra — the base algebra, the module and the dual module — are lifted from the two-index chain stages to the graded splitting algebra carrier: the base enters the degree-zero component at the bottom stage, the module the degree +1 component and the dual module the degree −1 component. The base entry carries the unit to the unit, and both module entries are linear over the base through the base entry, in the exact shape of the splitting data of the Key Lemma.

noncomputable def RS.splitOfBase {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') : A ⟶ chainBGr A M M' d

The base entry on the carrier: the base algebra enters the degree-zero component at the bottom stage.

Equations

• RS.splitOfBase A M M' d = CategoryTheory.CategoryStruct.comp (RS.chainBaseStage A M M' d) (CategoryTheory.CategoryStruct.comp (RS.chainBGrCompι A M M' d 0 0) (RS.chainBGrι A M M' d 0))

noncomputable def RS.splitIns {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') : M.X ⟶ chainBGr A M M' d

The module entry on the carrier: the module enters the degree +1 component at the bottom stage.

Equations

• RS.splitIns A M M' d = CategoryTheory.CategoryStruct.comp (RS.chainSeedQ A M M' d) (CategoryTheory.CategoryStruct.comp (RS.chainBGrCompι A M M' d 1 0) (RS.chainBGrι A M M' d 1))

noncomputable def RS.splitIns' {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') : M'.X ⟶ chainBGr A M M' d

The dual entry on the carrier: the dual module enters the degree −1 component at the bottom stage, through the arity transport identifying the bottom stage of the −1 line.

Equations

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

theorem RS.splitOfBase_unit {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 CategoryTheory.MonObj.one (splitOfBase A M M' d) = chainBGrUnit A M M' d

The base entry carries the unit to the unit: the carrier entry of the base algebra is unital.

theorem RS.splitIns_linear {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 (actLeft A M.X) (splitIns A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (splitIns A M M' d)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (splitOfBase A M M' d) (chainBGr A M M' d)) CategoryTheory.MonObj.mul)

The module entry is linear over the base, through the carrier entry of the base algebra: the splitting-data shape of the linearity law.

theorem RS.splitIns'_linear {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 (actLeft A M'.X) (splitIns' A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (splitIns' A M M' d)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (splitOfBase A M M' d) (chainBGr A M M' d)) CategoryTheory.MonObj.mul)

The dual entry is linear over the base, through the carrier entry of the base algebra: the splitting-data shape of the linearity law for the dual module.