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

- `IsNoetherian 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 #

- `isNoetherian_iff` 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 `RingTheory.Polynomial`.

## References #

- [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]
- [P. Samuel, Algebraic Theory of Numbers][samuel1967]

## Tags #

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

source
class IsNoetherian (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :
Prop

`IsNoetherian 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.

- noetherian (s : Submodule R M) : s.FG

  `IsNoetherian 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

source
theorem isNoetherian_def {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
IsNoetherian R M ↔ ∀ (s : Submodule R M), s.FG

An R-module is Noetherian iff all its submodules are finitely-generated.

source
theorem isNoetherian_submodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :
IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG
source
theorem isNoetherian_submodule_left {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :
IsNoetherian R ↥N ↔ ∀ (s : Submodule R M), (N ⊓ s).FG
source
theorem isNoetherian_submodule_right {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :
IsNoetherian R ↥N ↔ ∀ (s : Submodule R M), (s ⊓ N).FG
source
instance isNoetherian_submodule' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (N : Submodule R M) :
IsNoetherian R ↥N
source
theorem isNoetherian_of_le {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Submodule R M} [ht : IsNoetherian R ↥t] (h : s ≤ t) :
IsNoetherian R ↥s
source
theorem isNoetherian_iff' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
IsNoetherian R M ↔ WellFoundedGT (Submodule R M)
source
theorem isNoetherian_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
IsNoetherian R M ↔ WellFounded fun (x1 x2 : Submodule R M) => x1 > x2
source
theorem IsNoetherian.wf {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
IsNoetherian R M → WellFounded fun (x1 x2 : Submodule R M) => x1 > x2

Alias of the forward direction of `isNoetherian_iff`.

source
theorem IsNoetherian.wellFoundedGT {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
IsNoetherian R M → WellFoundedGT (Submodule R M)

Alias of the forward direction of `isNoetherian_iff'`.

source
theorem isNoetherian_mk {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
WellFoundedGT (Submodule R M) → IsNoetherian R M

Alias of the reverse direction of `isNoetherian_iff'`.

source
instance wellFoundedGT {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [h : IsNoetherian R M] :
WellFoundedGT (Submodule R M)
source
theorem isNoetherian_iff_fg_wellFounded {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
IsNoetherian R M ↔ WellFoundedGT { N : Submodule R M // N.FG }
source
theorem set_has_maximal_iff_noetherian {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
(∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M

A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them.

source
theorem monotone_stabilizes_iff_noetherian {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :
(∀ (f : ℕ →o Submodule R M), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M

A module is Noetherian iff every increasing chain of submodules stabilizes.

source
theorem Module.End.eventually_disjoint_ker_pow_range_pow {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (f : End R M) :
∀ᶠ (n : ℕ) in Filter.atTop, Disjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))

For an endomorphism of a Noetherian module, any sufficiently large iterate has disjoint kernel and range.

source
theorem LinearMap.eventually_iSup_ker_pow_eq {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) :
∀ᶠ (n : ℕ) in Filter.atTop, ⨆ (m : ℕ), ker (f ^ m) = ker (f ^ n)
source
@[reducible, inline]
abbrev IsNoetherianRing (R : Type u_1) [Semiring R] :
Prop

A (semi)ring is Noetherian if it is Noetherian as a module over itself, i.e. all its ideals are finitely generated.

Equations

- IsNoetherianRing R = IsNoetherian R R

Instances For

source
theorem isNoetherianRing_iff {R : Type u_1} [Semiring R] :
IsNoetherianRing R ↔ IsNoetherian R R
source
theorem isNoetherianRing_iff_ideal_fg (R : Type u_1) [Semiring R] :
IsNoetherianRing R ↔ ∀ (I : Ideal R), I.FG

A ring is Noetherian if and only if all its ideals are finitely-generated.