The graded splitting algebra carrier

The full splitting algebra is the sum over the integer degrees of the graded components: degree a is the line through the starting bidegree ((−a)⁺, a⁺), so nonnegative degrees extend the M-arity and negative degrees the M'-arity. The balanced degree is the algebra of the splitting chain, carrying the unit.

noncomputable def RS.chainBGrComponent {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] (d : ModDualityDatum A M M') (a : ℤ) : D

The graded component at an integer degree: the line through ((−a)⁺, a⁺) — nonnegative degrees raise the M-arity, negative degrees the M'-arity.

Equations

• RS.chainBGrComponent A M M' d a = RS.chainBdeg A M M' d (-a).toNat a.toNat

noncomputable def RS.chainBGrComponentZeroIso {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] (d : ModDualityDatum A M M') : chainBGrComponent A M M' d 0 ≅ chainB A M M' d

The degree-zero component is the splitting-chain algebra.

Equations

• RS.chainBGrComponentZeroIso A M M' d = RS.chainBdegZeroIso A M M' d

noncomputable def RS.chainBdegShiftIso {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] (d : ModDualityDatum A M M') (p₀ q₀ n : ℕ) : chainBdeg A M M' d (p₀ + n) (q₀ + n) ≅ chainBdeg A M M' d p₀ q₀

The iterated line shift: raising both offsets n times is the identity on the colimit.

Equations

• RS.chainBdegShiftIso A M M' d p₀ q₀ 0 = CategoryTheory.Iso.refl (RS.chainBdeg A M M' d (p₀ + 0) (q₀ + 0))
• RS.chainBdegShiftIso A M M' d p₀ q₀ n.succ = RS.chainBdegSuccIso A M M' d (p₀ + n) (q₀ + n) ≪≫ RS.chainBdegShiftIso A M M' d p₀ q₀ n

noncomputable def RS.chainBGrCompNormIso {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] (d : ModDualityDatum A M M') (a b : ℤ) : chainBdeg A M M' d ((-a).toNat + (-b).toNat) (a.toNat + b.toNat) ≅ chainBGrComponent A M M' d (a + b)

The pairwise offsets normalise to the sum degree: the line through the sum of two components' offsets is the raised line of the sum-degree component.

Equations

• RS.chainBGrCompNormIso A M M' d a b = CategoryTheory.eqToIso ⋯ ≪≫ RS.chainBdegShiftIso A M M' d (-(a + b)).toNat (a + b).toNat (a.toNat + b.toNat - (a + b).toNat)

noncomputable def RS.chainBGrCompMul {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b : ℤ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBGrComponent A M M' d a) (chainBGrComponent A M M' d b) ⟶ chainBGrComponent A M M' d (a + b)

The pairwise graded product: two components multiply into the sum-degree component through the offset normalisation.

Equations

• RS.chainBGrCompMul A M M' d a b = CategoryTheory.CategoryStruct.comp (RS.chainBdegMul A M M' d (-a).toNat a.toNat (-b).toNat b.toNat) (RS.chainBGrCompNormIso A M M' d a b).hom

noncomputable def RS.chainBGr {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') : D

The graded splitting algebra carrier: the sum of the graded components over all integer degrees.

Equations

• RS.chainBGr A M M' d = ∐ fun (a : ℤ) => RS.chainBGrComponent A M M' d a

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

The inclusion of a graded component.

Equations

• RS.chainBGrι A M M' d a = CategoryTheory.Limits.Sigma.ι (fun (a : ℤ) => RS.chainBGrComponent A M M' d a) a

noncomputable def RS.chainBGrUnit {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.MonoidalCategoryStruct.tensorUnit D ⟶ chainBGr A M M' d

The unit of the graded splitting algebra: the unit of the balanced algebra, in degree zero.

Equations

• RS.chainBGrUnit A M M' d = CategoryTheory.CategoryStruct.comp (RS.chainBUnit A M M' d) (CategoryTheory.CategoryStruct.comp (RS.chainBGrComponentZeroIso A M M' d).inv (RS.chainBGrι A M M' d 0))

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

The projection onto the degree-zero component: the identity in degree zero and zero elsewhere.

Equations

• RS.chainBGrProjZero A M M' d = CategoryTheory.Limits.Sigma.desc fun (b : ℤ) => if h : b = 0 then CategoryTheory.eqToHom ⋯ else 0

@[simp]

theorem RS.chainBGrι_projZero {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 (chainBGrι A M M' d 0) (chainBGrProjZero A M M' d) = CategoryTheory.CategoryStruct.id (chainBGrComponent A M M' d 0)

The degree-zero inclusion is split by the projection.

@[simp]

theorem RS.chainBGrι_projZero_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)] [∀ (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') {Z : D} (h : chainBGrComponent A M M' d 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainBGrι A M M' d 0) (CategoryTheory.CategoryStruct.comp (chainBGrProjZero A M M' d) h) = h

The degree-zero inclusion is split by the projection.

theorem RS.chainBGrUnit_ne_zero {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') (h : chainBUnit A M M' d ≠ 0) : chainBGrUnit A M M' d ≠ 0

The graded unit does not vanish when the balanced unit does not: the degree-zero retraction detects it.

noncomputable def RS.chainBGrMulStageCocone {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] (d : ModDualityDatum A M M') (a : ℤ) : CategoryTheory.Limits.Cocone ((CategoryTheory.Discrete.functor fun (b : ℤ) => chainBGrComponent A M M' d b).comp (CategoryTheory.MonoidalCategory.tensorLeft (chainBGrComponent A M M' d a)))

The multiply-then-include maps against a fixed left component form a cocone over the right degree.

Equations

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

noncomputable def RS.chainBGrMulStage {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a : ℤ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBGrComponent A M M' d a) (chainBGr A M M' d) ⟶ chainBGr A M M' d

The left-component stage of the graded multiplication: a fixed component multiplies the whole carrier degreewise.

Equations

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

theorem RS.whiskerLeft_ι_chainBGrMulStage {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainBGrComponent A M M' d a) (chainBGrι A M M' d b)) (chainBGrMulStage A M M' d a) = CategoryTheory.CategoryStruct.comp (chainBGrCompMul A M M' d a b) (chainBGrι A M M' d (a + b))

On a right component, the stage multiplication is the pairwise product followed by the sum-degree inclusion.

theorem RS.whiskerLeft_ι_chainBGrMulStage_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)] [∀ (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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b : ℤ) {Z : D} (h : chainBGr A M M' d ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainBGrComponent A M M' d a) (chainBGrι A M M' d b)) (CategoryTheory.CategoryStruct.comp (chainBGrMulStage A M M' d a) h) = CategoryTheory.CategoryStruct.comp (chainBGrCompMul A M M' d a b) (CategoryTheory.CategoryStruct.comp (chainBGrι A M M' d (a + b)) h)

On a right component, the stage multiplication is the pairwise product followed by the sum-degree inclusion.

noncomputable def RS.chainBGrMulCocone {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.Limits.Cocone ((CategoryTheory.Discrete.functor fun (a : ℤ) => chainBGrComponent A M M' d a).comp (CategoryTheory.MonoidalCategory.tensorRight (chainBGr A M M' d)))

The stage multiplications form a cocone over the left degree.

Equations

• RS.chainBGrMulCocone A M M' d = { pt := RS.chainBGr A M M' d, ι := CategoryTheory.Discrete.natTrans fun (a : CategoryTheory.Discrete ℤ) => RS.chainBGrMulStage A M M' d a.as }

noncomputable def RS.chainBGrMul {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBGr A M M' d) (chainBGr A M M' d) ⟶ chainBGr A M M' d

The multiplication of the graded splitting algebra: the pairwise graded products assembled over both degrees.

Equations

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

theorem RS.ι_whiskerRight_chainBGrMul {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBGrι A M M' d a) (chainBGr A M M' d)) (chainBGrMul A M M' d) = chainBGrMulStage A M M' d a

On a left component, the multiplication is the stage multiplication.

theorem RS.ι_whiskerRight_chainBGrMul_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)] [∀ (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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a : ℤ) {Z : D} (h : chainBGr A M M' d ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBGrι A M M' d a) (chainBGr A M M' d)) (CategoryTheory.CategoryStruct.comp (chainBGrMul A M M' d) h) = CategoryTheory.CategoryStruct.comp (chainBGrMulStage A M M' d a) h

On a left component, the multiplication is the stage multiplication.

theorem RS.ι_tensorHom_chainBGrMul {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrι A M M' d a) (chainBGrι A M M' d b)) (chainBGrMul A M M' d) = CategoryTheory.CategoryStruct.comp (chainBGrCompMul A M M' d a b) (chainBGrι A M M' d (a + b))

Defining equation of the graded multiplication: on a pair of components it is the pairwise product followed by the sum-degree inclusion.

theorem RS.ι_tensorHom_chainBGrMul_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)] [∀ (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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b : ℤ) {Z : D} (h : chainBGr A M M' d ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrι A M M' d a) (chainBGrι A M M' d b)) (CategoryTheory.CategoryStruct.comp (chainBGrMul A M M' d) h) = CategoryTheory.CategoryStruct.comp (chainBGrCompMul A M M' d a b) (CategoryTheory.CategoryStruct.comp (chainBGrι A M M' d (a + b)) h)

Defining equation of the graded multiplication: on a pair of components it is the pairwise product followed by the sum-degree inclusion.

theorem RS.chainBdegι_chainBdegZeroIso_hom {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] (d : ModDualityDatum A M M') (k : ℕ) : CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d 0 0 k) (chainBdegZeroIso A M M' d).hom = CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainColimitι (chainStage A M M') (chainDelta A M M' d) k)

Under the degree-zero identification, the stage insertions of the balanced line are the stage transports followed by the stage inclusions of the splitting-chain algebra.

theorem RS.chainBdegι_chainBdegZeroIso_hom_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)] [∀ (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] (d : ModDualityDatum A M M') (k : ℕ) {Z : D} (h : chainB A M M' d ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d 0 0 k) (CategoryTheory.CategoryStruct.comp (chainBdegZeroIso A M M' d).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainColimitι (chainStage A M M') (chainDelta A M M' d) k)) h

Under the degree-zero identification, the stage insertions of the balanced line are the stage transports followed by the stage inclusions of the splitting-chain algebra.

theorem RS.chainBdegShiftIso_hom_cast {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] (d : ModDualityDatum A M M') {p₀ q₀ p₀' q₀' n n' : ℕ} (hp : p₀ = p₀') (hq : q₀ = q₀') (hn : n = n') : CategoryTheory.CategoryStruct.comp (chainBdegCast A M M' d ⋯ ⋯) (chainBdegShiftIso A M M' d p₀' q₀' n').hom = CategoryTheory.CategoryStruct.comp (chainBdegShiftIso A M M' d p₀ q₀ n).hom (chainBdegCast A M M' d hp hq)

The iterated shift commutes with the offset transports.

theorem RS.chainBGrComponent_eqToHom_cast {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] (d : ModDualityDatum A M M') {x y : ℤ} (h : x = y) : CategoryTheory.eqToHom ⋯ = chainBdegCast A M M' d ⋯ ⋯

Degree transports on a component are offset transports.

theorem RS.chainBdeg_eqToHom_cast {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] (d : ModDualityDatum A M M') {p₀ q₀ p₀' q₀' : ℕ} (hp : p₀ = p₀') (hq : q₀ = q₀') : CategoryTheory.eqToHom ⋯ = chainBdegCast A M M' d hp hq

Line transports along paired offset equalities are offset transports.

theorem RS.chainBGrCompNormIso_hom_eq {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] (d : ModDualityDatum A M M') (a b : ℤ) : (chainBGrCompNormIso A M M' d a b).hom = CategoryTheory.CategoryStruct.comp (chainBdegCast A M M' d ⋯ ⋯) (chainBdegShiftIso A M M' d (-(a + b)).toNat (a + b).toNat (a.toNat + b.toNat - (a + b).toNat)).hom

The normaliser decomposes as an offset transport followed by the iterated shift.

theorem RS.chainBGrCompNormIso_comm {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] (d : ModDualityDatum A M M') (a b : ℤ) : CategoryTheory.CategoryStruct.comp (chainBGrCompNormIso A M M' d b a).hom (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (chainBdegCast A M M' d ⋯ ⋯) (chainBGrCompNormIso A M M' d a b).hom

The offset normalisation is braiding-compatible: the normaliser of the swapped degrees followed by the sum-degree transport is the offset transport followed by the normaliser.

theorem RS.chainBGrCompMul_comm {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b : ℤ) : CategoryTheory.CategoryStruct.comp (β_ (chainBGrComponent A M M' d a) (chainBGrComponent A M M' d b)).hom (CategoryTheory.CategoryStruct.comp (chainBGrCompMul A M M' d b a) (CategoryTheory.eqToHom ⋯)) = chainBGrCompMul A M M' d a b

Commutativity of the pairwise graded product: the braiding followed by the swapped product is the product, up to the sum-degree transport.

theorem RS.eqToHom_chainBGrι {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') {x y : ℤ} (h : x = y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (chainBGrι A M M' d y) = chainBGrι A M M' d x

Degree transports are absorbed by the inclusions.

theorem RS.chainBGr_tensorRight_hom_ext {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 (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') {X Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBGr A M M' d) X ⟶ Z} (w : ∀ (a : ℤ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBGrι A M M' d a) X) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBGrι A M M' d a) X) g) : f = g

Maps out of the carrier tensored on the right are determined by their restrictions to the components.

theorem RS.tensorLeft_chainBGr_hom_ext {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 (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') {X Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (chainBGr A M M' d) ⟶ Z} (w : ∀ (b : ℤ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (chainBGrι A M M' d b)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (chainBGrι A M M' d b)) g) : f = g

Maps out of the carrier tensored on the left are determined by their restrictions to the components.

theorem RS.chainBGr_pair_hom_ext {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 (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBGr A M M' d) (chainBGr A M M' d) ⟶ Z} (w : ∀ (a b : ℤ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrι A M M' d a) (chainBGrι A M M' d b)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrι A M M' d a) (chainBGrι A M M' d b)) g) : f = g

Maps out of a tensor square of the carrier agree once they agree on all pairs of components.

theorem RS.chainBGrMul_comm {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (β_ (chainBGr A M M' d) (chainBGr A M M' d)).hom (chainBGrMul A M M' d) = chainBGrMul A M M' d

The graded multiplication is commutative: the braiding followed by the multiplication is the multiplication.

The stage-level seed law on the left

theorem RS.chainSeed_mul2_left {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) (d : ModDualityDatum A M M') (p q : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainSeed A M M' d) (chainStage2 A M M' p q)) (chainMul2 A M M' 0 0 p q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (chainStage2 A M M' p q)).hom (CategoryTheory.CategoryStruct.comp (chainDelta2 A M M' d p q) (chainStage2Cast A M M' ⋯ ⋯))

The left unit law of the seed at two indices: multiplying by the seed on the left is the transition, through the unit braiding.

Stage computation of the shift and the normalisation

theorem RS.chainBdegShiftIso_succ {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] (d : ModDualityDatum A M M') (p₀ q₀ n : ℕ) : chainBdegShiftIso A M M' d p₀ q₀ (n + 1) = chainBdegSuccIso A M M' d (p₀ + n) (q₀ + n) ≪≫ chainBdegShiftIso A M M' d p₀ q₀ n

The iterated shift peels off one raise at a time.

theorem RS.chainBdegι_chainBdegSuccIso_hom {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] (d : ModDualityDatum A M M') (p₀ q₀ k : ℕ) : CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d (p₀ + 1) (q₀ + 1) k) (chainBdegSuccIso A M M' d p₀ q₀).hom = CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainBdegι A M M' d p₀ q₀ (k + 1))

Under the tail identification, the stage insertions of the raised line are the stage transports followed by the next stage insertions of the line.

theorem RS.chainBdegι_chainBdegSuccIso_hom_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)] [∀ (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] (d : ModDualityDatum A M M') (p₀ q₀ k : ℕ) {Z : D} (h : chainBdeg A M M' d p₀ q₀ ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d (p₀ + 1) (q₀ + 1) k) (CategoryTheory.CategoryStruct.comp (chainBdegSuccIso A M M' d p₀ q₀).hom h) = CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d p₀ q₀ (k + 1)) h)

Under the tail identification, the stage insertions of the raised line are the stage transports followed by the next stage insertions of the line.

theorem RS.chainBdegι_chainBdegShiftIso_hom {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] (d : ModDualityDatum A M M') (p₀ q₀ n k : ℕ) : CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d (p₀ + n) (q₀ + n) k) (chainBdegShiftIso A M M' d p₀ q₀ n).hom = CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainBdegι A M M' d p₀ q₀ (k + n))

Under the iterated shift, the stage insertions of the raised line are the stage transports followed by the shifted stage insertions of the line.

theorem RS.chainBdegι_chainBGrCompNormIso_hom {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] (d : ModDualityDatum A M M') (a b : ℤ) (k : ℕ) : CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d ((-a).toNat + (-b).toNat) (a.toNat + b.toNat) k) (chainBGrCompNormIso A M M' d a b).hom = CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainBdegι A M M' d (-(a + b)).toNat (a + b).toNat (k + (a.toNat + b.toNat - (a + b).toNat)))

Under the offset normalisation, the stage insertions of the summed line are the stage transports followed by the shifted stage insertions of the sum-degree component.

theorem RS.chainBdegι_chainBGrCompNormIso_hom_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)] [∀ (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] (d : ModDualityDatum A M M') (a b : ℤ) (k : ℕ) {Z : D} (h : chainBGrComponent A M M' d (a + b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d ((-a).toNat + (-b).toNat) (a.toNat + b.toNat) k) (CategoryTheory.CategoryStruct.comp (chainBGrCompNormIso A M M' d a b).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainBdegι A M M' d (-(a + b)).toNat (a + b).toNat (k + (a.toNat + b.toNat - (a + b).toNat)))) h

Under the offset normalisation, the stage insertions of the summed line are the stage transports followed by the shifted stage insertions of the sum-degree component.

Tensor surgery

Component insertions

noncomputable def RS.chainBGrCompι {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] (d : ModDualityDatum A M M') (a : ℤ) (k : ℕ) : chainStage2 A M M' ((-a).toNat + k) (a.toNat + k) ⟶ chainBGrComponent A M M' d a

The stage insertion of a graded component.

Equations

• RS.chainBGrCompι A M M' d a k = RS.chainBdegι A M M' d (-a).toNat a.toNat k

theorem RS.chainStage2Cast_chainBGrCompι {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] (d : ModDualityDatum A M M') (x : ℤ) {a b : ℕ} (h : a = b) : CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainBGrCompι A M M' d x b) = chainBGrCompι A M M' d x a

Stage transports along a stage equality are absorbed by the component insertions.

theorem RS.chainDelta2_chainBGrCompι {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] (d : ModDualityDatum A M M') (x : ℤ) (k : ℕ) : CategoryTheory.CategoryStruct.comp (chainDelta2 A M M' d ((-x).toNat + k) (x.toNat + k)) (chainBGrCompι A M M' d x (k + 1)) = chainBGrCompι A M M' d x k

The component insertions absorb the transitions.

theorem RS.chainBGrCompι_eqToHom {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] (d : ModDualityDatum A M M') {x y : ℤ} (h : x = y) (k : ℕ) : CategoryTheory.CategoryStruct.comp (chainBGrCompι A M M' d x k) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainBGrCompι A M M' d y k)

Degree transports intertwine the component insertions with the stage transports.

Stage computation and associativity of the pairwise

product

theorem RS.tensorLeft_chainBGrComp_hom_ext {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (b : ℤ) {X Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (chainBGrComponent A M M' d b) ⟶ Z} (w : ∀ (j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (chainBGrCompι A M M' d b j)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (chainBGrCompι A M M' d b j)) g) : f = g

Maps out of a component tensored on the left are determined by the stages.

theorem RS.chainBGrComp_triple_hom_ext {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b c : ℤ) {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBGrComponent A M M' d a) (chainBGrComponent A M M' d b)) (chainBGrComponent A M M' d c) ⟶ Z} (w : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrCompι A M M' d a i) (chainBGrCompι A M M' d b j)) (chainBGrCompι A M M' d c k)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrCompι A M M' d a i) (chainBGrCompι A M M' d b j)) (chainBGrCompι A M M' d c k)) g) : f = g

Maps out of a triple tensor of components agree once they agree on all triples of stages.

theorem RS.ι_tensorHom_chainBGrCompMul {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b : ℤ) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrCompι A M M' d a i) (chainBGrCompι A M M' d b j)) (chainBGrCompMul A M M' d a b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (chainMul2 A M M' ((-a).toNat + i) (a.toNat + i) ((-b).toNat + j) (b.toNat + j)) (chainStage2Cast A M M' ⋯ ⋯)) (chainBGrCompι A M M' d (a + b) (i + 1 + j + (a.toNat + b.toNat - (a + b).toNat)))

Defining equation of the pairwise graded product on stages: the two-index stage multiplication, transported and inserted at the shifted stage of the sum-degree component.

theorem RS.ι_tensorHom_chainBGrCompMul_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)] [∀ (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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b : ℤ) (i j : ℕ) {Z : D} (h : chainBGrComponent A M M' d (a + b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrCompι A M M' d a i) (chainBGrCompι A M M' d b j)) (CategoryTheory.CategoryStruct.comp (chainBGrCompMul A M M' d a b) h) = CategoryTheory.CategoryStruct.comp (chainMul2 A M M' ((-a).toNat + i) (a.toNat + i) ((-b).toNat + j) (b.toNat + j)) (CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (chainBGrCompι A M M' d (a + b) (i + 1 + j + (a.toNat + b.toNat - (a + b).toNat))) h))

Defining equation of the pairwise graded product on stages: the two-index stage multiplication, transported and inserted at the shifted stage of the sum-degree component.

theorem RS.chainBGrCompMul_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)] [∀ (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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (a b c : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBGrCompMul A M M' d a b) (chainBGrComponent A M M' d c)) (chainBGrCompMul A M M' d (a + b) c) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (chainBGrComponent A M M' d a) (chainBGrComponent A M M' d b) (chainBGrComponent A M M' d c)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainBGrComponent A M M' d a) (chainBGrCompMul A M M' d b c)) (CategoryTheory.CategoryStruct.comp (chainBGrCompMul A M M' d a (b + c)) (CategoryTheory.eqToHom ⋯)))

Associativity of the pairwise graded product: the two bracketings of a triple product agree up to the sum-degree transport reassociating the degrees.

Associativity of the graded multiplication

theorem RS.chainBGr_sandwich_hom_ext {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 (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (X Y : D) {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBGr A M M' d) Y) ⟶ Z} (w : ∀ (b : ℤ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBGrι A M M' d b) Y)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBGrι A M M' d b) Y)) g) : f = g

Sandwich extensionality: maps out of a tensor product with the carrier in the middle slot are determined by the components there.

theorem RS.chainBGr_pair_whiskerRight_hom_ext {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 (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') {X Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBGr A M M' d) (chainBGr A M M' d)) X ⟶ Z} (w : ∀ (a b : ℤ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrι A M M' d a) (chainBGrι A M M' d b)) X) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrι A M M' d a) (chainBGrι A M M' d b)) X) g) : f = g

Maps out of a tensor square of the carrier whiskered on the right agree once they agree on all pairs of components.

theorem RS.chainBGr_triple_hom_ext {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 (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBGr A M M' d) (chainBGr A M M' d)) (chainBGr A M M' d) ⟶ Z} (w : ∀ (a b c : ℤ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrι A M M' d a) (chainBGrι A M M' d b)) (chainBGrι A M M' d c)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrι A M M' d a) (chainBGrι A M M' d b)) (chainBGrι A M M' d c)) g) : f = g

Maps out of a triple tensor of the carrier agree once they agree on all triples of components.

theorem RS.chainBGrMul_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)] [∀ (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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBGrMul A M M' d) (chainBGr A M M' d)) (chainBGrMul A M M' d) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (chainBGr A M M' d) (chainBGr A M M' d) (chainBGr A M M' d)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainBGr A M M' d) (chainBGrMul A M M' d)) (chainBGrMul A M M' d))

Associativity of the graded multiplication: the two bracketings of a triple product agree.

The unit laws

theorem RS.chainBUnit_chainBGrComponentZeroIso_inv {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] (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (chainBUnit A M M' d) (chainBGrComponentZeroIso A M M' d).inv = CategoryTheory.CategoryStruct.comp (chainSeed A M M' d) (chainBGrCompι A M M' d 0 0)

The unit lands at the bottom stage: through the degree-zero identification, the unit of the balanced algebra is the seed at the bottom stage of the degree-zero component.

theorem RS.ι_tensorHom_chainBGrCompMul_zero_left {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (b : ℤ) (j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBGrCompι A M M' d 0 0) (chainBGrCompι A M M' d b j)) (chainBGrCompMul A M M' d 0 b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (chainMul2 A M M' 0 0 ((-b).toNat + j) (b.toNat + j)) (chainStage2Cast A M M' ⋯ ⋯)) (chainBGrCompι A M M' d (0 + b) (0 + 1 + j + (Int.toNat 0 + b.toNat - (0 + b).toNat)))

The stage rule of the pairwise product at degree zero on the left, with the balanced-line arities normalised.

theorem RS.chainBGrCompMul_unit_left {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (b : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (chainBUnit A M M' d) (chainBGrComponentZeroIso A M M' d).inv) (chainBGrComponent A M M' d b)) (CategoryTheory.CategoryStruct.comp (chainBGrCompMul A M M' d 0 b) (CategoryTheory.eqToHom ⋯)) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (chainBGrComponent A M M' d b)).hom

The left unit law of the pairwise graded product: the included unit against a component multiplies as the left unitor, through the sum-degree transport.

theorem RS.chainBGrCompMul_unit_left_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)] [∀ (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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') (b : ℤ) {Z : D} (h : chainBGrComponent A M M' d b ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (chainBUnit A M M' d) (chainBGrComponentZeroIso A M M' d).inv) (chainBGrComponent A M M' d b)) (CategoryTheory.CategoryStruct.comp (chainBGrCompMul A M M' d 0 b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (chainBGrComponent A M M' d b)).hom h

The left unit law of the pairwise graded product: the included unit against a component multiplies as the left unitor, through the sum-degree transport.

theorem RS.chainBGrUnit_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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBGrUnit A M M' d) (chainBGr A M M' d)) (chainBGrMul A M M' d) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (chainBGr A M M' d)).hom

The left unit law of the graded splitting algebra: the unit against the carrier is the left unitor.

theorem RS.chainBGrMul_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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainBGr A M M' d) (chainBGrUnit A M M' d)) (chainBGrMul A M M' d) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (chainBGr A M M' d)).hom

The right unit law of the graded splitting algebra: the carrier against the unit is the right unitor.

The monoid object

@[reducible]

noncomputable def RS.chainBGrMonObj {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.MonObj (chainBGr A M M' d)

The graded splitting algebra is a monoid object: the degree-zero unit and the graded multiplication satisfy the monoid laws.

Equations

• RS.chainBGrMonObj A M M' d = { one := RS.chainBGrUnit A M M' d, mul := RS.chainBGrMul A M M' d, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }

theorem RS.chainBGr_isCommMonObj {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] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ℤ) D] [∀ (X : D), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ℤ) (CategoryTheory.MonoidalCategory.tensorLeft X)] (d : ModDualityDatum A M M') : CategoryTheory.IsCommMonObj (chainBGr A M M' d)

The graded splitting algebra is commutative.