TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite modules over Noetherian rings admit prime filtrations

Statement

Let $R$ be a Noetherian commutative ring and let $M$ be a finitely generated left $R$ -module. Then there exist submodules

0 = M_{0} \subset M_{1} \subset \dots \subset M_{n} = M

such that each quotient $M_{i} / M_{i - 1}$ is isomorphic to $R / p_{i}$ for some prime ideal $p_{i}$ of $R$ . When $M = 0$ , this is the empty filtration with $n = 0$ .

Facts & Assumptions

Given: A Noetherian commutative ring $R$ and a finitely generated left $R$ -module $M$ .

[L1]

A finitely generated module over a Noetherian ring is Noetherian (Finitely generated modules over a left Noetherian ring are Noetherian).

[L2]

In a Noetherian module, every nonempty family of submodules has a maximal member (Finite generation, ACC, and maximal-condition characterizations of Noetherian modules).

[L3]

Every nonzero module over a Noetherian ring has an associated prime (A nonzero module over a Noetherian ring has an associated prime).

[L4]

If $p$ is associated to a module, then $R / p$ embeds in that module (Associated primes are exactly primes of embedded cyclic residue modules).

[L5]

Quotient modules are formed from cosets $M / N$ (Quotient module $M / N$ with scalar multiplication on additive cosets).

Proof

technique · direct

1.1

If $M = 0$ , then the empty chain $0 = M$ is already a prime filtration.

given

2.1

Assume $M \neq 0$ . Let $Σ = {N \leq M : N admits a prime filtration} .$ By step 1.1, the zero submodule belongs to $Σ$ . Since $M$ is Noetherian by [L1], fact [L2] gives a maximal member $N$ of $Σ$ .

L1L2step 1.1construct

3.1

If $N \neq M$ , then $M / N$ is a nonzero quotient module by [L5]. Fact [L3] gives an associated prime $p$ of $M / N$ , and [L4] yields an embedded copy of $R / p$ in $M / N$ . Let $N^{'}$ be its preimage in $M$ . Then $N ⊊ N^{'} \leq M$ and $N^{'} / N ≅ R / p$ . Appending $N^{'}$ to a prime filtration of $N$ gives a prime filtration of $N^{'}$ , contradicting the maximality of $N$ in step 2.1. Therefore $N = M$ .

L3L4L5step 2.1choosealgebra

4.1

When $M \neq 0$ , step 3.1 shows that $M$ itself has a prime filtration; the zero case was handled in step 1.1.

step 1.1step 3.1∎

Depends on

Used by

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Lemma (17.20) (standard reference, not scraped)
The Stacks Project, Lemma 10.62.1 (standard reference, not scraped)