theorem TensorCategories.isZero_dualTensor_tensor_of_isZero_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] (X Y : C) (h : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Xᘁ X) Y)

Auxiliary lemma: if X ⊗ Y is zero, then (Xᘁ ⊗ X) ⊗ Y is zero, obtained by tensoring on the left with Xᘁ and re-associating.

theorem TensorCategories.isZero_or_isZero_of_tensorObj_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)] (X Y : C) (h : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) : CategoryTheory.Limits.IsZero X ∨ CategoryTheory.Limits.IsZero Y

In a rigid abelian monoidal category with simple unit, if the tensor product X ⊗ Y is zero then at least one of X or Y is zero.