Documentation

Mathlib.RingTheory.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.

IsNoetherian 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 #

isNoetherian_iff 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 RingTheory.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

class IsNoetherian (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian 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.

noetherian : ∀ (s : Submodule R M), s.FG
IsNoetherian 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 IsNoetherian.noetherian {R : Type u_1} {M : Type u_2} :

∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M} [self : IsNoetherian R M] (s : Submodule R M), s.FG

IsNoetherian 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.

theorem isNoetherian_def {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian R M ↔ ∀ (s : Submodule R M), s.FG

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

theorem isNoetherian_submodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :

IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG

theorem isNoetherian_submodule_left {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :

IsNoetherian R ↥N ↔ ∀ (s : Submodule R M), (N ⊓ s).FG

theorem isNoetherian_submodule_right {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} :

IsNoetherian R ↥N ↔ ∀ (s : Submodule R M), (s ⊓ N).FG

instance isNoetherian_submodule' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (N : Submodule R M) :

IsNoetherian R ↥N

Equations

⋯ = ⋯

theorem isNoetherian_of_le {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s : Submodule R M} {t : Submodule R M} [ht : IsNoetherian R ↥t] (h : s ≤ t) :

IsNoetherian R ↥s

theorem isNoetherian_of_surjective {R : Type u_1} (M : Type u_2) {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] (f : M →ₗ[R] P) (hf : LinearMap.range f = ⊤) [IsNoetherian R M] :

IsNoetherian R P

instance isNoetherian_quotient {R : Type u_4} [Ring R] {M : Type u_5} [AddCommGroup M] [Module R M] (N : Submodule R M) [IsNoetherian R M] :

IsNoetherian R (M ⧸ N)

Equations

⋯ = ⋯

@[deprecated isNoetherian_quotient]

def Submodule.Quotient.isNoetherian {R : Type u_4} [Ring R] {M : Type u_5} [AddCommGroup M] [Module R M] (N : Submodule R M) [IsNoetherian R M] :

IsNoetherian R (M ⧸ N)

Alias of isNoetherian_quotient.

Equations

@Submodule.Quotient.isNoetherian = @isNoetherian_quotient

Instances For

theorem isNoetherian_of_linearEquiv {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] (f : M ≃ₗ[R] P) [IsNoetherian R M] :

IsNoetherian R P

theorem isNoetherian_top_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian R ↥⊤ ↔ IsNoetherian R M

theorem isNoetherian_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] [IsNoetherian R P] (f : M →ₗ[R] P) (hf : Function.Injective ⇑f) :

IsNoetherian R M

theorem fg_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P) (hf : Function.Injective ⇑f) :

N.FG

@[instance 100]

instance Module.IsNoetherian.finite (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] :

Module.Finite R M

Equations

⋯ = ⋯

instance Module.instFiniteSubtypeMemIdealOfIsNoetherian {R₁ : Type u_4} {S : Type u_5} [CommSemiring R₁] [Semiring S] [Algebra R₁ S] [IsNoetherian R₁ S] (I : Ideal S) :

Module.Finite R₁ ↥I

Equations

⋯ = ⋯

theorem Module.Finite.of_injective {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [IsNoetherian R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) :

Module.Finite R M

theorem isNoetherian_of_ker_bot {R : Type u_1} {M : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] [IsNoetherian R P] (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) :

IsNoetherian R M

theorem fg_of_ker_bot {R : Type u_1} {M : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) :

N.FG

instance isNoetherian_prod {R : Type u_1} {M : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] [IsNoetherian R M] [IsNoetherian R P] :

IsNoetherian R (M × P)

Equations

⋯ = ⋯

instance isNoetherian_pi {R : Type u_4} {ι : Type u_5} {M : ι → Type u_6} [Ring R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [Finite ι] [∀ (i : ι), IsNoetherian R (M i)] :

IsNoetherian R ((i : ι) → M i)

Equations

⋯ = ⋯

instance isNoetherian_pi' {R : Type u_4} {ι : Type u_5} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [Finite ι] [IsNoetherian R M] :

IsNoetherian R (ι → M)

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

Equations

⋯ = ⋯

instance isNoetherian_linearMap_pi (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] {ι : Type u_4} [Finite ι] :

IsNoetherian R ((ι → R) →ₗ[R] M)

Equations

⋯ = ⋯

instance isNoetherian_linearMap (R : Type u_1) (M : Type u_2) (N : Type u_3) [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [IsNoetherian R M] [Module.Finite R N] :

IsNoetherian R (N →ₗ[R] M)

Equations

⋯ = ⋯

theorem isNoetherian_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian R M ↔ WellFounded fun (x1 x2 : Submodule R M) => x1 > x2

theorem IsNoetherian.wf {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian R M → WellFounded fun (x1 x2 : Submodule R M) => x1 > x2

Alias of the forward direction of isNoetherian_iff.

theorem isNoetherian_iff' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian R M ↔ WellFoundedGT (Submodule R M)

theorem isNoetherian_mk {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

WellFoundedGT (Submodule R M) → IsNoetherian R M

Alias of the reverse direction of isNoetherian_iff'.

theorem IsNoetherian.wellFoundedGT {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian R M → WellFoundedGT (Submodule R M)

Alias of the forward direction of isNoetherian_iff'.

instance wellFoundedGT {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [h : IsNoetherian R M] :

WellFoundedGT (Submodule R M)

Equations

⋯ = ⋯

theorem isNoetherian_iff_fg_wellFounded {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian R M ↔ WellFoundedGT { N : Submodule R M // N.FG }

theorem set_has_maximal_iff_noetherian {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] :

(∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian 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] [AddCommMonoid M] [Module R M] :

(∀ (f : ℕ →o Submodule R M), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M

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

theorem eventuallyConst_of_isNoetherian {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (f : ℕ →o Submodule R M) :

Filter.EventuallyConst (⇑f) Filter.atTop

theorem IsNoetherian.induction {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] {P : Submodule R M → Prop} (hgt : ∀ (I : 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 Submodule.finite_ne_bot_of_independent {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] {ι : Type u_4} {N : ι → Submodule R M} (h : CompleteLattice.Independent N) :

{i : ι | N i ≠ ⊥}.Finite

theorem LinearIndependent.finite_of_isNoetherian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] [Nontrivial R] {ι : Type u_4} {v : ι → M} (hv : LinearIndependent R v) :

A linearly-independent family of vectors in a module over a non-trivial ring must be finite if the module is Noetherian.

theorem LinearIndependent.set_finite_of_isNoetherian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] [Nontrivial R] {s : Set M} (hi : LinearIndependent R Subtype.val) :

s.Finite

theorem isNoetherian_of_range_eq_ker {R : Type u_1} {M : Type u_2} {P : Type u_3} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] [IsNoetherian R M] [IsNoetherian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : LinearMap.range f = LinearMap.ker g) :

IsNoetherian R N

If the first and final modules in an exact sequence are Noetherian, then the middle module is also Noetherian.

theorem LinearMap.eventually_disjoint_ker_pow_range_pow {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) :

∀ᶠ (n : ℕ) in Filter.atTop, Disjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))

For an endomorphism of a Noetherian module, any sufficiently large iterate has disjoint kernel and range.

theorem LinearMap.eventually_iSup_ker_pow_eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) :

∀ᶠ (n : ℕ) in Filter.atTop, ⨆ (m : ℕ), LinearMap.ker (f ^ m) = LinearMap.ker (f ^ n)

theorem IsNoetherian.injective_of_surjective_of_injective {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (i : N →ₗ[R] M) (f : N →ₗ[R] M) (hi : Function.Injective ⇑i) (hf : Function.Surjective ⇑f) :

Function.Injective ⇑f

Orzech's theorem for Noetherian modules: if R is a ring (not necessarily commutative), M and N are R-modules, M is Noetherian, i : N →ₗ[R] M is injective, f : N →ₗ[R] M is surjective, then f is also injective. The proof here is adapted from Djoković's paper Epimorphisms of modules which must be isomorphisms [djokovic1973], utilizing LinearMap.iterateMapComap. See also Orzech's original paper: Onto endomorphisms are isomorphisms [orzech1971].

theorem IsNoetherian.injective_of_surjective_of_submodule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] {N : Submodule R M} (f : ↥N →ₗ[R] M) (hf : Function.Surjective ⇑f) :

Function.Injective ⇑f

Orzech's theorem for Noetherian modules: if R is a ring (not necessarily commutative), M is a Noetherian R-module, N is a submodule, f : N →ₗ[R] M is surjective, then f is also injective.

theorem IsNoetherian.injective_of_surjective_endomorphism {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) (s : Function.Surjective ⇑f) :

Function.Injective ⇑f

Any surjective endomorphism of a Noetherian module is injective.

theorem IsNoetherian.bijective_of_surjective_endomorphism {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) (s : Function.Surjective ⇑f) :

Function.Bijective ⇑f

Any surjective endomorphism of a Noetherian module is bijective.

theorem IsNoetherian.disjoint_partialSups_eventually_bot {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : ℕ → Submodule R M) (h : ∀ (n : ℕ), Disjoint ((partialSups 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.

theorem IsNoetherian.subsingleton_of_prod_injective {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (f : M × N →ₗ[R] M) (i : Function.Injective ⇑f) :

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

@[simp]

theorem IsNoetherian.equivPUnitOfProdInjective_symm_apply {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (f : M × N →ₗ[R] M) (i : Function.Injective ⇑f) :

∀ (x : PUnit.{w + 1} ), (IsNoetherian.equivPUnitOfProdInjective f i).symm x = 0

@[simp]

theorem IsNoetherian.equivPUnitOfProdInjective_apply {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (f : M × N →ₗ[R] M) (i : Function.Injective ⇑f) :

∀ (x : N), (IsNoetherian.equivPUnitOfProdInjective f i) x = 0

def IsNoetherian.equivPUnitOfProdInjective {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (f : M × N →ₗ[R] M) (i : Function.Injective ⇑f) :

N ≃ₗ[R] PUnit.{w + 1}

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

Equations

IsNoetherian.equivPUnitOfProdInjective f i = LinearEquiv.ofSubsingleton N PUnit.{?u.66 + 1}

Instances For

@[reducible, inline]

abbrev IsNoetherianRing (R : Type u_1) [Semiring R] :

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

Equations

IsNoetherianRing R = IsNoetherian R R

Instances For

theorem isNoetherianRing_iff {R : Type u_1} [Semiring R] :

IsNoetherianRing R ↔ IsNoetherian R R

theorem isNoetherianRing_iff_ideal_fg (R : Type u_1) [Semiring R] :

IsNoetherianRing R ↔ ∀ (I : Ideal R), I.FG

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

@[instance 80]

instance isNoetherian_of_finite (R : Type u_1) (M : Type u_2) [Finite M] [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian R M

Equations

⋯ = ⋯

@[instance 100]

instance isNoetherian_of_subsingleton (R : Type u_1) (M : Type u_2) [Subsingleton R] [Semiring R] [AddCommMonoid M] [Module R M] :

IsNoetherian R M

Modules over the trivial ring are Noetherian.

Equations

⋯ = ⋯

theorem isNoetherian_of_submodule_of_noetherian (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) (h : IsNoetherian R M) :

IsNoetherian R ↥N

theorem isNoetherian_of_tower (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [SMul R S] [Module S M] [Module R M] [IsScalarTower R S M] (h : IsNoetherian R M) :

IsNoetherian S M

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

theorem isNoetherian_of_fg_of_noetherian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [I : IsNoetherianRing R] (hN : N.FG) :

IsNoetherian R ↥N

instance isNoetherian_of_isNoetherianRing_of_finite (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] :

IsNoetherian R M

Equations

⋯ = ⋯

theorem isNoetherian_span_of_finite (R : Type u_1) {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] {A : Set M} (hA : A.Finite) :

IsNoetherian R ↥(Submodule.span R A)

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

theorem isNoetherianRing_of_surjective (R : Type u_1) [Ring R] (S : Type u_2) [Ring S] (f : R →+* S) (hf : Function.Surjective ⇑f) [H : IsNoetherianRing R] :

IsNoetherianRing S

instance isNoetherianRing_range {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] (f : R →+* S) [IsNoetherianRing R] :

IsNoetherianRing ↥f.range

Equations

⋯ = ⋯

theorem isNoetherianRing_of_ringEquiv (R : Type u_1) [Ring R] {S : Type u_2} [Ring S] (f : R ≃+* S) [IsNoetherianRing R] :

IsNoetherianRing S

theorem IsNoetherianRing.isNilpotent_nilradical (R : Type u_1) [CommRing R] [IsNoetherianRing R] :

IsNilpotent (nilradical R)

@[instance 100]

instance IsNoetherianRing.orzechProperty (R : Type u_1) [Ring R] [IsNoetherianRing R] :

OrzechProperty R

Any Noetherian ring satisfies Orzech property. See also IsNoetherian.injective_of_surjective_of_submodule and IsNoetherian.injective_of_surjective_of_injective.

Equations

⋯ = ⋯