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

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.

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.

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)

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