Descent of power vanishing to the module #
Given the sandwich retract of a dualizable module, vanishing of a relative tensor power descends to the module itself: the retract iterates up the tower, and the tower reassembles into a power pair whose first factor is the vanishing power.
theorem
RS.isZero_of_sandwich_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)
(i₀ : M ⟶ modTensorMod A (modTensorMod A M M') M)
(r₀ : modTensorMod A (modTensorMod A M M') M ⟶ M)
(h₀ : CategoryTheory.CategoryStruct.comp i₀ r₀ = CategoryTheory.CategoryStruct.id M)
{n : ℕ}
(h : CategoryTheory.Limits.IsZero (modPow A M.X (n + 2)))
:
Power vanishing descends along the sandwich retract: a
module with a sandwich retract whose (n + 2)-nd relative power
vanishes is itself zero.