Trace nondegeneracy, in Hom-typed form

HomSpace.eq_zero_of_traces_vanish is stated at the HomSpace level; the Karoubi envelope needs it at morphisms of skein objects, where the closure partner ranges over morphisms rather than fragments. Both forms are the same statement read through HomSpace.ofFragment.

With the nilpotent-trace vanishing of BlockFactorialTrace, this is what isSemisimpleRing_of_trace consumes to make every skein endomorphism algebra semisimple.

theorem RS.end_eq_zero_of_traces_vanish {R : ℕ} (f : EdgeRankParameter R) (Y : SkeinObj f) (a : Y ⟶ Y) (ha : ∀ (b : Y ⟶ Y), (HomSpace.traceMap f.val Y.arity) (CategoryTheory.CategoryStruct.comp a b) = 0) : a = 0

Trace nondegeneracy in the fully Hom-typed form: an endomorphism of a skein object all of whose composites have vanishing trace is zero.

theorem RS.hom_eq_zero_of_traces_vanish' {R : ℕ} (f : EdgeRankParameter R) (Y Z : SkeinObj f) (a : Y ⟶ Z) (ha : ∀ (b : Z ⟶ Y), (HomSpace.traceMap f.val Y.arity) (CategoryTheory.CategoryStruct.comp a b) = 0) : a = 0

Mixed-Hom trace nondegeneracy: a morphism between skein objects all of whose closures against reverse morphisms have vanishing trace is zero.