# mathlibdocumentation

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.

• fg N : Prop is the assertion that N is finitely generated as an R-module.

• is_noetherian 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

• exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul is Nakayama's lemma, in the following form: if N is a finitely generated submodule of an ambient R-module M and I is an ideal of R such that N ⊆ IN, then there exists r ∈ 1 + I such that rN = 0.

• is_noetherian_iff_well_founded 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 ring_theory.polynomial.

## References

• [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]

## Tags

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

def submodule.fg {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
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] [ M] {N : M} :
N.fg ∃ (S : set M), S.finite = 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} [ M] (I : ideal R) (N : 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] [ M] :

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

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

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

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

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

theorem submodule.fg_prod {R : Type u_1} {M : Type u_2} [semiring R] [ M] {P : Type u_3} [ P] {sb : M} {sc : 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] [ M] [ P] (f : M →ₗ[R] P) {s : M} :
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] [ M] :
Prop
• noetherian : ∀ (s : M), s.fg

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] [ M] {N : M} :
∀ (s : M), s N → s.fg

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

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

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

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

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

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

theorem fg_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [ M] [ P] [ P] {N : 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] [ M] [ P] [ M] [ P] :
(M × 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 : ι), (M i)] [fintype ι] [∀ (i : ι), (M i)] :
(Π (i : ι), M i)

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

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

theorem finite_of_linear_independent {R : Type u_1} {M : Type u_2} [comm_ring R] [nontrivial R] [ M] [ M] {s : set M} :
→ s.finite

theorem set_has_maximal_iff_noetherian {R : Type u_1} {M : Type u_2} [ring R] [ M] :
(∀ (a : set M)), a.nonempty(∃ (M' : M) (H : M' a), ∀ (I : M), I aM' II = 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]
def is_noetherian_ring.to_is_noetherian {R : Type u_1} [ring R]  :

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

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

theorem is_noetherian_of_submodule_of_noetherian (R : Type u_1) (M : Type u_2) [ring R] [ M] (N : M) :

theorem is_noetherian_of_quotient_of_noetherian (R : Type u_1) [ring R] (M : Type u_2) [ M] (N : M) :

theorem is_noetherian_of_fg_of_noetherian {R : Type u_1} {M : Type u_2} [ring R] [ M] (N : M)  :
N.fg

theorem is_noetherian_of_fg_of_noetherian' {R : Type u_1} {M : Type u_2} [ring R] [ M]  :
.fg

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

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

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

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

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

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