Whiskering by a nonzero object is faithful

In a rigid symmetric abelian category with simple unit, tensoring with a nonzero object kills no nonzero morphism. The contraction X ⊗ Xᘁ ⟶ 𝟙 (evaluation through the braiding) is nonzero — else the zigzag identity kills 𝟙 X — hence an epimorphism onto the simple unit; whiskering preserves it, and the exchange law then cancels it against f ▷ (X ⊗ Xᘁ) = 0.

Simplicity of the unit is carried as a hypothesis and discharged where End 𝟙 = ℂ is available.

theorem RS.evaluation_ne_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] {X : A} (hX : ¬CategoryTheory.Limits.IsZero X) : ε_ X Xᘁ ≠ 0

The evaluation of a nonzero object is nonzero: were it zero, the zigzag identity would make 𝟙 X zero.

theorem RS.eq_zero_of_whiskerRight_eq_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hs : CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) {X : A} (hX : ¬CategoryTheory.Limits.IsZero X) {P Q : A} {f : P ⟶ Q} (hw : CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = 0) : f = 0

Whiskering by a nonzero object is faithful on morphisms: in a rigid symmetric abelian category with simple unit, f ▷ X = 0 forces f = 0 when X is nonzero.

theorem RS.permAlg_symCast_ne_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalLinear ℂ A] (hs : CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) {X : A} (hX : ¬CategoryTheory.Limits.IsZero X) {m n : ℕ} (h : m ≤ n) (x : SymGroupAlgebra m) (hx : (permAlg X m) x ≠ 0) : (permAlg X n) ((symCast h) x) ≠ 0

theorem RS.isZero_tensor_of_isZero_left {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] {B V : A} (hB : CategoryTheory.Limits.IsZero B) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj B V)

A zero factor makes the tensor zero.

theorem RS.isZero_left_of_tensor_isZero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.SymmetricCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hs : CategoryTheory.Simple (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) {B V : A} (hV : ¬CategoryTheory.Limits.IsZero V) (h : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj B V)) : CategoryTheory.Limits.IsZero B

Base-change faithfulness (the kernel of Deligne 2.3): if the tensor with a nonzero dualizable object vanishes, the other factor vanishes — the whiskered evaluation is an epimorphism from a zero object.