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.
Length and valuation in a DVR
Statement
Let be a discrete valuation ring with uniformiser . Then for every integer ,
More generally, if is nonzero and with a unit, then
Facts & Assumptions
Given: A discrete valuation ring with uniformiser .
Every nonzero element of the fraction field of is uniquely with a unit and (Every nonzero fraction is a unit times a power of a uniformiser).
Every nonzero ideal of is for a unique integer (Ideals in a DVR are powers of the maximal ideal).
A composition series has finitely many simple factors, and the length is their number (Composition series and length of a module).
Length is additive in short exact sequences (Module length is additive in short exact sequences).
Proof
The case is , whose length is by [F1]. For , the ideals of correspond to the ideals of containing . By [L2], those are only and , so is simple and has length .
For each there is a short exact sequence . Multiplication by induces an isomorphism , so step 1.1 gives . Therefore [L3] yields .
By induction on , step 1.1 and step 2.1 give for every .
Let be nonzero, and write as in [L1]. Multiplication by the unit identifies the ideals and , so as -modules. Hence .
Depends on
Used by
- Computing the length of R/(πⁿ) Example
Dependency tree · two levels
11 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
- J. S. Milne, A Primer of Commutative Algebra, v4.03, Discrete valuation rings after Example 20.1 (standard reference, not scraped)
- Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., §23 (standard reference, not scraped)