Insertion maps into the splitting-chain stages

Single-module insertions for the two-index splitting chain: the module inserts into a symmetric power from the left through the singleton power and the symmetric multiplication, and this insertion descends through the module-tensor coequalizer into either slot of a two-index chain stage. How the descended insertions meet the stage multiplication and the seed transition is the subject of FirstSlot.lean and SecondSlot.lean.

• symInsL: the insertion X ⊗ symPow A X (n + 1) ⟶ symPow A X (n + 2), the symmetric multiplication against the singleton power.
• symInsL_actAcross/symInsL_actRight: the insertion is compatible with the monoid action on the symmetric factor, in the carried-past left form and in the braided right form.
• chainInsP/chainInsQ: the descended insertions of the dual pair's modules into the first and second slots of a two-index stage, with defining equations whiskerLeft_π_chainInsP and whiskerLeft_π_chainInsQ.
• symInsL_symMul: the insertion is associative against the symmetric multiplication, up to the arity transport.

Insertion into a symmetric power

noncomputable def RS.symInsL {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] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj X (symPow A X (n + 1)) ⟶ symPow A X (n + 2)

Left insertion into a symmetric power: the module enters through the singleton power and multiplies.

Equations

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

theorem RS.symPowAct_symPowCast {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] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (X : D) [CategoryTheory.ModObj A X] {m n : ℕ} (h : m + 1 = n + 1) : CategoryTheory.CategoryStruct.comp (symPowAct A X m) (symPowCast A X h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (symPowCast A X h)) (symPowAct A X n)

The symmetric-power action passes an arity transport.

theorem RS.symInsL_actAcross {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] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : CategoryTheory.CategoryStruct.comp (braidPast A X (symPow A X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (symPowAct A X n)) (symInsL A X n)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (symInsL A X n)) (symPowAct A X (n + 1))

The insertion is compatible with the action on the symmetric factor, in carried-past form: the monoid crosses the inserted module and acts on the enlarged power.

theorem RS.symInsL_symPowAct {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] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (symPowAct A X n)) (symInsL A X n) = CategoryTheory.CategoryStruct.comp (braidPast A X (symPow A X (n + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (symInsL A X n)) (symPowAct A X (n + 1)))

The carried-past compatibility, solved for the action-first composite.

theorem RS.symInsL_actRight {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] (X : D) [CategoryTheory.ModObj A X] (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (actRight A (symPowMod A X n).X)) (symInsL A X n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X (symPow A X (n + 1)) A).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (symInsL A X n) A) (actRight A (symPowMod A X (n + 1)).X))

The insertion is compatible with the braided right action on the symmetric factor: the monoid leaves through the inserted module and acts on the right of the enlarged power.

Structural crossings for the descent conditions

Insertion into the first slot

theorem RS.chainInsP_cond {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 : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (modTensorLegM A (symPowMod A M'.X p) (symPowMod A M.X q))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X (symPow A M'.X (p + 1)) (symPow A M.X (q + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (symInsL A M'.X p) (symPow A M.X (q + 1))) (modTensorπ A (symPowMod A M'.X (p + 1)) (symPowMod A M.X q)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (modTensorLegN A (symPowMod A M'.X p) (symPowMod A M.X q))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X (symPow A M'.X (p + 1)) (symPow A M.X (q + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (symInsL A M'.X p) (symPow A M.X (q + 1))) (modTensorπ A (symPowMod A M'.X (p + 1)) (symPowMod A M.X q))))

The two module-tensor legs agree after the insertion of the dual module into the first slot: the leg acting on the second factor slides under the insertion, the leg acting on the first factor crosses it, and the level-(p + 1, q) coequalizer absorbs both.

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

Insertion into the first slot of a two-index stage: the dual module enters the first symmetric power, descended through the module-tensor coequalizer.

Equations

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

theorem RS.whiskerLeft_π_chainInsP {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 : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X q))) (chainInsP A M M' p q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X (symPow A M'.X (p + 1)) (symPow A M.X (q + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (symInsL A M'.X p) (symPow A M.X (q + 1))) (modTensorπ A (symPowMod A M'.X (p + 1)) (symPowMod A M.X q)))

Defining equation of the first-slot insertion.

theorem RS.whiskerLeft_π_chainInsP_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 : ℕ) {Z : D} (h : chainStage2 A M M' (p + 1) q ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M'.X (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X q))) (chainInsP A M M' p q)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M'.X (symPow A M'.X (p + 1)) (symPow A M.X (q + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (symInsL A M'.X p) (symPow A M.X (q + 1))) (modTensorπ A (symPowMod A M'.X (p + 1)) (symPowMod A M.X q)))) h

Defining equation of the first-slot insertion.

Insertion into the second slot

theorem RS.chainInsQ_cond {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 : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorLegM A (symPowMod A M'.X p) (symPowMod A M.X q))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X (symPow A M'.X (p + 1)) (symPow A M.X (q + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M.X (symPow A M'.X (p + 1))).hom (symPow A M.X (q + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (symPow A M'.X (p + 1)) M.X (symPow A M.X (q + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (symPow A M'.X (p + 1)) (symInsL A M.X q)) (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X (q + 1))))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorLegN A (symPowMod A M'.X p) (symPowMod A M.X q))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X (symPow A M'.X (p + 1)) (symPow A M.X (q + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M.X (symPow A M'.X (p + 1))).hom (symPow A M.X (q + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (symPow A M'.X (p + 1)) M.X (symPow A M.X (q + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (symPow A M'.X (p + 1)) (symInsL A M.X q)) (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X (q + 1)))))))

The two module-tensor legs agree after the insertion of the module into the second slot: the module is carried past the first symmetric power, the leg acting on the first factor slides under the carrying, the leg acting on the second factor crosses the insertion, and the level-(p, q + 1) coequalizer absorbs both.

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

Insertion into the second slot of a two-index stage: the module is carried past the first symmetric power and enters the second, descended through the module-tensor coequalizer.

Equations

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

theorem RS.whiskerLeft_π_chainInsQ {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 : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X q))) (chainInsQ A M M' p q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X (symPow A M'.X (p + 1)) (symPow A M.X (q + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M.X (symPow A M'.X (p + 1))).hom (symPow A M.X (q + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (symPow A M'.X (p + 1)) M.X (symPow A M.X (q + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (symPow A M'.X (p + 1)) (symInsL A M.X q)) (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X (q + 1))))))

Defining equation of the second-slot insertion.

theorem RS.whiskerLeft_π_chainInsQ_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 : ℕ) {Z : D} (h : chainStage2 A M M' p (q + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X q))) (chainInsQ A M M' p q)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X (symPow A M'.X (p + 1)) (symPow A M.X (q + 1))).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M.X (symPow A M'.X (p + 1))).hom (symPow A M.X (q + 1))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (symPow A M'.X (p + 1)) M.X (symPow A M.X (q + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (symPow A M'.X (p + 1)) (symInsL A M.X q)) (modTensorπ A (symPowMod A M'.X p) (symPowMod A M.X (q + 1))))))) h

Defining equation of the second-slot insertion.

The insertion against the multiplication

theorem RS.symPowCast_symPowCast {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [CategoryTheory.Linear ℂ D] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] {a b c : ℕ} (h : a = b) (h' : b = c) : CategoryTheory.CategoryStruct.comp (symPowCast A X h) (symPowCast A X h') = symPowCast A X ⋯

Arity transports compose.

theorem RS.symInsL_symMul {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] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (symInsL A X m) (symPow A X (n + 1))) (symMul A X (m + 2) (n + 1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X (symPow A X (m + 1)) (symPow A X (n + 1))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (symMul A X (m + 1) (n + 1))) (CategoryTheory.CategoryStruct.comp (symInsL A X (m + 1 + n)) (symPowCast A X ⋯)))

The insertion is associative against the multiplication: inserting and multiplying is multiplying and inserting into the product, up to the arity transport.