Theorems · Theorem · commutative algebra

IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime

∀ (A : Type u) [inst : CommRing A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M] [IsNoetherianRing A]
  [Module.Finite A M], ∃ s, 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.

Defined in

Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleIsNoetherianRingModule.Finite