TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

Cohen's criterion: a commutative ring in which every prime ideal is finitely generated is Noetherian

Statement

Let $R$ be a commutative ring in which every prime ideal (Prime ideals and maximal ideals in a commutative ring) is finitely generated. Then $R$ is Noetherian.

The proof uses Zorn's lemma through If some ideal is not finitely generated, there is one maximal among the ideals that are not, and therefore the axiom of choice. It does not use, and could not use, a maximal condition on the ideals of $R$ : that condition is part of what is being proved.

Facts & Assumptions

Given: A commutative ring $R$ in which every prime ideal is finitely generated.

[L1]

A proper ideal $P ⊊ R$ of a commutative ring is prime when $a b \in P$ implies $a \in P$ or $b \in P$ (Prime ideals and maximal ideals in a commutative ring).

[L2]

If at least one ideal of a commutative ring is not finitely generated, then the set $Σ$ of its non-finitely-generated ideals, ordered by inclusion, has a maximal element; the proof uses Zorn's lemma (If some ideal is not finitely generated, there is one maximal among the ideals that are not).

[L3]

An ideal maximal in $Σ$ is prime (An ideal maximal among the non-finitely-generated ideals is prime).

[L4]

For a commutative ring, being Noetherian is equivalent to every ideal being finitely generated (A commutative ring is Noetherian exactly when every ideal is finitely generated, exactly when its ideals satisfy the ascending chain condition, and exactly when every nonempty set of ideals has a maximal member).

Proof

technique · contradiction

1.1

Suppose $R$ is not Noetherian. By the ideal-level characterisation, some ideal of $R$ is then not finitely generated, so the set $Σ$ of non-finitely-generated ideals of $R$ is nonempty.

assume-contraL4given

2.1

Since $Σ$ is nonempty, it has a maximal element $p$ : an ideal that is not finitely generated and that no non-finitely-generated ideal strictly contains. This is where Zorn's lemma is used; no chain condition on $R$ is available, and none is invoked.

L2step 1.1

3.1

That maximal element is a prime ideal of $R$ .

L3step 2.1

4.1

By hypothesis every prime ideal of $R$ is finitely generated, so $p$ is finitely generated, contradicting $p \in Σ$ . The supposition of step 1.1 fails: every ideal of $R$ is finitely generated, and $R$ is Noetherian.

L1L4step 1.1step 3.1discharge-contradiction∎

Remarks

The hypothesis is about primes only, and that is the whole point. Checking finite generation of every ideal is the definition; checking it on primes is a strictly smaller task, and Cohen's criterion says the smaller task suffices.
The maximal element does not come from Noetherian induction. Noetherian induction: a property that passes to an ideal whenever it holds for every strictly larger ideal holds for every ideal and the maximal condition of A commutative ring is Noetherian exactly when every ideal is finitely generated, exactly when its ideals satisfy the ascending chain condition, and exactly when every nonempty set of ideals has a maximal member both presuppose the conclusion here. The element is produced by Zorn's lemma applied to a poset of ideals in a ring assumed not to satisfy any chain condition.
A prime ideal of the ring, not a maximal one. An ideal maximal among the non-finitely-generated ideals is prime produces primeness, not maximality among proper ideals, and the hypothesis is applied to primes accordingly.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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., (16.10) (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, v4.03, §3 (standard reference, not scraped)