The cover factorisation of the twisted power identification

Over the plain tensor-power covers, the twisted power identification is the diagonal shuffle followed by the projection of the module factor. This reduces the conjugation of the permutation action through the identification to the committed plain equivariance.

theorem RS.modPowπ_one {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] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (modPowπ A X 1) (modPowOne A X).hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom

The arity-one projection is the unitor through the singleton identification.

theorem RS.modPowOne_inv {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] (A : D) [CategoryTheory.MonObj A] (X : D) [CategoryTheory.ModObj A X] : (modPowOne A X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (modPowπ A X 1)

The singleton inverse is the unitor into the projection.

theorem RS.twistPow_cover_factor {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] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] (V : D) (R : CategoryTheory.Mod D A) (k : ℕ) : CategoryTheory.CategoryStruct.comp (modPowπ A (tensorLeftMod A V R).X (k + 1)) (twistPowModIso A V R k).hom.hom = CategoryTheory.CategoryStruct.comp (plainShuffle V R.X (k + 1)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (tensorPow D V (k + 1)) (modPowπ A R.X (k + 1)))

The cover factorisation: over the plain covers, the twisted power identification is the diagonal shuffle followed by the projection of the module factor.