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.
Two minimal decompositions of share radicals but not the embedded component
Example
Assume the Axiom of Choice (The Axiom of Choice), and let be a field.
In ,
The radical set is the same in both decompositions, but the embedded -primary component changes.
Facts & Assumptions
Given: The Axiom of Choice, a field , the polynomial ring , and the ideal .
Over a Noetherian commutative ring, for a finitely generated module and a minimal primary decomposition whose component radicals are prime, the radical set depends only on the quotient (The radicals in a minimal primary decomposition are intrinsic).
Assuming the Axiom of Choice, an isolated primary component with prime radical in the Noetherian finite-module setting is recovered by localization and contraction (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 ).
Verification
The inclusion is immediate, and every element of the right side has the form with , so . Likewise , and if then for some . The right-hand side lies in , so ; thus and . Hence .
The field is Noetherian because its only ideals are and , so [L3] makes Noetherian. The ideal is prime because . The quotients and are local rings with square-zero maximal ideals, so and are -primary. Both decompositions are irredundant: lies in neither nor , while and . Hence both displayed decompositions are minimal primary decompositions with prime radicals and .
Fact [L1] now predicts exactly the common radical set from step 2.1. The second component differs: one decomposition uses , the other uses .
Localizing at the minimal prime kills the -primary component in either decomposition, so [L2] recovers the same isolated component from both. The difference therefore lies only in the embedded component.
This is the standard warning that first uniqueness does not imply componentwise uniqueness of embedded pieces.
Depends on
Used by
Nothing in the library uses this result yet.
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., Examples (18.14)-(18.15) (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, §19 (standard reference, not scraped)