Noetherian rings and modules
The following are equivalent for a module M over a ring R:
- Every increasing chain of submodule M₁ ⊆ M₂ ⊆ M₃ ⊆ ⋯ eventually stabilises.
- 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.
R be a ring and let
N be an
fg N : Propis the assertion that
Nis finitely generated as an
is_noetherian R Mis the proposition that
Mis a Noetherian
R-module. It is a class, implemented as the predicate that all
Mare finitely generated.
exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smulis 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.
Note that the Hilbert basis theorem, that if a commutative ring R is Noetherian then so is R[X],
is proved in
- [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]
Noetherian, noetherian, Noetherian ring, Noetherian module, noetherian ring, noetherian module
Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV
If 0 → M' → M → M'' → 0 is exact and M' and M'' are finitely generated then so is M.
is_noetherian R M is the proposition that
M is a Noetherian
implemented as the predicate that all
M are finitely generated.
A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them.
A ring is Noetherian if it is Noetherian as a module over itself, i.e. all its ideals are finitely generated.