Finitely generated modules with finitely many elements

A module M over a commutative ring A is a module over A ⧸ ann_A M, on which it is faithful. Hence the quotient A ⧸ ann_A M embeds into the additive endomorphisms of M, and is finite when M is. Conversely a finitely generated module over a finite ring is finite. So a finitely generated module is finite exactly when the quotient of the ring by its annihilator is.

Main results

• Module.finite_quotient_annihilator: the quotient of the ring by the annihilator of a finite module is finite.
• Module.finite_iff_finite_quotient_annihilator: a finitely generated module is finite iff the quotient of the ring by its annihilator is finite.

theorem Module.finite_quotient_annihilator {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [Finite M] : Finite (A ⧸ annihilator A M)

The quotient of the ring by the annihilator of a finite module is finite: it embeds into the additive endomorphisms of the module.

theorem Module.finite_iff_finite_quotient_annihilator {A : Type u_1} {M : Type u_2} [CommRing A] [AddCommGroup M] [Module A M] [Module.Finite A M] : Finite M ↔ Finite (A ⧸ annihilator A M)

A finitely generated module is finite iff the quotient of the ring by its annihilator is finite.