Noetherian rings and modules #
The following are equivalent for a module M over a ring R:
- Every increasing chain of submodules 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.
(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 #
R be a ring and let
N be an
submodule.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.
Main statements #
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.
The kernel of the composition of two linear maps is finitely generated if both kernels are and the first morphism is surjective.
is_noetherian R M is the proposition that
M is a Noetherian
implemented as the predicate that all
M are finitely generated.
Instances of this typeclass
A version of
is_noetherian_pi for non-dependent functions. We need this instance because
sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to
ι → ℝ is finite dimensional over
A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them.
∀ I > J, P I implies
P J, then
P holds for all submodules.
If the first and final modules in a short exact sequence are noetherian, then the middle module is also noetherian.
For any endomorphism of a Noetherian module, there is some nontrivial iterate with disjoint kernel and range.
f of submodules of a noetherian module,
f (n+1) disjoint from the supremum of
f 0, ...,
is eventually zero.
M ⊕ N embeds into
M noetherian over
N is trivial.
M / S / R is a scalar tower, and
M / R is Noetherian, then
M / S is