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] :
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) :
N.fgN 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} :
N₁.fgN₂.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} :
N.fg(submodule.map f 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} :
(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] :
(M ≃ₗ[R] P).fg.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} :
sb.fgsc.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} :
(submodule.map f s).fg(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) :

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) :
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} :

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.

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

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) :

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) :

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] :

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] :

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} :

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) :
M.fgN.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