The first-slot insertion against the stage structure

The insertion of a letter into the first slot of a two-index chain stage, defined in Base.lean, meets the two structure maps of the chain: the stage multiplication and the seed transition.

• chainInsP_mul: inserting a letter into a merged stage is inserting into the first factor and multiplying, up to the index transport.
• chainInsP_delta2: the insertion passes the seed transition, raising the merged arities by one on each side.

An insertion past the interchange

The insertion against the stage multiplication

theorem RS.tensorHom_whiskerRight_absorb {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] {X₁ X₂ Y₁ Y₂ Z₁ W : D} (a : X₁ ⟶ Y₁) (b : X₂ ⟶ Y₂) (f : Y₁ ⟶ Z₁) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Y₂ ⟶ W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom a b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp a f) b) h

Absorb a whiskered morphism into the first tensor factor.

theorem RS.chainInsP_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)) (chainInsP 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 (chainInsP A M M' p q) (chainStage2 A M M' r s)) (CategoryTheory.CategoryStruct.comp (chainMul2 A M M' (p + 1) q r s) (chainStage2Cast A M M' ⋯ ⋯)))

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

theorem RS.chainInsP_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)) (chainInsP A M M' (p + 1) (q + 1)) = CategoryTheory.CategoryStruct.comp (chainInsP A M M' p q) (chainDelta2 A M M' d (p + 1) q)

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