Points of objects tensor without vanishing

In the setting of Deligne's theorem the tensor unit is simple, so a nonzero morphism out of it is a monomorphism; whiskering is exact, so the tensor of two nonzero points is again a monomorphism, and in particular nonzero. This is the input that makes a tensor product of nonzero algebras nonzero.

theorem RS.mono_of_point_ne_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {X : A} {u : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ X} (h : u ≠ 0) : CategoryTheory.Mono u

A nonzero point is a monomorphism: the unit is simple.

theorem RS.mono_tensorHom_point {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {X Y : A} {u : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ X} {v : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ Y} (hu0 : u ≠ 0) (hv0 : v ≠ 0) : CategoryTheory.Mono (CategoryTheory.MonoidalCategoryStruct.tensorHom u v)

The tensor of two nonzero points is a monomorphism.

theorem RS.tensorHom_point_ne_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {X Y : A} {u : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ X} {v : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ Y} (hu0 : u ≠ 0) (hv0 : v ≠ 0) : CategoryTheory.MonoidalCategoryStruct.tensorHom u v ≠ 0

The tensor of two nonzero points is nonzero.