mathlib documentation

ring_theory.noetherian

Noetherian rings and modules

The following are equivalent for a module M over a ring R:

  1. Every increasing chain of submodule 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.

Main definitions

Let R be a ring and let M and P be R-modules. Let N be an R-submodule of M.

Main statements

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

Tags

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

def submodule.fg {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] (N : submodule R M) :
Prop

A submodule of M is finitely generated if it is the span of a finite subset of M.

Equations
theorem submodule.fg_def {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {N : submodule R M} :
N.fg ∃ (S : set M), S.finite submodule.span R S = N

theorem submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] (I : ideal R) (N : submodule R M) (hn : N.fg) (hin : N I N) :
∃ (r : R), r - 1 I ∀ (n : M), n Nr n = 0

Nakayama's Lemma. Atiyah-Macdonald 2.5, Eisenbud 4.7, Matsumura 2.2, Stacks 00DV

theorem submodule.fg_bot {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] :

theorem submodule.fg_sup {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {N₁ N₂ : submodule R M} (hN₁ : N₁.fg) (hN₂ : N₂.fg) :
(N₁ N₂).fg

theorem submodule.fg_map {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {P : Type u_3} [add_comm_monoid P] [semimodule R P] {f : M →ₗ[R] P} {N : submodule R M} (hs : N.fg) :

theorem submodule.fg_of_fg_map {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [module R M] [add_comm_group P] [module R P] (f : M →ₗ[R] P) (hf : f.ker = ) {N : submodule R M} (hfn : (submodule.map f N).fg) :
N.fg

theorem submodule.fg_top {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (N : submodule R M) :

theorem submodule.fg_of_linear_equiv {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {P : Type u_3} [add_comm_monoid P] [semimodule R P] (e : M ≃ₗ[R] P) (h : .fg) :

theorem submodule.fg_prod {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {P : Type u_3} [add_comm_monoid P] [semimodule R P] {sb : submodule R M} {sc : submodule R P} (hsb : sb.fg) (hsc : sc.fg) :
(sb.prod sc).fg

theorem submodule.fg_of_fg_map_of_fg_inf_ker {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [module R M] [add_comm_group P] [module R P] (f : M →ₗ[R] P) {s : submodule R M} (hs1 : (submodule.map f s).fg) (hs2 : (s f.ker).fg) :
s.fg

If 0 → M' → M → M'' → 0 is exact and M' and M'' are finitely generated then so is M.

@[class]
structure is_noetherian (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [semimodule R M] :
Prop

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
theorem is_noetherian_submodule {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {N : submodule R M} :
is_noetherian R N ∀ (s : submodule R M), s N → s.fg

theorem is_noetherian_submodule_left {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {N : submodule R M} :
is_noetherian R N ∀ (s : submodule R M), (N s).fg

theorem is_noetherian_submodule_right {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {N : submodule R M} :
is_noetherian R N ∀ (s : submodule R M), (s N).fg

@[instance]
def is_noetherian_submodule' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_noetherian R M] (N : submodule R M) :

theorem is_noetherian_of_surjective {R : Type u_1} (M : Type u_2) {P : Type u_3} [ring R] [add_comm_group M] [add_comm_group P] [module R M] [module R P] (f : M →ₗ[R] P) (hf : f.range = ) [is_noetherian R M] :

theorem is_noetherian_of_linear_equiv {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [add_comm_group P] [module R M] [module R P] (f : M ≃ₗ[R] P) [is_noetherian R M] :

theorem is_noetherian_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [add_comm_group P] [module R M] [module R P] [is_noetherian R P] (f : M →ₗ[R] P) (hf : f.ker = ) :

theorem fg_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [add_comm_group P] [module R M] [module R P] [is_noetherian R P] {N : submodule R M} (f : M →ₗ[R] P) (hf : f.ker = ) :
N.fg

@[instance]
def is_noetherian_prod {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [add_comm_group P] [module R M] [module R P] [is_noetherian R M] [is_noetherian R P] :

@[instance]
def is_noetherian_pi {R : Type u_1} {ι : Type u_2} {M : ι → Type u_3} [ring R] [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [fintype ι] [∀ (i : ι), is_noetherian R (M i)] :
is_noetherian R (Π (i : ι), M i)

theorem is_noetherian_iff_well_founded {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :

theorem well_founded_submodule_gt (R : Type u_1) (M : Type u_2) [ring R] [add_comm_group M] [module R M] [is_noetherian R M] :

theorem finite_of_linear_independent {R : Type u_1} {M : Type u_2} [comm_ring R] [nontrivial R] [add_comm_group M] [module R M] [is_noetherian R M] {s : set M} (hs : linear_independent R coe) :

theorem set_has_maximal_iff_noetherian {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :
(∀ (a : set (submodule R M)), a.nonempty(∃ (M' : submodule R M) (H : M' a), ∀ (I : submodule R M), I aM' II = M')) is_noetherian R M

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

theorem is_noetherian.induction {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_noetherian R M] {P : submodule R M → Prop} (hgt : ∀ (I : submodule R M), (∀ (J : submodule R M), J > IP J)P I) (I : submodule R M) :
P I

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

@[class]
def is_noetherian_ring (R : Type u_1) [ring R] :
Prop

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

Equations
Instances
@[instance]

@[instance]
def ring.is_noetherian_of_fintype (R : Type u_1) (M : Type u_2) [fintype M] [ring R] [add_comm_group M] [module R M] :

theorem ring.is_noetherian_of_zero_eq_one {R : Type u_1} [ring R] (h01 : 0 = 1) :

theorem is_noetherian_of_submodule_of_noetherian (R : Type u_1) (M : Type u_2) [ring R] [add_comm_group M] [module R M] (N : submodule R M) (h : is_noetherian R M) :

theorem is_noetherian_of_quotient_of_noetherian (R : Type u_1) [ring R] (M : Type u_2) [add_comm_group M] [module R M] (N : submodule R M) (h : is_noetherian R M) :

theorem is_noetherian_of_fg_of_noetherian {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (N : submodule R M) [is_noetherian_ring R] (hN : N.fg) :

theorem is_noetherian_of_fg_of_noetherian' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_noetherian_ring R] (h : .fg) :

theorem is_noetherian_span_of_finite (R : Type u_1) {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_noetherian_ring R] {A : set M} (hA : A.finite) :

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

theorem is_noetherian_ring_of_surjective (R : Type u_1) [comm_ring R] (S : Type u_2) [comm_ring S] (f : R →+* S) (hf : function.surjective f) [H : is_noetherian_ring R] :

@[instance]
def is_noetherian_ring_set_range {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] (f : R →+* S) [is_noetherian_ring R] :

@[instance]
def is_noetherian_ring_range {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] (f : R →+* S) [is_noetherian_ring R] :

theorem is_noetherian_ring_of_ring_equiv (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] (f : R ≃+* S) [is_noetherian_ring R] :

theorem submodule.fg_mul {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (M N : submodule R A) (hm : M.fg) (hn : N.fg) :
(M * N).fg

theorem submodule.fg_pow {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (M : submodule R A) (h : M.fg) (n : ) :
(M ^ n).fg

theorem exists_prime_spectrum_prod_le {R : Type u_1} [comm_ring R] [is_noetherian_ring R] (I : ideal R) :

In a noetherian ring, every ideal contains a product of prime ideals ([samuel, § 3.3, Lemma 3])

In a noetherian integral domain which is not a field, every non-zero ideal contains a non-zero product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as product or prime ideals ([samuel, § 3.3, Lemma 3])