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_span {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set M} (hs : s.finite) :
theorem submodule.fg_span_singleton {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] (x : 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.

theorem submodule.map_fg_of_fg {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] (I : ideal R) (h : submodule.fg I) (f : R →+* S) :

The image of a finitely generated ideal is finitely generated.

theorem submodule.fg_ker_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [add_comm_group P] [module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf1 : f.ker.fg) (hf2 : g.ker.fg) (hsur : function.surjective f) :
(g.comp f).ker.fg

The kernel of the composition of two linear maps is finitely generated if both kernels are and the first morphism is surjective.

theorem submodule.fg_restrict_scalars {R : Type u_1} {S : Type u_2} {M : Type u_3} [comm_ring R] [comm_ring S] [algebra R S] [add_comm_group M] [module S M] [module R M] [is_scalar_tower R S M] (N : submodule S M) (hfin : N.fg) (h : function.surjective (algebra_map R S)) :
theorem submodule.fg_ker_ring_hom_comp {R : Type u_1} {S : Type u_2} {A : Type u_3} [comm_ring R] [comm_ring S] [comm_ring A] (f : R →+* S) (g : S →+* A) (hf : submodule.fg f.ker) (hg : submodule.fg g.ker) (hsur : function.surjective f) :
theorem submodule.fg_iff_compact {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [semimodule R M] (s : submodule R M) :

Finitely generated submodules are precisely compact elements in the submodule lattice.

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

Instances
@[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])