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.
The Krull intersection is the -torsion submodule, and it vanishes in the Jacobson-radical case
Statement
The first clause below is choice-free; the second uses the published Jacobson-radical unit criterion and therefore inherits its Axiom-of-Choice boundary.
Let be a Noetherian commutative ring, let be an ideal, and let be a finite -module. Put
Then:
- is exactly the set of elements for which for some ;
- if , then .
Facts & Assumptions
Given: A Noetherian commutative ring , an ideal , a finite -module , and .
Artin-Rees applies to the submodule (Artin-Rees controls intersections of submodules with high ideal powers).
If a finite module satisfies , then for some (Determinant trick for Nakayama).
Assuming the Axiom of Choice, exactly when is a unit for every (Assuming the Axiom of Choice, an element lies in the Jacobson radical exactly when one minus any multiple is a unit).
A submodule of a finite module over a Noetherian ring is finite (Over a Noetherian ring a module is Noetherian exactly when it is finitely generated, exactly when it is finitely presented).
Proof
Since for every , Artin-Rees gives some such that for all , In particular .
Conversely, if for some , then . Iterating gives for every , hence .
Steps 2.1 and 1.2 identify with the set of -torsion elements claimed in part 1.
The submodule is finite by [L4]. Applying [L2] to and the equality from step 1.1 gives with So every element of satisfies the displayed torsion condition.
Assume now . For any , step 2.1 gives some with . By [L3], is a unit, so multiplying by its inverse gives . Thus .
Therefore both stated conclusions hold.
Depends on
- Artin-Rees controls intersections of submodules with high ideal powers
- Determinant trick for Nakayama
- Assuming the Axiom of Choice, an element lies in the Jacobson radical exactly when one minus any multiple is a unit
- Over a Noetherian ring a module is Noetherian exactly when it is finitely generated, exactly when it is finitely presented
Used by
Dependency tree · two levels
18 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
- Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, Exercise (20.19) (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, §24 (standard reference, not scraped)