A vanishing tensor power forces a vanishing object

Deligne's 1.17 (Catégories tensorielles, 2002): in a symmetric monoidal preadditive category, an object X with a right dual whose n-th tensor power vanishes for some n ≠ 0 vanishes itself.

The descent step is isZero_tensorPow_pred: a vanishing (n + 2)-nd power forces a vanishing (n + 1)-st power. Writing the (n + 1)-st power as P ⊗ X, the triangle identity for the exact pairing (X, Xᘁ), whiskered on the left by P, factors the identity of P ⊗ X through P ⊗ ((X ⊗ Xᘁ) ⊗ X); associators and one braiding identify that object with the (n + 2)-nd power tensored with Xᘁ, which is zero because tensoring preserves zero objects over a preadditive monoidal structure. Downward induction and the left unitor then give the theorem.

theorem RS.isZero_tensorObj_of_isZero_tensorObj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] (X : A) [CategoryTheory.HasRightDual X] {P : A} (h : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj P X) X)) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj P X)

The descent step at a general left factor: if (P ⊗ X) ⊗ X vanishes, so does P ⊗ X. The identity of P ⊗ X factors through P ⊗ ((X ⊗ Xᘁ) ⊗ X) by the triangle identity for the pairing (X, Xᘁ) whiskered by P, and that object is zero, being isomorphic to ((P ⊗ X) ⊗ X) ⊗ Xᘁ by associators and the braiding β_ Xᘁ X.

theorem RS.isZero_tensorPow_pred {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] (X : A) [CategoryTheory.HasRightDual X] {n : ℕ} (h : CategoryTheory.Limits.IsZero (tensorPow A X (n + 2))) : CategoryTheory.Limits.IsZero (tensorPow A X (n + 1))

Deligne 1.17, descent: a vanishing (n + 2)-nd tensor power forces a vanishing (n + 1)-st tensor power.

theorem RS.isZero_of_isZero_tensorPow {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.Preadditive A] [CategoryTheory.MonoidalPreadditive A] (X : A) [CategoryTheory.HasRightDual X] {n : ℕ} (hn : n ≠ 0) (h : CategoryTheory.Limits.IsZero (tensorPow A X n)) : CategoryTheory.Limits.IsZero X

Deligne 1.17 (Catégories tensorielles): a vanishing tensor power forces a vanishing object — if X ^ ⊗ n = 0 for some n ≠ 0, then X = 0.