# mathlibdocumentation

ring_theory.noetherian

# Noetherian rings and modules #

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

1. Every increasing chain of submodules 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.

(Note that we do not assume yet that our rings are commutative, so perhaps this should be called "left Noetherian". To avoid cumbersome names once we specialize to the commutative case, we don't make this explicit in the declaration names.)

## 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.

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

## Tags #

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