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))
:
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))
:
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.