Finitely generated modules

Extensions of Mathlib's FGModuleCat: free modules of finite rank are projective, every finitely generated module is a quotient of one, and finite modules over a Noetherian ring are Noetherian objects.