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.
is an integral domain if and only if is a prime ideal
Statement
is an integral domain if and only if is a prime ideal.
Here is commutative and is an ideal.
Facts & Assumptions
Given: A commutative ring and a two-sided ideal .
A prime ideal is proper and satisfies or (Prime ideals and maximal ideals in a commutative ring).
Products in are (For a two-sided ideal , the additive cosets form a ring with identity ).
An integral domain is a nonzero commutative ring without zero divisors (Zero divisor, and integral domain: a commutative ring with and no zero divisors).
The canonical projection has kernel ; equivalently, exactly when (The canonical projection is a surjective ring homomorphism with kernel ).
Proof
If is prime, then is proper, so by [L4]; and gives , hence or , while commutativity of makes the quotient commutative.
If is a domain and , then , so [L3] and [L4] give or ; its nonzero identity gives , hence .
These implications prove the equivalence.
Depends on
- Prime ideals and maximal ideals in a commutative ring
- For a two-sided ideal $I$, the additive cosets form a ring $R/I$ with identity $1+I$
- Zero divisor, and integral domain: a commutative ring with $1 \ne 0$ and no zero divisors
- The canonical projection $R\to R/I$ is a surjective ring homomorphism with kernel $I$
Used by
- Every maximal ideal of a commutative ring is prime Corollary
- Rₚ/pRₚcongFrac(R/p) is the residue field at p Corollary
- Under an integral extension, a prime is maximal if and only if its contraction is maximal Corollary
- The generic point of the affine line has no relative k-valued coordinate Counterexample
- Localizing (x²,xy)=(x)∩(x,y)² keeps only the matching component Example
- Spec Z has one generic point and closed prime-number points Example
- The prime ideals of a field and of the integers Example
- The ring (ℤ/2)^ℕ is zero-dimensional but not Noetherian Example
- ℤ₍ₚ₎ consists of rationals with denominator not divisible by p, has maximal ideal pℤ₍ₚ₎, and residue field Fₚ Example
- A prime chain in R extends to a longer chain in R[x] Lemma
- Only one saturated step can lie over a fixed contracted prime in R[x] Lemma
- Reduce the principal ideal theorem to a Noetherian local domain Lemma
- A classical affine variety has a domain as its coordinate ring, and conversely Theorem
- A classical affine variety has a domain coordinate ring, and conversely Theorem
- Every prime ideal of an Artinian ring is maximal Theorem
- Lying over for integral ring maps Theorem
- The dimension formula for affine domains Theorem
Dependency tree · two levels
16 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
- Ernst, An Inquiry-Based Approach to Abstract Algebra, Maximal and Prime Ideals (standard reference, not scraped)