The pair side of the power step

Deligne's 1.15 power induction, pair side: pushing the primed back merge and the swapped unprimed front merge into the successor power pairing yields the tensor pairing of the stage datum with the bottom datum. The comparison is taken over the projection cover, where the successor triangle core (powDeltaCore_pairing) supplies the identity after a symmetric rearrangement of the four carriers; the rearrangement itself is the retraction tensorMu_braid_retract, a pure braid coherence.

theorem RS.modPowPairing_succ_tensor {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)] [∀ (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') (n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorMap A (powMulMod A M'.X n 0) (CategoryTheory.CategoryStruct.comp (modTensorSwapMod A (modPowMod A M.X n) (modPowMod A M.X 0)) (CategoryTheory.CategoryStruct.comp (powMulMod A M.X 0 n) (modPowCastMod A M.X ⋯)))) (modPowPairing A M M' d (n + 1)) = tensorPair A (powDualityDatum A M M' d n) (powDualityDatum A M M' d 0)

The pair side of the power step (Deligne 1.15): pushing the primed back merge and the swapped unprimed front merge into the successor power pairing yields the tensor pairing of the stage datum with the bottom datum.