A braid-coherence identity for the interchange prefix

Both sides of the identity proved here are words in associators and braidings realising the same permutation of the four strands (P, q₁, R, q₂) ↦ (q₁, q₂, P, R): the left-hand side crosses R past the second Q-strand and then P past both Q-strands, while the right-hand side crosses the first Q-strand past R (inside tensorμ) and then the block P ⊗ R past Q ⊗ Q. The surplus adjacent pair of crossings β_ Q R ≫ β_ R Q cancels by the symmetry axiom, and the residual pure-associator words close by coherence.

theorem RS.braid_prefix_coherence {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (P Q R : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q) (β_ R Q).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q) Q R).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator P Q Q).hom R) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ P (CategoryTheory.MonoidalCategoryStruct.tensorObj Q Q)).hom R))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ P Q R Q) (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj P R) (CategoryTheory.MonoidalCategoryStruct.tensorObj Q Q)).hom (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q Q) P R).inv)

Pure braid coherence for the interchange prefix: braiding the third strand past the fourth, reassociating, and braiding P past the two Q-strands as a block agrees with interchanging via tensorμ, braiding the block P ⊗ R past Q ⊗ Q, and reassociating.

theorem RS.braid_prefix_coherence_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] (P Q R : D) {Z : D} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Q Q) P) R ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q) (β_ R Q).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q) Q R).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator P Q Q).hom R) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ P (CategoryTheory.MonoidalCategoryStruct.tensorObj Q Q)).hom R) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ P Q R Q) (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj P R) (CategoryTheory.MonoidalCategoryStruct.tensorObj Q Q)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj Q Q) P R).inv h))

Pure braid coherence for the interchange prefix: braiding the third strand past the fourth, reassociating, and braiding P past the two Q-strands as a block agrees with interchanging via tensorμ, braiding the block P ⊗ R past Q ⊗ Q, and reassociating.