Paired left actions and the joint action

The zag companion of the paired right action relation: acting on both carriers on the left and projecting is multiplying the scalars and acting on the projected pair.

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

Pure braid coherence for the zag prefix: reassociating and braiding the block P ⊗ Q past P', then swapping P' back past P, agrees with interchanging via tensorμ and reassociating. The block braiding decomposes into the elementary crossings β_ Q P' and β_ P P'; the latter cancels against the final β_ P' P by the symmetry axiom, leaving exactly the single crossing carried by tensorμ.

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

Pure braid coherence for the zag prefix: reassociating and braiding the block P ⊗ Q past P', then swapping P' back past P, agrees with interchanging via tensorμ and reassociating. The block braiding decomposes into the elementary crossings β_ Q P' and β_ P P'; the latter cancels against the final β_ P' P by the symmetry axiom, leaving exactly the single crossing carried by tensorμ.

theorem RS.tensorHom_actLeft_π {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (N₁ N₂ : CategoryTheory.Mod D A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (actLeft A N₁.X) (actLeft A N₂.X)) (modTensorπ A N₁ N₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ A N₁.X A N₂.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (CategoryTheory.MonoidalCategoryStruct.tensorObj N₁.X N₂.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modTensorπ A N₁ N₂)) (modTensorAct A N₁ N₂)))

Paired left actions descend to the joint action: acting on both carriers on the left and projecting is multiplying the scalars and acting on the projected pair — the zag companion of the paired right action relation of the relative tensor.