Noetherian rings and modules

The following are equivalent for a module M over a ring R:

1. Every increasing chain of submodule M₁ ⊆ M₂ ⊆ M₃ ⊆ ⋯ eventually stabilises.
2. Every submodule is finitely generated.

A module satisfying these equivalent conditions is said to be a Noetherian R-module. A ring is a Noetherian ring if it is Noetherian as a module over itself.

Main definitions

Let R be a ring and let M and P be R-modules. Let N be an R-submodule of M.

• fg N : Prop is the assertion that N is finitely generated as an R-module.

• is_noetherian R M is the proposition that M is a Noetherian R-module. It is a class, implemented as the predicate that all R-submodules of M are finitely generated.

Main statements

• exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul is Nakayama's lemma, in the following form: if N is a finitely generated submodule of an ambient R-module M and I is an ideal of R such that N ⊆ IN, then there exists r ∈ 1 + I such that rN = 0.

• is_noetherian_iff_well_founded is the theorem that an R-module M is Noetherian iff > is well-founded on submodule R M.

Note that the Hilbert basis theorem, that if a commutative ring R is Noetherian then so is R[X], is proved in ring_theory.polynomial.

References

• [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]

Tags

Noetherian, noetherian, Noetherian ring, Noetherian module, noetherian ring, noetherian module