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.
r one s two intersection of height one localisations
Statement
Assume the Axiom of Choice.
If is a commutative Noetherian domain satisfying , then inside its fraction field one has . For a field the empty intersection is interpreted as .
Facts & Assumptions
Given: The objects and hypotheses in the statement, including the Axiom of Choice (The Axiom of Choice); cited dependent-choice and resolution-existence hypotheses are retained.
serre r k and s k conditions: For a commutative Noetherian ring and an integer , condition means that is regular whenever . Condition means that for every prime . A finite module satisfies if for every prime in its support. Outside the support the condition is vacuous, consistent with depth of the zero module being and the empty support having no nonnegative dimension. Thus the zero module satisfies all conditions, and the zero ring satisfies both families vacuously.
Every submodule of a finite module over a Noetherian ring has a minimal primary decomposition: Assume Dependent Choice. Let be a Noetherian commutative ring and let be a finitely generated left -module. Every submodule has a finite primary decomposition. After deleting redundant components and combining equal radicals, one obtains a minimal primary decomposition. When , the decomposition is the empty intersection, interpreted as . In particular, every ideal of a Noetherian ring has a minimal primary decomposition.
The radicals in a minimal primary decomposition are exactly the associated primes of the quotient: Let be a Noetherian commutative ring, let be a finitely generated left -module, and let be a minimal primary decomposition in which each is -primary. Assume each is a prime ideal. Then
Depth drops by one after quotienting by a regular element: Let be Noetherian, let be finite, let lie in the Jacobson radical, and let be -regular. Then
The local depth-zero associated-prime criterion: Let be a Noetherian local ring and let be a finite -module. Then
Associated primes commute with localization for finite modules: Let be a Noetherian commutative ring, let be a finitely generated left -module, and let be multiplicative. Then
A nonzero module over a Noetherian ring has an associated prime: Under Dependent Choice, if is a Noetherian commutative ring and a nonzero left -module, then is nonempty.
Proof
Let be a nonunit. If , localization and the depth-zero criterion make depth zero. Since is regular, the depth formula gives . Condition forces , and , force equality.
Choose a minimal primary decomposition , with radicals . Those radicals are associated to , hence have height one. If belongs to every height-one localization, then for each there is with . Primaryness gives , hence and .
If is a unit, membership is immediate without a primary decomposition. The inclusion from into every localization is automatic. If the height-one family is empty, a nonzero nonunit would yield an associated prime of its nonzero quotient and hence a height-one prime by the preceding argument; thus is a field and the stipulated empty intersection is correct.
Depends on
- The Axiom of Choice
- serre r k and s k conditions
- Every submodule of a finite module over a Noetherian ring has a minimal primary decomposition
- The radicals in a minimal primary decomposition are exactly the associated primes of the quotient
- Depth drops by one after quotienting by a regular element
- The local depth-zero associated-prime criterion
- Associated primes commute with localization for finite modules
- A nonzero module over a Noetherian ring has an associated prime
Used by
- A Weil divisor that is not Cartier at the vertex of the quadric cone Counterexample
- The intersection product needs Cartier or complementary-dimension hypotheses Counterexample
- No derived residue map into structure cohomology of a normal surface modification Lemma
- Proper normal curve rational function map Lemma
- r one s two integral element membership Lemma
- Reduced Cartier multiples on a normal local surface Lemma
- Reflexive surface modules and codimension-one lattice extension Lemma
- The smooth locus of a normal completion of a group has only constant functions Lemma
- Under AC, the Picard-to-class-group map is injective on normal Noetherian integral schemes Lemma
- Regular functions on a normal variety are cut out in codimension one Theorem
Dependency tree · two levels
31 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
- Proposition 8.41 proof, pp.57–58; Stacks 10.157.6(1)–(2) (standard reference, not scraped)