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.
is_noetherian_iff_well_foundedis 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
- [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]
Noetherian, noetherian, Noetherian ring, Noetherian module, noetherian ring, noetherian module
A submodule of
M is finitely generated if it is the span of a finite subset of
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.
Finitely generated submodules are precisely compact elements in the submodule lattice.
A finitely generated idempotent ideal is generated by an idempotent element
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
An R-module is Noetherian iff all its submodules are finitely-generated.
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.
Any surjective endomorphism of a Noetherian module is injective.
Any surjective endomorphism of a Noetherian module is bijective.
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.
A (semi)ring is Noetherian if it is Noetherian as a module over itself, i.e. all its ideals are finitely generated.
- is_noetherian_ring R = is_noetherian R R
A ring is Noetherian if and only if all its ideals are finitely-generated.
Modules over the trivial ring are Noetherian.
M / S / R is a scalar tower, and
M / R is Noetherian, then
M / S is
In a module over a noetherian ring, the submodule generated by finitely many vectors is noetherian.