Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01
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.

Choose the first generator's minimal prime inside the target prime

Statement

Let R be a Noetherian commutative ring, let n2, let

I=(x1,,xn),

and let p be a prime ideal minimal over I. Let p1,,pr be the minimal prime ideals over (x2,,xn). If p is not one of the pi and if

p=pdpd1p0

is a strict prime chain, then there exists a strict prime chain of the same length ending at p whose first proper subprime p1 is not contained in any pi. For such a chain one can choose

bp1i=1rpi,

and then p is minimal over (b,x2,,xn).

Facts & Assumptions

Given: A Noetherian commutative ring R, an integer n2, the ideal I=(x1,,xn), a prime ideal p minimal over I, the minimal primes p1,,pr over (x2,,xn), and a strict chain p=pdp0.

[L1]

A Noetherian ring has finitely many minimal primes over any ideal (A Noetherian ring has finitely many minimal prime ideals, Minimal primes over a proper ideal exist).

[L2]

Finite prime avoidance lets us choose an element outside a finite union of prime ideals once the ambient ideal is not contained in that union (An ideal contained in a finite union of prime ideals lies in one of them).

[L3]

Every prime minimal over a principal ideal has height at most 1 (Krull's principal ideal theorem).

Proof

technique · direct
1.1

By [L1], the family {p1,,pr} is finite. Repeatedly applying the two-step prime-avoidance argument to the triples ppjpj1 for 1jd1 produces a strict chain of the same length ending at p whose first proper subprime is not contained in any pi. Relabel so that the resulting chain is again p=pdpd1p0 with p1pi for every i.

L1L2L3given
2.1

Since p1 is not contained in the finite union ipi, [L2] gives bp1ipi. In particular bp, so p contains (b,x2,,xn).

L2step 1.1
3.1

Let qp be prime minimal over (b,x2,,xn). Because q contains (x2,,xn), it contains one of the minimal primes pi. By the choice of b, one has bpi, so qpi. If qp, then pqpi is a strict chain in the quotient ring R/(x2,,xn), so the prime p/(x2,,xn) has height at least 2. But p is minimal over (x1,,xn), hence p/(x2,,xn) is minimal over the principal ideal generated by the image of x1, contradicting [L3]. Therefore q=p.

L3step 2.1given
4.1

Hence p is minimal over (b,x2,,xn), with b chosen from the first proper subprime of a chain of the same length.

step 3.1

Depends on

Used by

Dependency tree · two levels

12 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