Alphabeta MathHow 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.
A nonzero module over a Noetherian ring has an associated prime
Statement
Assume Dependent Choice.
Let be a Noetherian commutative ring and let be a nonzero left -module. Then is nonempty.
Facts & Assumptions
Given: Dependent Choice, a Noetherian commutative ring and a nonzero left -module (The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain).
A prime ideal belongs to exactly when it is the annihilator of some element of (Associated primes of a module).
Under Dependent Choice, some nonzero element of has annihilator maximal among annihilators of nonzero elements (A nonzero module over a Noetherian ring has a maximal element annihilator).
An annihilator maximal among annihilators of nonzero elements is prime (A maximal element annihilator is prime).
Proof
By [L2], choose with such that is maximal among the annihilators of nonzero elements of . Then [L3] shows that is prime.
By [L1], the prime ideal belongs to .
Therefore is nonempty.
Depends on
Used by
- A module over a Noetherian ring has no associated primes exactly when it is zero Corollary
- A normal Noetherian domain is the intersection of its height-one localizations Lemma
- A zero divisor is contained in an associated prime Lemma
- An S-rational map defined after a faithfully flat smooth base change is defined Lemma
- Associated-prime localizations detect elements and have depth zero Lemma
- Projective weak models and rational mapping Lemma
- r one s two intersection of height one localisations Lemma
- serre r zero s one characterises reducedness Lemma
- The radicals in a minimal primary decomposition are exactly the associated primes of the quotient Lemma
- Finite modules over Noetherian rings admit prime filtrations Theorem
Dependency tree · two levels
13 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., Proposition (17.13) (standard reference, not scraped)
- The Stacks Project, Lemma 10.63.7 (standard reference, not scraped)