Laws of the graded line multiplication

Commutativity and associativity of the multiplication of shifted graded components: the braiding followed by the swapped multiplication is the multiplication, and the two bracketings of a triple product agree, in both cases up to the offset transports. Each law descends from the corresponding two-index stage law of ChainStage2 through pair and triple extensionality for tensored chain colimits, mirroring the homogeneous laws of ChainAlgebra.

Extensionality for tensors of distinct chain colimits

theorem RS.chainColimitHet_pair_hom_ext {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] {Z : E} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δB) (chainColimit C δC) ⟶ Z} (w : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δB i) (chainColimitι C δC j)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δB i) (chainColimitι C δC j)) g) : f = g

Maps out of a tensor of two chain colimits agree once they agree on all pairs of stages.

theorem RS.chainColimitHet_pair_whiskerRight_hom_ext {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] {X Z : E} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δB) (chainColimit C δC)) X ⟶ Z} (w : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δB i) (chainColimitι C δC j)) X) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δB i) (chainColimitι C δC j)) X) g) : f = g

Maps out of a tensor of two chain colimits whiskered on the right agree once they agree on all pairs of stages.

theorem RS.chainColimitHet_triple_hom_ext {E : Type u} [CategoryTheory.Category.{v, u} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.Limits.HasColimitsOfShape SmallNat E] (B C F : ℕ → E) (δB : (n : ℕ) → B n ⟶ B (n + 1)) (δC : (n : ℕ) → C n ⟶ C (n + 1)) (δF : (n : ℕ) → F n ⟶ F (n + 1)) [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorRight X)] [∀ (X : E), CategoryTheory.Limits.PreservesColimitsOfShape SmallNat (CategoryTheory.MonoidalCategory.tensorLeft X)] {Z : E} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (chainColimit B δB) (chainColimit C δC)) (chainColimit F δF) ⟶ Z} (w : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δB i) (chainColimitι C δC j)) (chainColimitι F δF k)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainColimitι B δB i) (chainColimitι C δC j)) (chainColimitι F δF k)) g) : f = g

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

The stage-level laws

theorem RS.chainStage2Cast_whiskerRight_chainMul2 {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 p' q' : ℕ} (hp : p = p') (hq : q = q') (e f : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainStage2Cast A M M' hp hq) (chainStage2 A M M' e f)) (chainMul2 A M M' p' q' e f) = CategoryTheory.CategoryStruct.comp (chainMul2 A M M' p q e f) (chainStage2Cast A M M' ⋯ ⋯)

Stage transports slide out of the first factor of the two-index multiplication.

theorem RS.whiskerLeft_chainStage2Cast_chainMul2 {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) (a b : ℕ) {p q p' q' : ℕ} (hp : p = p') (hq : q = q') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainStage2 A M M' a b) (chainStage2Cast A M M' hp hq)) (chainMul2 A M M' a b p' q') = CategoryTheory.CategoryStruct.comp (chainMul2 A M M' a b p q) (chainStage2Cast A M M' ⋯ ⋯)

Stage transports slide out of the second factor of the two-index multiplication.

theorem RS.chainBdegMulStage_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) (p₀ q₀ r₀ s₀ i j : ℕ) : CategoryTheory.CategoryStruct.comp (β_ (chainStage2 A M M' (p₀ + i) (q₀ + i)) (chainStage2 A M M' (r₀ + j) (s₀ + j))).hom (CategoryTheory.CategoryStruct.comp (chainBdegMulStage A M M' r₀ s₀ p₀ q₀ j i) (chainStage2Cast A M M' ⋯ ⋯)) = chainBdegMulStage A M M' p₀ q₀ r₀ s₀ i j

Commutativity of the stagewise line multiplication, up to the stage transport onto the common arities.

theorem RS.chainBdegMulStage_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) (p₀ q₀ r₀ s₀ t₀ u₀ i j k : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainBdegMulStage A M M' p₀ q₀ r₀ s₀ i j) (chainStage2 A M M' (t₀ + k) (u₀ + k))) (chainBdegMulStage A M M' (p₀ + r₀) (q₀ + s₀) t₀ u₀ (i + 1 + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (chainStage2 A M M' (p₀ + i) (q₀ + i)) (chainStage2 A M M' (r₀ + j) (s₀ + j)) (chainStage2 A M M' (t₀ + k) (u₀ + k))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainStage2 A M M' (p₀ + i) (q₀ + i)) (chainBdegMulStage A M M' r₀ s₀ t₀ u₀ j k)) (CategoryTheory.CategoryStruct.comp (chainBdegMulStage A M M' p₀ q₀ (r₀ + t₀) (s₀ + u₀) i (j + 1 + k)) (chainStage2Cast A M M' ⋯ ⋯)))

Associativity of the stagewise line multiplication, up to the stage transport reassociating the offsets.

Transport of the stage insertions

theorem RS.chainStage2Cast_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₀ : ℕ) {a b : ℕ} (h : a = b) : CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainBdegι A M M' d p₀ q₀ b) = chainBdegι A M M' d p₀ q₀ a

Stage transports along a stage-index equality are absorbed by the stage insertions of a line.

theorem RS.chainBdegι_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₀') (k : ℕ) : CategoryTheory.CategoryStruct.comp (chainBdegι A M M' d p₀ q₀ k) (chainBdegCast A M M' d hp hq) = CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) (chainBdegι A M M' d p₀' q₀' k)

The stage insertions intertwine the offset transports of a line with the stage transports.

The colimit-level laws

theorem RS.chainBdeg_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] [∀ (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₀ : ℕ) {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBdeg A M M' d p₀ q₀) (chainBdeg A M M' d r₀ s₀) ⟶ Z} (w : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBdegι A M M' d p₀ q₀ i) (chainBdegι A M M' d r₀ s₀ j)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBdegι A M M' d p₀ q₀ i) (chainBdegι A M M' d r₀ s₀ j)) g) : f = g

Maps out of a tensor of two graded components agree once they agree on all pairs of stages.

theorem RS.chainBdeg_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') (p₀ q₀ r₀ s₀ t₀ u₀ : ℕ) {Z : D} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (chainBdeg A M M' d p₀ q₀) (chainBdeg A M M' d r₀ s₀)) (chainBdeg A M M' d t₀ u₀) ⟶ Z} (w : ∀ (i j k : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBdegι A M M' d p₀ q₀ i) (chainBdegι A M M' d r₀ s₀ j)) (chainBdegι A M M' d t₀ u₀ k)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainBdegι A M M' d p₀ q₀ i) (chainBdegι A M M' d r₀ s₀ j)) (chainBdegι A M M' d t₀ u₀ k)) g) : f = g

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

theorem RS.chainBdegMul_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') (p₀ q₀ r₀ s₀ : ℕ) : CategoryTheory.CategoryStruct.comp (β_ (chainBdeg A M M' d p₀ q₀) (chainBdeg A M M' d r₀ s₀)).hom (CategoryTheory.CategoryStruct.comp (chainBdegMul A M M' d r₀ s₀ p₀ q₀) (chainBdegCast A M M' d ⋯ ⋯)) = chainBdegMul A M M' d p₀ q₀ r₀ s₀

Commutativity of the graded line multiplication: the braiding followed by the swapped multiplication is the multiplication, up to the offset transport.