Nonzero representable generators of finite functors

Every nonzero finite-dimensional functor receives a nonzero morphism from one finite-dimensional representable. This is the componentwise form of the finite-representable generation theorem.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_exists_nonzero_representableMap {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (hM : ¬CategoryTheory.Limits.IsZero M) : ∃ (X : C) (f : finiteDimensionalLinearCoyoneda X ⋯ ⟶ M), f ≠ 0

A nonzero finite-dimensional functor receives a nonzero map from a finite-dimensional representable.