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.
Localizing keeps only the matching component
Example
Assume the Axiom of Choice (The Axiom of Choice), and let be a field.
In ,
Localizing at kills the -primary component, while localizing at preserves both components.
Facts & Assumptions
Given: The Axiom of Choice, a field , the polynomial ring , and the decomposition .
Assuming the Axiom of Choice, over a Noetherian commutative ring and in a finitely generated module, localizing a primary component away from its radical preserves it, while localizing at a multiplicative set meeting its radical turns it into the whole localized module (Localisation of a primary submodule either stays primary or becomes the whole module).
Assuming the Axiom of Choice, an isolated primary component with prime radical in the Noetherian finite-module setting is recovered by localizing at its prime and contracting back (Isolated primary components are recovered by localization and contraction).
A polynomial ring in finitely many variables over a Noetherian commutative ring is Noetherian (If is Noetherian then is Noetherian for every ).
A polynomial ring in finitely many variables over an integral domain is an integral domain (A polynomial ring in finitely many indeterminates over an integral domain is an integral domain).
For a commutative ring and an ideal , the quotient is an integral domain if and only if is prime ( is an integral domain if and only if is a prime ideal).
A proper ideal is -primary when every zero divisor on acts nilpotently and (Primary submodules and primary ideals).
A primary decomposition is minimal exactly when no component is redundant and the component radicals are pairwise distinct; an isolated component has a radical minimal among those radicals (Primary decompositions, minimality, and isolated components).
Verification
The field is Noetherian because its only ideals are and , so [L3] makes Noetherian. As an -module, is finitely generated by . The inclusion is immediate. Conversely, every element of has the form with , hence lies in . So .
Since a field is an integral domain, [L4] makes an integral domain, so [L5] makes prime. If multiplication by a class on the domain has nontrivial kernel, then ; hence that multiplication is zero and therefore nilpotent. Also , whose radical is . Thus [L6] shows that is -primary.
Put . Every class in has the form . If , this class is a unit, with inverse because . Therefore every zero divisor lies in and is square-zero, so every zero divisor on acts nilpotently. Moreover and : every element of has square in , while forces the constant term of to vanish. Finally, is a domain, so [L5] makes prime. Thus [L6] shows that is -primary.
The two prime radicals and are distinct, with . The decomposition from step 1.1 is irredundant: , so the component is not redundant, while , so the component is not redundant. By [L7], the displayed primary decomposition is minimal, and its -primary component is isolated because is the smaller of the two radicals.
At the prime , the element becomes a unit. Since , fact [L1] and steps 1.1–2.1 give , while survives. Hence Since step 2.1 proves that is the isolated component of a minimal primary decomposition, fact [L2] says it contracts back to .
At the maximal ideal , neither prime radical meets the denominator set, so [L1] and steps 1.1–2.1 preserve both primary components. Thus the whole decomposition survives in .
This computation shows concretely how localization removes exactly the components whose radicals meet the denominator set.
Depends on
- The Axiom of Choice
- Primary submodules and primary ideals
- Primary decompositions, minimality, and isolated components
- If $R$ is Noetherian then $R[x_1,\ldots,x_n]$ is Noetherian for every $n\in\mathbb N$
- A polynomial ring in finitely many indeterminates over an integral domain is an integral domain
- $R/P$ is an integral domain if and only if $P$ is a prime ideal
- Localisation of a primary submodule either stays primary or becomes the whole module
- Isolated primary components are recovered by localization and contraction
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
28 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., Example (18.16) (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, §19 (standard reference, not scraped)