The power-level chain and the copairing powers

The module-power mirror of the symmetric chain: the power multiplication descends through the module-tensor coequalizer and bundles as a module map; through the interchange, power stages multiply; the copairing seeds the bottom stage, and the iterated seed multiplication is the copairing power of the duality datum.

theorem RS.modPowMul_modTensor_cond {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] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorLegM A (modPowMod A X m) (modPowMod A X n)) (modPowMul A X (m + 1) (n + 1)) = CategoryTheory.CategoryStruct.comp (modTensorLegN A (modPowMod A X m) (modPowMod A X n)) (modPowMul A X (m + 1) (n + 1))

The two module-tensor legs of a pair of module powers agree after the power multiplication.

noncomputable def RS.powMulDesc {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] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : modTensor A (modPowMod A X m) (modPowMod A X n) ⟶ modPow A X (m + 1 + n + 1)

The descended power multiplication on the module tensor product of two module powers.

Equations

• RS.powMulDesc A X m n = RS.modTensorDesc A (RS.modPowMod A X m) (RS.modPowMod A X n) (RS.modPowMul A X (m + 1) (n + 1)) ⋯

@[simp]

theorem RS.modTensorπ_powMulDesc {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] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modPowMod A X m) (modPowMod A X n)) (powMulDesc A X m n) = modPowMul A X (m + 1) (n + 1)

Defining equation of the descended power multiplication.

@[simp]

theorem RS.modTensorπ_powMulDesc_assoc {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] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) {Z : D} (h : modPow A X (m + 1 + n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (modTensorπ A (modPowMod A X m) (modPowMod A X n)) (CategoryTheory.CategoryStruct.comp (powMulDesc A X m n) h) = CategoryTheory.CategoryStruct.comp (modPowMul A X (m + 1) (n + 1)) h

Defining equation of the descended power multiplication.

theorem RS.powMulDesc_act {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] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : CategoryTheory.CategoryStruct.comp (modTensorAct A (modPowMod A X m) (modPowMod A X n)) (powMulDesc A X m n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (powMulDesc A X m n)) (modPowAct A X (m + 1 + n))

The descended power multiplication intertwines the module actions.

noncomputable def RS.powMulMod {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] (X : D) [CategoryTheory.ModObj A X] (m n : ℕ) : modTensorMod A (modPowMod A X m) (modPowMod A X n) ⟶ modPowMod A X (m + 1 + n)

The descended power multiplication as a map of modules.

Equations

• RS.powMulMod A X m n = CategoryTheory.Mod.Hom.mk' (RS.powMulDesc A X m n) ⋯

theorem RS.actLeft_modPowOne_inv {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] (X : D) [CategoryTheory.ModObj A X] : CategoryTheory.CategoryStruct.comp (actLeft A X) (modPowOne A X).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (modPowOne A X).inv) (modPowAct A X 0)

The inverse of the singleton power iso carries the module action to the descended action.

noncomputable def RS.toModPowModZero {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] (M : CategoryTheory.Mod D A) : M ⟶ modPowMod A M.X 0

A module maps into the singleton stage of its power tower.

Equations

• RS.toModPowModZero A M = CategoryTheory.Mod.Hom.mk' (RS.modPowOne A M.X).inv ⋯

noncomputable def RS.powStage {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] (M M' : CategoryTheory.Mod D A) (k : ℕ) : D

One stage of the power chain: the module tensor product of matching module powers of the dual pair, in copairing order.

Equations

• RS.powStage A M M' k = RS.modTensor A (RS.modPowMod A M.X k) (RS.modPowMod A M'.X k)

noncomputable def RS.powChainMul {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) (m n : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (powStage A M M' m) (powStage A M M' n) ⟶ powStage A M M' (m + 1 + n)

The power chain multiplication: two power stages interchange and multiply into the stage of summed arity.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.powSeed {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] (M M' : CategoryTheory.Mod D A) (d : ModDualityDatum A M M') : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ powStage A M M' 0

The seed of the power chain: the copairing lands in the bottom stage.

Equations

• RS.powSeed A M M' d = CategoryTheory.CategoryStruct.comp (RS.copairUnit A M M' d) (RS.modTensorMap A (RS.toModPowModZero A M) (RS.toModPowModZero A M'))

noncomputable def RS.modPowCastMod {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] (X : D) [CategoryTheory.ModObj A X] {a b : ℕ} (h : a + 1 = b + 1) : modPowMod A X a ⟶ modPowMod A X b

An arity transport of module powers, as a map of modules.

Equations

• RS.modPowCastMod A X h = CategoryTheory.Mod.Hom.mk' (RS.modPowCast A X h) ⋯

noncomputable def RS.modTensorSwapMod {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] (P Q : CategoryTheory.Mod D A) : modTensorMod A P Q ⟶ modTensorMod A Q P

The braiding of the module tensor product, as a map of modules.

Equations

• RS.modTensorSwapMod A P Q = CategoryTheory.Mod.Hom.mk' (RS.modTensorSwap A P Q) ⋯

noncomputable def RS.powDelta {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') (k : ℕ) : powStage A M M' k ⟶ powStage A M M' (k + 1)

The power chain transition: insert the seed at the outer position of the nested pairing — the new factor joins the M-power at the front and the M'-power at the back, so the peel of the nested pairing removes exactly the inserted pair.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.powUnitStage {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') (k : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ powStage A M M' k

The copairing powers: the iterated seed multiplication along the power chain.

Equations

• RS.powUnitStage A M M' d 0 = RS.powSeed A M M' d
• RS.powUnitStage A M M' d k.succ = CategoryTheory.CategoryStruct.comp (RS.powUnitStage A M M' d k) (RS.powDelta A M M' d k)

theorem RS.powUnitStage_succ {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') (k : ℕ) : CategoryTheory.CategoryStruct.comp (powUnitStage A M M' d k) (powDelta A M M' d k) = powUnitStage A M M' d (k + 1)

The copairing powers ride along the transitions.