The two-index splitting-chain stages

The unbalanced generalisation of the splitting chain: stages carry two independent symmetric-power arities, one for each slot of the dual pair. The balanced chain is the diagonal. The stage multiplication, its commutativity and associativity laws, and the seed transitions all restate the balanced machinery at two free indices; the substrate for the graded splitting algebra.

The two-index stages

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

A two-index stage of the splitting chain: the module tensor product of independently sized symmetric powers of the dual pair.

Equations

• RS.chainStage2 A M M' p q = RS.modTensor A (RS.symPowMod A M'.X p) (RS.symPowMod A M.X q)

@[simp]

theorem RS.chainStage2_diag {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' k k = chainStage A M M' k

The diagonal of the two-index stages is the balanced stage.

Stage transports

noncomputable def RS.chainStage2Cast {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 p' q' : ℕ} (hp : p = p') (hq : q = q') : chainStage2 A M M' p q ⟶ chainStage2 A M M' p' q'

Transport of a two-index stage along equalities of arities.

Equations

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

@[simp]

theorem RS.chainStage2Cast_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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) (p q : ℕ) : chainStage2Cast A M M' ⋯ ⋯ = CategoryTheory.CategoryStruct.id (chainStage2 A M M' p q)

The trivial transport is the identity.

@[simp]

theorem RS.chainStage2Cast_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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) {p q p' q' p'' q'' : ℕ} (hp : p = p') (hq : q = q') (hp' : p' = p'') (hq' : q' = q'') : CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' hp hq) (chainStage2Cast A M M' hp' hq') = chainStage2Cast A M M' ⋯ ⋯

Stage transports compose.

@[simp]

theorem RS.chainStage2Cast_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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) {p q p' q' p'' q'' : ℕ} (hp : p = p') (hq : q = q') (hp' : p' = p'') (hq' : q' = q'') {Z : D} (h : chainStage2 A M M' p'' q'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' hp hq) (CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' hp' hq') h) = CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ⋯ ⋯) h

Stage transports compose.

theorem RS.modTensorπ_chainStage2Cast {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 p' q' : ℕ} (hp : p = p') (hq : q = q') : CategoryTheory.CategoryStruct.comp (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X q)) (chainStage2Cast A M M' hp hq) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowCast A M'.X ⋯) (symPowCast A M.X ⋯)) (modTensorπ A (symPowMod A M'.X p') (symPowMod A M.X q'))

The stage projection intertwines the symmetric-power and two-index stage transports.

theorem RS.modTensorπ_chainStage2Cast_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)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (M M' : CategoryTheory.Mod D A) {p q p' q' : ℕ} (hp : p = p') (hq : q = q') {Z : D} (h : chainStage2 A M M' p' q' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X q)) (chainStage2Cast A M M' hp hq)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symPowCast A M'.X ⋯) (symPowCast A M.X ⋯)) (modTensorπ A (symPowMod A M'.X p') (symPowMod A M.X q'))) h

The stage projection intertwines the symmetric-power and two-index stage transports.

The two-index stage multiplication

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

The two-index chain multiplication: two stages interchange and multiply into the stage of the slotwise summed arities.

Equations

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

theorem RS.tensorHom_π_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 r s : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X q)) (modTensorπ A (symPowMod A M'.X r) (symPowMod A M.X s))) (chainMul2 A M M' p q r s) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (symPow A M'.X (p + 1)) (symPow A M.X (q + 1)) (symPow A M'.X (r + 1)) (symPow A M.X (s + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symMul A M'.X (p + 1) (r + 1)) (symMul A M.X (q + 1) (s + 1))) (modTensorπ A (symPowMod A M'.X (p + 1 + r)) (symPowMod A M.X (q + 1 + s))))

Defining equation of the two-index chain multiplication: under the stage projections it is the raw crossing followed by the slotwise symmetric multiplications.

Symmetric-power laws with transported arities

Commutativity of the two-index multiplication

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

Commutativity of the two-index chain multiplication, up to the slotwise stage transports.

Tensor surgery and the associativity core

Associativity of the two-index multiplication

theorem RS.chainMul2_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) (a b c d e f : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainMul2 A M M' a b c d) (chainStage2 A M M' e f)) (CategoryTheory.CategoryStruct.comp (chainMul2 A M M' (a + 1 + c) (b + 1 + d) e f) (chainStage2Cast A M M' ⋯ ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (chainStage2 A M M' a b) (chainStage2 A M M' c d) (chainStage2 A M M' e f)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainStage2 A M M' a b) (chainMul2 A M M' c d e f)) (CategoryTheory.CategoryStruct.comp (chainMul2 A M M' a b (c + 1 + e) (d + 1 + f)) (chainStage2Cast A M M' ⋯ ⋯)))

Associativity of the two-index chain multiplication, up to the slotwise stage transports onto the common arities.

The two-index transitions

noncomputable def RS.chainDelta2 {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 : ℕ) : chainStage2 A M M' p q ⟶ chainStage2 A M M' (p + 1) (q + 1)

The two-index chain transition: multiplication by the seed, which raises both arities by one.

Equations

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

theorem RS.chainSeed_mul2_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 : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainStage2 A M M' p q) (chainSeed A M M' d)) (chainMul2 A M M' p q 0 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (chainStage2 A M M' p q)).hom (chainDelta2 A M M' d p q)

The right unit law of the seed at two indices: multiplying by the seed on the right is the transition.

theorem RS.chainDelta2_mul_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') (i j k l : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (chainStage2 A M M' i j) (chainDelta2 A M M' d k l)) (chainMul2 A M M' i j (k + 1) (l + 1)) = CategoryTheory.CategoryStruct.comp (chainMul2 A M M' i j k l) (chainDelta2 A M M' d (i + 1 + k) (j + 1 + l))

The right transition square at two indices: inserting the seed in the second factor and multiplying is multiplying and then inserting the seed.

theorem RS.chainStage2Cast_delta2 {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') {a b a' b' : ℕ} (ha : a = a') (hb : b = b') : CategoryTheory.CategoryStruct.comp (chainStage2Cast A M M' ha hb) (chainDelta2 A M M' d a' b') = CategoryTheory.CategoryStruct.comp (chainDelta2 A M M' d a b) (chainStage2Cast A M M' ⋯ ⋯)

Transitions transport along index casts.

theorem RS.chainDelta2_mul_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') (i j k l : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainDelta2 A M M' d i j) (chainStage2 A M M' k l)) (chainMul2 A M M' (i + 1) (j + 1) k l) = CategoryTheory.CategoryStruct.comp (chainMul2 A M M' i j k l) (CategoryTheory.CategoryStruct.comp (chainDelta2 A M M' d (i + 1 + k) (j + 1 + l)) (chainStage2Cast A M M' ⋯ ⋯))

The left transition square at two indices: inserting the seed in the first factor and multiplying is multiplying and then inserting the seed, up to the index transports.