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
• P. Samuel, Algebraic Theory of Numbers

Tags

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

theorem isNoetherian_of_surjective {R : Type u_1} (M : Type u_2) {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] (f : M →ₗ[R] P) (hf : LinearMap.range f = ⊤) [IsNoetherian R M] : IsNoetherian R P

instance isNoetherian_range {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] (f : M →ₗ[R] P) [IsNoetherian R M] : IsNoetherian R ↥(LinearMap.range f)

instance isNoetherian_quotient {R : Type u_1} [Semiring R] {A : Type u_4} {M : Type u_5} [Ring A] [AddCommGroup M] [SMul R A] [Module R M] [Module A M] [IsScalarTower R A M] (N : Submodule A M) [IsNoetherian R M] : IsNoetherian R (M ⧸ N)

theorem isNoetherian_of_linearEquiv {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] (f : M ≃ₗ[R] P) [IsNoetherian R M] : IsNoetherian R P

theorem LinearEquiv.isNoetherian_iff {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] (f : M ≃ₗ[R] P) : IsNoetherian R M ↔ IsNoetherian R P

theorem isNoetherian_top_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : IsNoetherian R ↥⊤ ↔ IsNoetherian R M

theorem isNoetherian_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] [IsNoetherian R P] (f : M →ₗ[R] P) (hf : Function.Injective ⇑f) : IsNoetherian R M

theorem fg_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P) (hf : Function.Injective ⇑f) : N.FG

@[instance 80]

instance isNoetherian_of_finite (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Finite M] : IsNoetherian R M

@[instance 100]

instance Module.IsNoetherian.finite (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] : Module.Finite R M

instance Module.instFiniteSubtypeMemIdealOfIsNoetherian {R₁ : Type u_4} {S : Type u_5} [CommSemiring R₁] [Semiring S] [Algebra R₁ S] [IsNoetherian R₁ S] (I : Ideal S) : Module.Finite R₁ ↥I

theorem Module.Finite.of_injective {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [IsNoetherian R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) : Module.Finite R M

theorem isNoetherian_of_ker_bot {R : Type u_1} {M : Type u_2} {P : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] [IsNoetherian R P] (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) : IsNoetherian R M

theorem fg_of_ker_bot {R : Type u_1} {M : Type u_2} {P : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) : N.FG

instance isNoetherian_prod {R : Type u_1} {M : Type u_2} {P : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] [IsNoetherian R M] [IsNoetherian R P] : IsNoetherian R (M × P)

instance isNoetherian_sup {R : Type u_1} {P : Type u_4} [Ring R] [AddCommGroup P] [Module R P] (M₁ M₂ : Submodule R P) [IsNoetherian R ↥M₁] [IsNoetherian R ↥M₂] : IsNoetherian R ↥(M₁ ⊔ M₂)

instance isNoetherian_pi {R : Type u_1} [Ring R] {ι : Type u_5} [Finite ι] {M : ι → Type u_6} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), IsNoetherian R (M i)] : IsNoetherian R ((i : ι) → M i)

instance isNoetherian_pi' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_5} [Finite ι] [IsNoetherian R M] : IsNoetherian R (ι → M)

A version of isNoetherian_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 ℝ).

instance isNoetherian_iSup {R : Type u_1} {P : Type u_4} [Ring R] [AddCommGroup P] [Module R P] {ι : Type u_5} [Finite ι] {M : ι → Submodule R P} [∀ (i : ι), IsNoetherian R ↥(M i)] : IsNoetherian R ↥(⨆ (i : ι), M i)

theorem isNoetherian_of_range_eq_ker {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [IsNoetherian R M] [IsNoetherian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : LinearMap.range f = LinearMap.ker g) : IsNoetherian R N

If the first and final modules in an exact sequence are Noetherian, then the middle module is also Noetherian.

theorem isNoetherian_iff_submodule_quotient {R : Type u_1} {P : Type u_4} [Ring R] [AddCommGroup P] [Module R P] (S : Submodule R P) : IsNoetherian R P ↔ IsNoetherian R ↥S ∧ IsNoetherian R (P ⧸ S)

instance isNoetherian_linearMap_pi (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] {ι : Type u_4} [Finite ι] : IsNoetherian R ((ι → R) →ₗ[R] M)

instance isNoetherian_linearMap (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [IsNoetherian R M] [Module.Finite R N] : IsNoetherian R (N →ₗ[R] M)

theorem IsNoetherian.induction {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] {P : Submodule R M → Prop} (hgt : ∀ (I : Submodule R M), (∀ J > I, P J) → P I) (I : Submodule R M) : P I

If ∀ I > J, P I implies P J, then P holds for all submodules.

theorem LinearMap.isNoetherian_iff_of_bijective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_3} {P : Type u_4} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] P) (hl : Function.Bijective ⇑l) : IsNoetherian R M ↔ IsNoetherian S P

theorem Submodule.finite_ne_bot_of_iSupIndep {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] {ι : Type u_5} {N : ι → Submodule R M} (h : iSupIndep N) : {i : ι | N i ≠ ⊥}.Finite

theorem LinearIndependent.finite_of_isNoetherian {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] [Nontrivial R] {ι : Type u_5} {v : ι → M} (hv : LinearIndependent R v) : Finite ι

A linearly-independent family of vectors in a module over a non-trivial ring must be finite if the module is Noetherian.

theorem LinearIndependent.set_finite_of_isNoetherian {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] [Nontrivial R] {s : Set M} (hi : LinearIndependent R Subtype.val) : s.Finite

theorem IsNoetherian.disjoint_partialSups_eventually_bot {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (f : ℕ → Submodule R M) (h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊥

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.

@[instance 100]

instance isNoetherian_of_subsingleton (R : Type u_1) (M : Type u_2) [Subsingleton R] [Semiring R] [AddCommMonoid M] [Module R M] : IsNoetherian R M

Modules over the trivial ring are Noetherian.

theorem isNoetherian_of_submodule_of_noetherian (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) (h : IsNoetherian R M) : IsNoetherian R ↥N

theorem isNoetherian_of_tower (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [SMul R S] [Module S M] [Module R M] [IsScalarTower R S M] (h : IsNoetherian R M) : IsNoetherian S M

If M / S / R is a scalar tower, and M / R is Noetherian, then M / S is also Noetherian.

instance isNoetherian_of_isNoetherianRing_of_finite (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : IsNoetherian R M

theorem isNoetherian_of_fg_of_noetherian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [I : IsNoetherianRing R] (hN : N.FG) : IsNoetherian R ↥N

theorem isNoetherian_span_of_finite (R : Type u_1) {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] {A : Set M} (hA : A.Finite) : IsNoetherian R ↥(Submodule.span R A)

In a module over a Noetherian ring, the submodule generated by finitely many vectors is Noetherian.

theorem IsNoetherianRing.of_finite (R : Type u_1) (S : Type u_2) [Ring R] [Ring S] [Module R S] [IsScalarTower R S S] [IsNoetherianRing R] [Module.Finite R S] : IsNoetherianRing S

theorem isNoetherianRing_of_surjective (R : Type u_1) [Semiring R] (S : Type u_2) [Semiring S] (f : R →+* S) (hf : Function.Surjective ⇑f) [H : IsNoetherianRing R] : IsNoetherianRing S

instance isNoetherianRing_rangeS {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) [IsNoetherianRing R] : IsNoetherianRing ↥f.rangeS

instance isNoetherianRing_range {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] (f : R →+* S) [IsNoetherianRing R] : IsNoetherianRing ↥f.range

theorem isNoetherianRing_of_ringEquiv (R : Type u_1) [Semiring R] {S : Type u_2} [Semiring S] (f : R ≃+* S) [IsNoetherianRing R] : IsNoetherianRing S

instance instIsNoetherianRingProd {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [IsNoetherianRing R] [IsNoetherianRing S] : IsNoetherianRing (R × S)

instance instIsNoetherianRingForallOfFinite {ι : Type u_2} [Finite ι] {R : ι → Type u_1} [(i : ι) → Semiring (R i)] [∀ (i : ι), IsNoetherianRing (R i)] : IsNoetherianRing ((i : ι) → R i)