LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

An ideal maximal among the non-finitely-generated ideals is prime

Statement

Let $R$ be a commutative ring and let $p$ be an ideal of $R$ that is maximal in the set $Σ$ of non-finitely-generated ideals of $R$ (If some ideal is not finitely generated, there is one maximal among the ideals that are not): that is, $p$ is not finitely generated, and every ideal of $R$ strictly containing $p$ is finitely generated. Then $p$ is a prime ideal (Prime ideals and maximal ideals in a commutative ring).

Facts & Assumptions

Given: A commutative ring $R$ and an ideal $p$ maximal in the set $Σ$ of ideals of $R$ that are not finitely generated (If some ideal is not finitely generated, there is one maximal among the ideals that are not). For an ideal $a$ and $a \in R$ , write $(a : a) : = {r \in R : r a \in a}$ and $a a : = {a x : x \in a}$ .

[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]

In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ ; the empty sum is included and equals $0$ (In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ ).

[L3]

For $S \subseteq R$ , $(S)$ is the intersection of all two-sided ideals containing $S$ , so $S \subseteq (S)$ ; $({a})$ is written $(a)$ (The ideal generated by a subset and principal ideals).

[L4]

For ideals $I, J$ of $R$ , the sum is $I + J = {i + j : i \in I, j \in J}$ (The sum $I + J$ and product $I J$ of two-sided ideals).

[L5]

A nonempty subset $I \subseteq R$ is a two-sided ideal exactly when it is closed under $x - y$ and under $r x, x r$ for all $r \in R$ , $x, y \in I$ (Ideal criteria and intersections of ideals).

Proof

technique · contradiction

1.1L2L3given

$p$ is a proper ideal: the unit ideal $R = (1)$ is generated by one element, so $R \notin Σ$ , whereas $p \in Σ$ .

1.2assume-contraL1given

Suppose $p$ is not prime. By the previous step it is proper, so there are $a, b \in R$ with $a b \in p$ , $a \notin p$ and $b \notin p$ .

2.1L2L3L4step 1.2

The ideal $p + (a)$ strictly contains $p$ , since $a$ lies in it and not in $p$ , so by maximality it is finitely generated. Every element of $p + (a)$ has the form $x + w a$ with $x \in p$ and $w \in R$ , because $(a) = R a$ ; so a finite generating list may be written $x_{1} + w_{1} a, \dots, x_{n} + w_{n} a$ with $x_{i} \in p$ , $w_{i} \in R$ and $n \in N$ .

2.2L2L5step 1.2

The set $q : = (p : a)$ is an ideal of $R$ : it contains $0$ , and if $r a, r^{'} a \in p$ then $(r - r^{'}) a = r a - r^{'} a \in p$ and $(s r) a = s (r a) \in p$ for every $s \in R$ . It contains $p$ , since $x a \in p$ for $x \in p$ , and it contains $b$ , since $b a = a b \in p$ ; as $b \notin p$ the containment $p \subseteq q$ is strict, so by maximality $q$ is finitely generated, say $q = (q_{1}, \dots, q_{m})$ with $m \in N$ .

3.1L2L5step 2.2

The set $a q$ is an ideal, being closed under differences and under multiplication by $R$ because $q$ is, and it is generated by $a q_{1}, \dots, a q_{m}$ : any $q \in q$ is $\sum_{j} r_{j} q_{j}$ , so $a q = \sum_{j} r_{j} (a q_{j})$ . Moreover $a q \subseteq p$ by the definition of $q$ .

3.2L2L4step 2.1step 2.2

$p = (x_{1}, \dots, x_{n}) + a q$ . The inclusion from right to left holds because each $x_{i}$ lies in $p$ and $a q \subseteq p$ . For the other inclusion take $z \in p \subseteq p + (a)$ and write $z = \sum_{i = 1}^{n} c_{i} (x_{i} + w_{i} a) = \sum_{i = 1}^{n} c_{i} x_{i} + y a$ with $c_{i} \in R$ and $y = \sum_{i = 1}^{n} c_{i} w_{i}$ ; then $y a = z - \sum_{i} c_{i} x_{i}$ lies in $p$ , so $y \in q$ and $y a \in a q$ , whence $z \in (x_{1}, \dots, x_{n}) + a q$ .

4.1L1L2L4step 1.1step 3.1step 3.2discharge-contradiction∎

Both summands are finitely generated, so $p = (x_{1}, \dots, x_{n}, a q_{1}, \dots, a q_{m})$ is finitely generated, contradicting $p \in Σ$ . The supposition of step 1.2 is therefore untenable: whenever $a b \in p$ , either $a \in p$ or $b \in p$ , and with step 1.1 this makes $p$ prime.

Remarks

Where each maximality use goes. Maximality of $p$ in $Σ$ is used exactly twice, in step 2.1 on $p + (a)$ and in step 2.2 on the colon ideal $(p : a)$ ; both are strictly larger than $p$ precisely because $a \notin p$ and $b \notin p$ .
The generators of $p + (a)$ are normalised, not merely chosen. Writing them as $x_{i} + w_{i} a$ with $x_{i} \in p$ is what lets step 3.2 separate the part of $z$ lying in $(x_{1}, \dots, x_{n})$ from the multiple of $a$ ; an unnormalised list would not split that way.
No Noetherian hypothesis anywhere. The lemma is used inside a proof whose conclusion is that the ring is Noetherian, so assuming a chain condition here would be circular.

Depends on

Used by

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

Dependency tree · two levels

14 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)