Merging the sandwich tower into a power pair

Each stage of the sandwich tower reassembles, up to associators and braidings of the module tensor product, into a pair of module powers: the stage sandwichTower A M M' (k + 1) carries k + 2 letters M interleaved with k + 1 letters M', and the shuffle collects them into modPowMod A M.X (k + 1) (carrier modPow A M.X (k + 2), so k + 2 letters M) tensored with modPowMod A M'.X k (carrier modPow A M'.X (k + 1), so k + 1 letters M').

• modTensorSwapModIso: the braiding as a module isomorphism.
• leftMergeModIso: absorb a module into its own power from the left.
• sandwichMergeModIso: the merge, as modules.
• sandwichMergeIso: the merge at the carrier level.
• isZero_sandwichTower_of_isZero_modPow: vanishing of the power descends to every tower stage.

noncomputable def RS.modTensorSwapModIso {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 an isomorphism of modules.

Equations

• RS.modTensorSwapModIso A P Q = { hom := RS.modTensorSwapMod A P Q, inv := RS.modTensorSwapMod A Q P, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def RS.leftMergeModIso {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] (N : CategoryTheory.Mod D A) (n : ℕ) : modTensorMod A N (modPowMod A N.X n) ≅ modPowMod A N.X (n + 1)

The left absorption: a module merges into its own power from the left, through the braiding, the bottom-stage identification and the adjacent merge.

Equations

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

noncomputable def RS.sandwichMergeModIso {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) (k : ℕ) : sandwichTower A M M' (k + 1) ≅ modTensorMod A (modPowMod A M.X (k + 1)) (modPowMod A M'.X k)

The sandwich merge: the (k + 1)-st tower stage carries k + 2 letters M and k + 1 letters M', and reassembles as the module tensor product of the corresponding module powers.

Equations

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

noncomputable def RS.sandwichMergeIso {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) (k : ℕ) : (sandwichTower A M M' (k + 1)).X ≅ modTensor A (modPowMod A M.X (k + 1)) (modPowMod A M'.X k)

The sandwich merge at the carrier level: the carrier of the (k + 1)-st tower stage is the relative tensor product of modPow A M.X (k + 2) with modPow A M'.X (k + 1), presented through the bundled module powers.

Equations

• RS.sandwichMergeIso A M M' k = { hom := (RS.sandwichMergeModIso A M M' k).hom.hom, inv := (RS.sandwichMergeModIso A M M' k).inv.hom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem RS.isZero_sandwichTower_of_isZero_modPow {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) (k : ℕ) (h : CategoryTheory.Limits.IsZero (modPow A M.X (k + 2))) : CategoryTheory.Limits.IsZero (sandwichTower A M M' (k + 1)).X

Vanishing descends the tower: if the (k + 2)-nd relative power of the module vanishes, so does the carrier of the (k + 1)-st sandwich tower stage.