mathlib documentation

ring_theory.noetherian

Noetherian rings and modules #

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

Every increasing chain of submodules M₁ ⊆ M₂ ⊆ M₃ ⊆ ⋯ eventually stabilises.
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.

submodule.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]
[samuel1967]

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] [module 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

N.fg = ∃ (S : finset M), submodule.span R ↑S = N

theorem submodule.fg_def {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {N : submodule R M} :

N.fg ↔ ∃ (S : set M), S.finite ∧ submodule.span R S = N

theorem submodule.fg_iff_add_submonoid_fg {M : Type u_2} [add_comm_monoid M] (P : submodule ℕ M) :

P.fg ↔ P.to_add_submonoid.fg

theorem submodule.fg_iff_add_subgroup_fg {G : Type u_1} [add_comm_group G] (P : submodule ℤ G) :

P.fg ↔ P.to_add_subgroup.fg

theorem submodule.fg_iff_exists_fin_generating_family {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {N : submodule R M} :

N.fg ↔ ∃ (n : ℕ) (s : fin n → M), submodule.span R (set.range 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 ∈ N → r • 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] [module R M] :

theorem subalgebra.fg_bot_to_submodule {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :

⊥.to_submodule.fg

theorem submodule.fg_span {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {s : set M} (hs : s.finite) :

(submodule.span R s).fg

theorem submodule.fg_span_singleton {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (x : M) :

(submodule.span R {x}).fg

theorem submodule.fg_sup {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module 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] [module R M] {P : Type u_3} [add_comm_monoid P] [module R P] (f : M →ₗ[R] P) {N : submodule R M} (hs : N.fg) :

(submodule.map f N).fg

theorem submodule.fg_of_fg_map_injective {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {P : Type u_3} [add_comm_monoid P] [module R P] (f : M →ₗ[R] P) (hf : function.injective ⇑f) {N : submodule R M} (hfn : (submodule.map f N).fg) :

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} [semiring R] [add_comm_monoid M] [module R M] (N : submodule R M) :

⊤.fg ↔ N.fg

theorem submodule.fg_of_linear_equiv {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {P : Type u_3} [add_comm_monoid P] [module 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] [module R M] {P : Type u_3} [add_comm_monoid P] [module R P] {sb : submodule R M} {sc : submodule R P} (hsb : sb.fg) (hsc : sc.fg) :

(sb.prod sc).fg

theorem submodule.fg_pi {R : Type u_1} [semiring R] {ι : Type u_2} {M : ι → Type u_3} [fintype ι] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] {p : Π (i : ι), submodule R (M i)} (hsb : ∀ (i : ι), (p i).fg) :

(submodule.pi set.univ p).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.

def ideal.fg {R : Type u_1} [semiring R] (I : ideal R) :

Prop

An ideal of R is finitely generated if it is the span of a finite subset of R.

This is defeq to submodule.fg, but unfolds more nicely.

Equations

I.fg = ∃ (S : finset R), ideal.span ↑S = I

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

(ideal.map f I).fg

The image of a finitely generated ideal is finitely generated.

This is the ideal version of submodule.fg.map.

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

(submodule.restrict_scalars R N).fg

theorem ideal.fg_ker_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 : f.ker.fg) (hg : g.ker.fg) (hsur : function.surjective ⇑f) :

(g.comp f).ker.fg

theorem submodule.fg_iff_compact {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] (s : submodule R M) :

s.fg ↔ complete_lattice.is_compact_element s

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] [module R M] :

Prop

noetherian : ∀ (s : submodule R 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_def {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :

is_noetherian R M ↔ ∀ (s : submodule R M), s.fg

An R-module is Noetherian iff all its submodules are finitely-generated.

theorem is_noetherian_submodule {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid 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} [semiring R] [add_comm_monoid 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} [semiring R] [add_comm_monoid M] [module R M] {N : submodule R M} :

is_noetherian R ↥N ↔ ∀ (s : submodule R M), (s ⊓ N).fg

@[protected, instance]

def is_noetherian_submodule' {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] [is_noetherian R M] (N : submodule R M) :

is_noetherian R ↥N

theorem is_noetherian_of_le {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] {s t : submodule R M} [ht : is_noetherian R ↥t] (h : s ≤ t) :

is_noetherian R ↥s

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

is_noetherian R P

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

is_noetherian R P

theorem is_noetherian_top_iff {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :

is_noetherian R ↥⊤ ↔ is_noetherian R M

theorem is_noetherian_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [semiring R] [add_comm_monoid M] [add_comm_monoid P] [module R M] [module R P] [is_noetherian R P] (f : M →ₗ[R] P) (hf : function.injective ⇑f) :

is_noetherian R M

theorem fg_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [semiring R] [add_comm_monoid M] [add_comm_monoid P] [module R M] [module R P] [is_noetherian R P] {N : submodule R M} (f : M →ₗ[R] P) (hf : function.injective ⇑f) :

N.fg

theorem is_noetherian_of_ker_bot {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 = ⊥) :

is_noetherian R M

theorem fg_of_ker_bot {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

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

is_noetherian R (M × P)

@[protected, 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)

@[protected, instance]

def is_noetherian_pi' {R : Type u_1} {ι : Type u_2} {M : Type u_3} [ring R] [add_comm_group M] [module R M] [fintype ι] [is_noetherian R M] :

is_noetherian R (ι → M)

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

theorem is_noetherian_iff_well_founded {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :

is_noetherian R M ↔ well_founded gt

theorem well_founded_submodule_gt (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [module R M] [is_noetherian R M] :

well_founded gt

theorem set_has_maximal_iff_noetherian {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :

(∀ (a : set (submodule R M)), a.nonempty → (∃ (M' : submodule R M) (H : M' ∈ a), ∀ (I : submodule R M), I ∈ a → M' ≤ I → I = M')) ↔ is_noetherian R M

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

theorem monotone_stabilizes_iff_noetherian {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] :

(∀ (f : ℕ →o submodule R M), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ⇑f n = ⇑f m) ↔ is_noetherian R M

A module is Noetherian iff every increasing chain of submodules stabilizes.

theorem is_noetherian.induction {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] [is_noetherian R M] {P : submodule R M → Prop} (hgt : ∀ (I : submodule R M), (∀ (J : 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 finite_of_linear_independent {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [nontrivial R] [is_noetherian R M] {s : set M} (hs : linear_independent R coe) :

theorem is_noetherian_of_range_eq_ker {R : Type u_1} {M : Type u_2} {P : Type u_3} {N : Type w} [ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [add_comm_group P] [module R P] [is_noetherian R M] [is_noetherian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf : function.injective ⇑f) (hg : function.surjective ⇑g) (h : f.range = g.ker) :

is_noetherian R N

If the first and final modules in a short exact sequence are noetherian, then the middle module is also noetherian.

theorem is_noetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [I : is_noetherian R M] (f : M →ₗ[R] M) :

∃ (n : ℕ), n ≠ 0 ∧ (f ^ n).ker ⊓ (f ^ n).range = ⊥

For any endomorphism of a Noetherian module, there is some nontrivial iterate with disjoint kernel and range.

theorem is_noetherian.injective_of_surjective_endomorphism {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_noetherian R M] (f : M →ₗ[R] M) (s : function.surjective ⇑f) :

function.injective ⇑f

Any surjective endomorphism of a Noetherian module is injective.

theorem is_noetherian.bijective_of_surjective_endomorphism {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_noetherian R M] (f : M →ₗ[R] M) (s : function.surjective ⇑f) :

function.bijective ⇑f

Any surjective endomorphism of a Noetherian module is bijective.

theorem is_noetherian.disjoint_partial_sups_eventually_bot {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [I : is_noetherian R M] (f : ℕ → submodule R M) (h : ∀ (n : ℕ), disjoint (⇑(partial_sups 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.

noncomputable def is_noetherian.equiv_punit_of_prod_injective {R : Type u_1} {M : Type u_2} {N : Type w} [ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] [is_noetherian R M] (f : M × N →ₗ[R] M) (i : function.injective ⇑f) :

N ≃ₗ[R] punit

If M ⊕ N embeds into M, for M noetherian over R, then N is trivial.

Equations

is_noetherian.equiv_punit_of_prod_injective f i = nonempty.some _

@[class]

structure is_noetherian_ring (R : Type u_1) [semiring R] :

Prop

to_is_noetherian : is_noetherian R R

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

Instances

theorem is_noetherian_ring_iff {R : Type u_1} [semiring R] :

is_noetherian_ring R ↔ is_noetherian R R

theorem is_noetherian_ring_iff_ideal_fg (R : Type u_1) [comm_semiring R] :

is_noetherian_ring R ↔ ∀ (I : ideal R), I.fg

A commutative ring is Noetherian if and only if all its ideals are finitely-generated.

@[protected, instance]

def ring.is_noetherian_of_fintype (R : Type u_1) (M : Type u_2) [fintype M] [semiring R] [add_comm_monoid M] [module R M] :

is_noetherian R M

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

is_noetherian_ring R

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

is_noetherian R ↥N

@[protected, instance]

def submodule.quotient.is_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] :

is_noetherian R (M ⧸ N)

theorem is_noetherian_of_tower (R : Type u_1) {S : Type u_2} {M : Type u_3} [semiring R] [semiring S] [add_comm_monoid M] [has_scalar R S] [module S M] [module R M] [is_scalar_tower R S M] (h : is_noetherian R M) :

is_noetherian S M

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

@[protected, instance]

def ideal.quotient.is_noetherian_ring {R : Type u_1} [comm_ring R] [h : is_noetherian_ring R] (I : ideal R) :

is_noetherian_ring (R ⧸ I)

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

is_noetherian R ↥N

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

is_noetherian R M

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

is_noetherian R ↥(submodule.span R 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] :

is_noetherian_ring S

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

is_noetherian_ring ↥(f.range)

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

is_noetherian_ring S

theorem submodule.fg_mul {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring 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_semiring R] [semiring A] [algebra R A] (M : submodule R A) (h : M.fg) (n : ℕ) :

(M ^ n).fg