def CoherentSpecFinitelyGenerated.IsLocallyFinitelyGenerated (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] : Prop

An R-module M is locally finitely generated if there exists a finite set of elements of R generating the unit ideal such that each corresponding localization of M is finitely generated.

theorem CoherentSpecFinitelyGenerated.lemma23_coherent_tilde_iff_fg (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] : IsLocallyFinitelyGenerated R M ↔ Module.Finite R M

Lemma 23 (Lec 12): on Spec A the sheaf M̃ is coherent (i.e. locally finitely generated) iff the module M is finitely generated as an R-module.