FGModuleCat: pin the universe, or Module.Finite k (X ⟶ Y) is not found

With variable (k : Type) [Field k], writing FGModuleCat k leaves the object universe as a metavariable, and inferInstance : FiniteDimensional k (X ⟶ Y) then fails. FGModuleCat.{0} k (or FGModuleCat.{v} k with v fixed) finds Mathlib's Module.Finite K (V ⟶ W) instance at once. Also, HasFiniteBiproducts (FGModuleCat k) is not found from its Abelian instance when a lemma takes [Preadditive C] [HasFiniteBiproducts C] separately (instance diamond). Add instance : HasFiniteBiproducts (FGModuleCat.{v} k) := .of_hasFiniteProducts. With both, a general criterion like 'Hom-finite + idempotent complete ⇒ Krull–Schmidt' applies directly.