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.
normal domain implies s two
Statement
Assume the Axiom of Choice (The Axiom of Choice). Every commutative Noetherian integrally closed domain satisfies .
Facts & Assumptions
Given: The objects and hypotheses in the statement. The Axiom of Choice is assumed; 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.
A domain is integrally closed if and only if its prime localisations are, equivalently if and only if its maximal localisations are: Assume the Axiom of Choice. Let be a domain. Then the following are equivalent: 1. is integrally closed. 2. For every prime ideal of , the localisation is integrally closed. 3. For every maximal ideal of , the localisation is integrally closed.
The local depth-zero associated-prime criterion: Let be a Noetherian local ring and let be a finite -module. 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
Krull's height theorem: Let be a Noetherian commutative ring, let be an ideal generated by elements, and let be a prime ideal minimal over . Then .
Proof
Localize at any prime. The resulting ring is again an integrally closed domain. In dimension zero it is a field and the required bound is zero; in positive dimension a nonzero element of the maximal ideal is a nonzerodivisor, so its depth is at least one. It remains to consider .
If such an had depth one, choose . The regular-element depth formula and the depth-zero criterion supply with . Put . Then .
If , take finite generators of the nonzero ideal and write with . The adjugate identity for gives for all . Some in a domain, hence . This is a monic equation for , contradicting integral closedness.
Otherwise there exists with a unit. For every , belongs to , so . The height theorem with one generator gives , again impossible. Therefore depth is at least two at every prime of height at least two; with the low-dimensional cases this is .
Depends on
- The Axiom of Choice
- serre r k and s k conditions
- A domain is integrally closed if and only if its prime localisations are, equivalently if and only if its maximal localisations are
- The local depth-zero associated-prime criterion
- Depth drops by one after quotienting by a regular element
- Krull's height theorem
Used by
- serre normality criterion two directions Corollary
- 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
- A nonsingular formal arc on a normal Noetherian surface becomes regular Lemma
- A normal Noetherian domain is the intersection of its height-one localizations Lemma
- Completed local degrees of finite normal surface covers Lemma
- Dimension and cohomology of local normal surface modifications Lemma
- Dualizing modules and trace pairing for normal projective surface modifications Lemma
- Nilpotent-orbit tensor covariants extend and polarize Lemma
- No derived residue map into structure cohomology of a normal surface modification Lemma
- Normality and fibre cohomology of a rational surface point blowup Lemma
- Positive conormal degree for a fibre divisor on a normal surface Lemma
- Proper normal curve rational function map Lemma
- Reduced Cartier multiples on a normal local surface Lemma
- Surface finite type normalization finite 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
25 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
- Lemma 8.40 proof, pp.56–57 (normal hypothesis required); 8.41 (standard reference, not scraped)