Free modules of finite rank in FGModuleCat

The free module Fin k → R is projective among finitely generated modules, and every finitely generated module is a quotient of one. The first statement is projectivity in all modules transported along the forgetful functor, which preserves epimorphisms because it preserves finite colimits; the second is Module.Finite.exists_fin' read in the category.

Neither statement needs R noetherian, and this file no longer assumes it. Mathlib's PreservesFiniteColimits (forget₂ (FGModuleCat k) (ModuleCat k)) holds over any ring, because a finite colimit of finitely generated modules is a quotient of a finite coproduct. Noetherian hypotheses enter FGModuleCat for finite limits, where a kernel of finitely generated modules need not be finitely generated. The consumers below are noetherian for their own reasons, not for this one.

These are the "enough acyclic generators" inputs for coherent sheaves on an affine noetherian scheme, through Coh.affineEquivalence.

theorem FGModuleCat.exists_finFree_epi {R : Type u} [CommRing R] (M : FGModuleCat R) : ∃ (k : ℕ) (q : of R (Fin k → R) ⟶ M), CategoryTheory.Epi q

Every finitely generated module is a quotient of a free module of finite rank.

theorem FGModuleCat.projective_of_finFree {R : Type u} [CommRing R] (k : ℕ) : CategoryTheory.Projective (of R (Fin k → R))

Free modules of finite rank are projective among finitely generated modules: the forgetful functor to all modules preserves epimorphisms, so a lift in all modules is a lift.

No noetherian hypothesis. The epimorphism preservation comes from Mathlib's PreservesFiniteColimits instance for forget₂ (FGModuleCat R) (ModuleCat R), which is stated over any ring.