The shifted splitting chains

The off-diagonal lines of the two-index stage lattice: for a starting bidegree the chain climbs both arities in step, and its colimit is the corresponding graded component of the splitting algebra. The balanced line recovers the degree-zero algebra carrier.

noncomputable def RS.chainBdeg {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₀ : ℕ) : D

The shifted graded component: the colimit of the two-index stages along the line through the starting bidegree, climbing both arities by the seed transition.

Equations

• RS.chainBdeg A M M' d p₀ q₀ = RS.chainColimit (fun (k : ℕ) => RS.chainStage2 A M M' (p₀ + k) (q₀ + k)) fun (k : ℕ) => RS.chainDelta2 A M M' d (p₀ + k) (q₀ + k)

noncomputable def RS.chainBdegι {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 : ℕ) : chainStage2 A M M' (p₀ + k) (q₀ + k) ⟶ chainBdeg A M M' d p₀ q₀

The stage insertion of a shifted graded component.

Equations

• RS.chainBdegι A M M' d p₀ q₀ k = RS.chainColimitι (fun (k : ℕ) => RS.chainStage2 A M M' (p₀ + k) (q₀ + k)) (fun (k : ℕ) => RS.chainDelta2 A M M' d (p₀ + k) (q₀ + k)) k

theorem RS.chainDelta2_chainBdegι {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 (chainDelta2 A M M' d (p₀ + k) (q₀ + k)) (chainBdegι A M M' d p₀ q₀ (k + 1)) = chainBdegι A M M' d p₀ q₀ k

The stage insertions commute with the transitions.

theorem RS.chainCast_line {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (p₀ q₀ : ℕ) {a b : ℕ} (h : a = b) : chainCast (fun (k : ℕ) => chainStage2 A M M' (p₀ + k) (q₀ + k)) h = chainStage2Cast A M M' ⋯ ⋯

The family cast of a line agrees with the two-index stage transport.

noncomputable def RS.chainBdegMulStage {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) (p₀ q₀ r₀ s₀ i j : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainStage2 A M M' (p₀ + i) (q₀ + i)) (chainStage2 A M M' (r₀ + j) (s₀ + j)) ⟶ chainStage2 A M M' (p₀ + r₀ + (i + 1 + j)) (q₀ + s₀ + (i + 1 + j))

The stagewise multiplication of two lines: the two-index stage multiplication, transported onto the sum line.

Equations

• RS.chainBdegMulStage A M M' p₀ q₀ r₀ s₀ i j = CategoryTheory.CategoryStruct.comp (RS.chainMul2 A M M' (p₀ + i) (q₀ + i) (r₀ + j) (s₀ + j)) (RS.chainStage2Cast A M M' ⋯ ⋯)

theorem RS.chainBdegMulStage_delta_right {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₀ r₀ s₀ i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainStage2 A M M' (p₀ + i) (q₀ + i)) (chainDelta2 A M M' d (r₀ + j) (s₀ + j))) (chainBdegMulStage A M M' p₀ q₀ r₀ s₀ i (j + 1)) = CategoryTheory.CategoryStruct.comp (chainBdegMulStage A M M' p₀ q₀ r₀ s₀ i j) (chainDelta2 A M M' d (p₀ + r₀ + (i + 1 + j)) (q₀ + s₀ + (i + 1 + j)))

The right transition square of the line multiplication.

theorem RS.chainBdegMulStage_delta_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₀ r₀ s₀ i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainDelta2 A M M' d (p₀ + i) (q₀ + i)) (chainStage2 A M M' (r₀ + j) (s₀ + j))) (chainBdegMulStage A M M' p₀ q₀ r₀ s₀ (i + 1) j) = CategoryTheory.CategoryStruct.comp (chainBdegMulStage A M M' p₀ q₀ r₀ s₀ i j) (CategoryTheory.CategoryStruct.comp (chainDelta2 A M M' d (p₀ + r₀ + (i + 1 + j)) (q₀ + s₀ + (i + 1 + j))) (chainStage2Cast A M M' ⋯ ⋯))

The left transition square of the line multiplication.

noncomputable def RS.chainBdegZeroStageIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (k : ℕ) : chainStage2 A M M' (0 + k) (0 + k) ≅ chainStage A M M' k

The stage identification of the balanced line.

Equations

• RS.chainBdegZeroStageIso A M M' k = { hom := RS.chainStage2Cast A M M' ⋯ ⋯, inv := RS.chainStage2Cast A M M' ⋯ ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.chainBdegZeroIso {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') : chainBdeg A M M' d 0 0 ≅ chainB A M M' d

The balanced line is the degree-zero algebra carrier: the zero-offset line's colimit is the splitting-chain algebra.

Equations

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

noncomputable def RS.chainBdegSuccStageIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (p₀ q₀ k : ℕ) : chainStage2 A M M' (p₀ + 1 + k) (q₀ + 1 + k) ≅ chainStage2 A M M' (p₀ + (k + 1)) (q₀ + (k + 1))

The stages of the raised line are the shifted stages of the line.

Equations

• RS.chainBdegSuccStageIso A M M' p₀ q₀ k = { hom := RS.chainStage2Cast A M M' ⋯ ⋯, inv := RS.chainStage2Cast A M M' ⋯ ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

The raised line is the line: shifting both offsets by one is passing to the tail of the chain, which has the same colimit.

Equations

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

noncomputable def RS.chainBdegMul {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') (p₀ q₀ r₀ s₀ : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBdeg A M M' d p₀ q₀) (chainBdeg A M M' d r₀ s₀) ⟶ chainBdeg A M M' d (p₀ + r₀) (q₀ + s₀)

The graded multiplication: two lines multiply into the sum line at the colimit level.

Equations

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

noncomputable def RS.chainBdegCast {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₀') : chainBdeg A M M' d p₀ q₀ ⟶ chainBdeg A M M' d p₀' q₀'

Transport of a graded component along offset equalities.

Equations

• RS.chainBdegCast A M M' d hp hq = CategoryTheory.eqToHom ⋯

@[simp]

theorem RS.chainBdegCast_rfl {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₀ : ℕ) : chainBdegCast A M M' d ⋯ ⋯ = CategoryTheory.CategoryStruct.id (chainBdeg A M M' d p₀ q₀)

The trivial offset transport is the identity.

@[simp]

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

Offset transports compose.

@[simp]

theorem RS.chainBdegCast_trans_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₀ p₀' q₀' p₀'' q₀'' : ℕ} (hp : p₀ = p₀') (hq : q₀ = q₀') (hp' : p₀' = p₀'') (hq' : q₀' = q₀'') {Z : D} (h : chainBdeg A M M' d p₀'' q₀'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainBdegCast A M M' d hp hq) (CategoryTheory.CategoryStruct.comp (chainBdegCast A M M' d hp' hq') h) = CategoryTheory.CategoryStruct.comp (chainBdegCast A M M' d ⋯ ⋯) h

Offset transports compose.

theorem RS.ι_tensorHom_chainBdegMul {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') (p₀ q₀ r₀ s₀ i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBdegι A M M' d p₀ q₀ i) (chainBdegι A M M' d r₀ s₀ j)) (chainBdegMul A M M' d p₀ q₀ r₀ s₀) = CategoryTheory.CategoryStruct.comp (chainBdegMulStage A M M' p₀ q₀ r₀ s₀ i j) (chainBdegι A M M' d (p₀ + r₀) (q₀ + s₀) (i + 1 + j))

On stages, the graded multiplication is the stagewise line multiplication.

theorem RS.ι_tensorHom_chainBdegMul_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') (p₀ q₀ r₀ s₀ i j : ℕ) {Z : D} (h : chainBdeg A M M' d (p₀ + r₀) (q₀ + s₀) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBdegι A M M' d p₀ q₀ i) (chainBdegι A M M' d r₀ s₀ j)) (CategoryTheory.CategoryStruct.comp (chainBdegMul A M M' d p₀ q₀ r₀ s₀) h) = CategoryTheory.CategoryStruct.comp (chainBdegMulStage A M M' p₀ q₀ r₀ s₀ i j) (CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d (p₀ + r₀) (q₀ + s₀) (i + 1 + j)) h)

On stages, the graded multiplication is the stagewise line multiplication.

noncomputable def RS.chainBdegInsPStage {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalLinear ℂ D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (p₀ q₀ k : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X (chainStage2 A M M' (p₀ + k) (q₀ + k)) ⟶ chainStage2 A M M' (p₀ + 1 + k) (q₀ + k)

The stage insertion transported onto the line.

Equations

• RS.chainBdegInsPStage A M M' p₀ q₀ k = CategoryTheory.CategoryStruct.comp (RS.chainInsP A M M' (p₀ + k) (q₀ + k)) (RS.chainStage2Cast A M M' ⋯ ⋯)

theorem RS.chainBdegInsPStage_delta {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₀ k : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (chainDelta2 A M M' d (p₀ + k) (q₀ + k))) (chainBdegInsPStage A M M' p₀ q₀ (k + 1)) = CategoryTheory.CategoryStruct.comp (chainBdegInsPStage A M M' p₀ q₀ k) (chainDelta2 A M M' d (p₀ + 1 + k) (q₀ + k))

The line insertion commutes with the transitions.

theorem RS.lineIns_chainMap_ι {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₀ : ℕ) {a b : ℕ} (h : a ≤ b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (chainMap (fun (k : ℕ) => chainStage2 A M M' (p₀ + k) (q₀ + k)) (fun (k : ℕ) => chainDelta2 A M M' d (p₀ + k) (q₀ + k)) h)) (CategoryTheory.CategoryStruct.comp (chainBdegInsPStage A M M' p₀ q₀ b) (chainBdegι A M M' d (p₀ + 1) q₀ b)) = CategoryTheory.CategoryStruct.comp (chainBdegInsPStage A M M' p₀ q₀ a) (chainBdegι A M M' d (p₀ + 1) q₀ a)

The line insertion absorbs the chain maps under the inclusions.

noncomputable def RS.chainBdegInsPCocone {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₀ : ℕ) : CategoryTheory.Limits.Cocone ((chainDiagram (fun (k : ℕ) => chainStage2 A M M' (p₀ + k) (q₀ + k)) fun (k : ℕ) => chainDelta2 A M M' d (p₀ + k) (q₀ + k)).comp (CategoryTheory.MonoidalCategory.tensorLeft M'.X))

The insertion cocone over the line diagram.

Equations

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

noncomputable def RS.chainBdegInsP {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') (p₀ q₀ : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj M'.X (chainBdeg A M M' d p₀ q₀) ⟶ chainBdeg A M M' d (p₀ + 1) q₀

The colimit-level line insertion.

Equations

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

theorem RS.whiskerLeft_ι_chainBdegInsP {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') (p₀ q₀ k : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (chainBdegι A M M' d p₀ q₀ k)) (chainBdegInsP A M M' d p₀ q₀) = CategoryTheory.CategoryStruct.comp (chainBdegInsPStage A M M' p₀ q₀ k) (chainBdegι A M M' d (p₀ + 1) q₀ k)

On a stage, the line insertion is insert-then-include.

theorem RS.whiskerLeft_ι_chainBdegInsP_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.tensorLeft X)] (d : ModDualityDatum A M M') (p₀ q₀ k : ℕ) {Z : D} (h : chainBdeg A M M' d (p₀ + 1) q₀ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (chainBdegι A M M' d p₀ q₀ k)) (CategoryTheory.CategoryStruct.comp (chainBdegInsP A M M' d p₀ q₀) h) = CategoryTheory.CategoryStruct.comp (chainBdegInsPStage A M M' p₀ q₀ k) (CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d (p₀ + 1) q₀ k) h)

On a stage, the line insertion is insert-then-include.