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₁ ⊔ span 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 Submodule.IsQuotientEquivQuotientPrime), 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.

Stacks Tag 00L0

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.

Stacks Tag 00LC