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
• [Sam67]

Tags

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

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.

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.

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

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

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

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

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

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)

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

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.

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

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

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)

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 }

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.

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.

@[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

theorem isNoetherianRing_iff {R : Type u_1} [Semiring R] : IsNoetherianRing R ↔ IsNoetherian R R

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.