Reflecting a finite relation through linear Yoneda

theorem CategoryTheory.linearYoneda_reflect_sum_relation {k : Type w} [Ring k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] {ι : Type u_1} [Fintype ι] {Z X : C} (V : ι → C) (p : (i : ι) → Z ⟶ V i) (q : (i : ι) → V i ⟶ X) (M : Functor Cᵒᵖ (ModuleCat k)) (inc : (i : ι) → (linearYoneda k C).obj (V i) ⟶ M) (h : M ⟶ (linearYoneda k C).obj X) (t : (linearYoneda k C).obj Z ⟶ M) (ht : t = ∑ i : ι, CategoryStruct.comp ((linearYoneda k C).map (p i)) (inc i)) (hq : ∀ (i : ι), (linearYoneda k C).map (q i) = CategoryStruct.comp (inc i) h) (hh : CategoryStruct.comp t h = 0) : ∑ i : ι, CategoryStruct.comp (p i) (q i) = 0

A relation among maps of representables reflects to the represented morphisms. The finite sum is evaluated at the identity of its source.