Linearity of the finite category-algebra equivalence

instance MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.moduleEquivalence_additive {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (moduleEquivalence hP).functor.Additive

instance MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.moduleEquivalence_linear {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Functor.Linear k (moduleEquivalence hP).functor