Finitely generated module over Noetherian ring have finitely many associated primes.

In this file we proved that any finitely generated module over a Noetherian ring have finitely many associated primes.

Main results

• IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime: If A is a Noetherian ring and M is a finitely generated A-module, then there exists a chain of submodules 0 = M₀ ≤ M₁ ≤ M₂ ≤ ... ≤ Mₙ = M of M, such that for each 0 ≤ i < n, Mᵢ₊₁ / Mᵢ is isomorphic to A / pᵢ for some prime ideal pᵢ of A.

• IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime: If a property on finitely generated modules over a Noetherian ring satisfies that:

  • it holds for zero module,
  • it holds for any module isomorphic to some A ⧸ p where p is a prime ideal of A,
  • it is stable by short exact sequences,

  then the property holds for every finitely generated modules.

• associatedPrimes.finite: There are only finitely many associated primes of a finitely generated module over a Noetherian ring.

def Submodule.IsQuotientEquivQuotientPrime {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] (N₁ N₂ : Submodule A M) : Prop

A Prop asserting that two submodules N₁, N₂ satisfy N₁ ≤ N₂ and N₂ / N₁ is isomorphic to A / p for some prime ideal p of A.

Equations

• N₁.IsQuotientEquivQuotientPrime N₂ = (N₁ ≤ N₂ ∧ ∃ (p : PrimeSpectrum A), Nonempty ((↥N₂ ⧸ N₁.submoduleOf N₂) ≃ₗ[A] A ⧸ p.asIdeal))

theorem Submodule.isQuotientEquivQuotientPrime_iff {A : Type u} [CommRing A] {M : Type v} [AddCommGroup M] [Module A M] {N₁ N₂ : Submodule A M} : N₁.IsQuotientEquivQuotientPrime N₂ ↔ ∃ (x : M), Ideal.IsPrime (LinearMap.ker (LinearMap.toSpanSingleton A (M ⧸ N₁) (N₁.mkQ x))) ∧ N₂ = N₁ ⊔ A ∙ x

theorem IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] [IsNoetherianRing A] [Module.Finite A M] : ∃ (s : RelSeries {(N₁, N₂) : Submodule A M × Submodule A M | N₁.IsQuotientEquivQuotientPrime N₂}), s.head = ⊥ ∧ s.last = ⊤

If A is a Noetherian ring and M is a finitely generated A-module, then there exists a chain of submodules 0 = M₀ ≤ M₁ ≤ M₂ ≤ ... ≤ Mₙ = M of M, such that for each 0 ≤ i < n, Mᵢ₊₁ / Mᵢ is isomorphic to A / pᵢ for some prime ideal pᵢ of A.

theorem IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime (A : Type u) [CommRing A] [IsNoetherianRing A] ⦃M : Type v⦄ [AddCommGroup M] [Module A M] (x✝ : Module.Finite A M) {motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop} (subsingleton : ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N) (quotient : ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A) (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N) (exact : ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v) [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v) [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃), Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂) : motive M

If a property on finitely generated modules over a Noetherian ring satisfies that:

• it holds for zero module (it's formalized as it holds for any module which is subsingleton),
• it holds for A ⧸ p for every prime ideal p of A (to avoid universe problem, it's formalized as it holds for any module isomorphic to A ⧸ p),
• it is stable by short exact sequences,

then the property holds for every finitely generated modules.

NOTE: This should be the induction principle for M, but due to the bug https://github.com/leanprover/lean4/issues/4246 currently it is induction for Module.Finite A M.

theorem associatedPrimes.finite (A : Type u) [CommRing A] (M : Type v) [AddCommGroup M] [Module A M] [IsNoetherianRing A] [Module.Finite A M] : (associatedPrimes A M).Finite

There are only finitely many associated primes of a finitely generated module over a Noetherian ring.

theorem Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRing (A : Type u) [CommRing A] [IsNoetherianRing A] [IsFractionRing A A] (I : Ideal A) [hI : I.IsMaximal] : I ∈ associatedPrimes A A

Every maximal ideal of a commutative Noetherian total ring of fractions A is an associated prime of the A-module A.

instance instFiniteMaximalSpectrumOfIsFractionRing (A : Type u) [CommRing A] [IsNoetherianRing A] [IsFractionRing A A] : Finite (MaximalSpectrum A)

A commutative Noetherian total ring of fractions is semilocal.

theorem Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors {A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A} (h : Disjoint ↑I ↑(nonZeroDivisors A)) : ⊥ < Module.annihilator A ↥I

An ideal consisting of zero divisors in a commutative Noetherian ring is annihilated by some nonzero element. This is not true in general for finitely generated modules in commutative rings, see https://math.stackexchange.com/q/1189814 and http://dx.doi.org/10.2140/pjm.1979.83.375 (keywords: Property (A), Quentel's Condition (C)).

It is also not true that every finitely generated module over every commutative Noetherian ring is annihilated by some nonzero element if each element is annihilated by some nonzero element, see https://math.stackexchange.com/a/3187153.

theorem Ideal.nonempty_inter_nonZeroDivisors_of_faithfulSMul {A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A} [FaithfulSMul A ↥I] : (↑I ∩ ↑(nonZeroDivisors A)).Nonempty