TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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

Assume the Axiom of Choice. 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$ , a finitely generated left $R$ -module $M$ , and the Axiom of Choice (The Axiom of Choice), hence dependent choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

[L1]

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

[L2]

Under dependent choice, 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.1given

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

2.1L1L2step 1.1givenconstruct

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], [L2] gives a maximal member $N$ of $Σ$ . This use of the maximal condition spends DC, supplied by the assumed AC; AC also supplies the choice assumptions of the associated-prime input in the next step.

3.1L3L4L5step 2.1choosealgebra

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

4.1step 1.1step 3.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.

Finite modules over Noetherian rings admit prime filtrations

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources