Noetherian rings and modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
Let R
be a ring and let M
and P
be R
-modules. Let N
be an R
-submodule of M
.
is_noetherian R M
is the proposition thatM
is a NoetherianR
-module. It is a class, implemented as the predicate that allR
-submodules ofM
are finitely generated.
Main statements #
is_noetherian_iff_well_founded
is the theorem that an R-module M is Noetherian iff>
is well-founded onsubmodule 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]
- [samuel1967]
Tags #
Noetherian, noetherian, Noetherian ring, Noetherian module, noetherian ring, noetherian module
is_noetherian R M
is the proposition that M
is a Noetherian R
-module,
implemented as the predicate that all R
-submodules of 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
prove that ι → ℝ
is finite dimensional over ℝ
).
A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them.
If ∀ 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.
A sequence f
of submodules of a noetherian module,
with f (n+1)
disjoint from the supremum of f 0
, ..., f n
,
is eventually zero.
If M ⊕ N
embeds into M
, for M
noetherian over R
, then N
is trivial.
Equations
A (semi)ring is Noetherian if it is Noetherian as a module over itself, i.e. all its ideals are finitely generated.
Equations
- 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.
If M / S / R
is a scalar tower, and M / R
is Noetherian, then M / S
is
also noetherian.
In a module over a noetherian ring, the submodule generated by finitely many vectors is noetherian.