The second-slot insertion against the stage structure

The mirror of FirstSlot.lean for the insertion into the second slot of a two-index chain stage: the letter is carried past the first slot by the braiding, so the crossings the proofs need are established first.

• chainInsQ_mul: inserting a letter into a merged stage is inserting into the first factor's second slot and multiplying, up to the index transport.
• chainInsQ_delta2: the insertion passes the seed transition, raising the merged arities by one on each side.

Braided crossings for the second-slot insertion

theorem RS.chainInsQ_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) (p q r s : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X (chainMul2 A M M' p q r s)) (chainInsQ A M M' (p + 1 + r) (q + 1 + s)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X (chainStage2 A M M' p q) (chainStage2 A M M' r s)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (chainInsQ A M M' p q) (chainStage2 A M M' r s)) (CategoryTheory.CategoryStruct.comp (chainMul2 A M M' p (q + 1) r s) (chainStage2Cast A M M' ⋯ ⋯)))

The second-slot insertion passes the stage multiplication: inserting a letter into the merged stage is inserting into the first factor's second slot and multiplying, up to the index transport.

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

The transition square for the second-slot insertion: the insertion passes the seed transition, raising the merged arities by one on each side.