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.
Finite modules over Noetherian rings have finitely many associated primes
Statement
Assume the Axiom of Choice.
Let be a Noetherian commutative ring and let be a finitely generated left -module. Then is a finite set.
Facts & Assumptions
Given: The Axiom of Choice, a Noetherian commutative ring and a finitely generated left -module (The Axiom of Choice).
Under the stated Axiom of Choice, the module admits a prime filtration with (Finite modules over Noetherian rings admit prime filtrations).
In a short exact sequence, associated primes of the middle term are contained in the union of those of the outer terms (Associated primes in a short exact sequence).
Proof
Choose a prime filtration as in [L1]. If , then and , which is finite.
Assume . Applying [L2] to gives Since , the class of has annihilator , so . Repeating this argument down the filtration yields
The right-hand side of step 1.2 is finite, so is finite.
Depends on
Used by
- A Hilbert polynomial bounds regularity independently of ambient dimension Lemma
- A regular element exists by prime avoidance Lemma
- Depth from first nonzero Koszul cohomology Lemma
- Fibre-regular hypersurface cuts preserve flatness and produce finite image slices Lemma
- positive depth ring has regular minimal generator Lemma
- Reduced Cartier multiples on a normal local surface Lemma
- Regular hyperplane step for coherent support induction Lemma
- Regularity gives generation, multiplication, and vanishing Lemma
- Surface finite type normalization finite Lemma
- Uniform regularity for all quotients with a fixed Hilbert polynomial Lemma
- Finite étale covers extend across the closed point of a regular local ring Theorem
- Zero divisors on a module over a Noetherian ring are the union of its associated primes Theorem
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
- A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem (17.21) (standard reference, not scraped)
- The Stacks Project, Lemma 10.63.5 (standard reference, not scraped)