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.
Uniqueness of invariant factors and elementary divisors over a PID
Statement
A finitely generated PID module is classified by its free rank and invariant factors, equivalently its elementary divisors. More precisely, the free rank is unique; invariant factors are unique up to associates in their divisibility order; elementary divisors are unique up to associates and permutation; and two finitely generated modules are isomorphic exactly when these data agree.
Facts & Assumptions
Given: Primary and invariant-factor existence from Primary decomposition and elementary-divisor form for finitely generated PID modules, invariant basis number for nonzero commutative rings (Every nonzero commutative ring has invariant basis number for finite bases), and the torsion/free splitting of A finitely generated PID module is its torsion submodule direct-summed with a finite free module.
The dimensions of recover every elementary-divisor exponent multiplicity (-power torsion dimensions recover the elementary divisors of a PID module).
Proof
An isomorphism carries torsion elements to torsion elements, so it induces an isomorphism of torsion submodules and of the quotients by torsion. The latter quotients are finite free, and invariant basis number recovers their common free rank.
For every associate class of irreducible and every , an isomorphism preserves , multiplication by , and the resulting -dimension. By [L1], it therefore preserves every elementary-divisor multiplicity.
Aligning the unique prime-power columns as in the primary-decomposition theorem recovers one divisibility chain of invariant factors up to associates. Hence invariant factors are unique as well. Empty torsion data, pure torsion, pure free, and the zero module are included.
Conversely, equal free ranks and equal invariant-factor or elementary-divisor data give termwise isomorphisms between the corresponding direct-sum decompositions; their direct sum constructs a module isomorphism. This proves both directions of the classification.
Depends on
- $p$-power torsion dimensions recover the elementary divisors of a PID module
- Primary decomposition and elementary-divisor form for finitely generated PID modules
- Every nonzero commutative ring has invariant basis number for finite bases
- A finitely generated PID module is its torsion submodule direct-summed with a finite free module
Used by
- The fundamental theorem of finitely generated abelian groups from PID modules Corollary
- Invariant factors and elementary divisors of an endomorphism Definition
- The free rank of a finitely generated module over a PID Definition
- Existence and uniqueness of rational canonical form Theorem
- Jordan canonical form from the elementary divisors of V_T Theorem
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
- M. Brussel, Finitely Generated Modules over a PID, Section 3.6 (standard reference, not scraped)
- A. Apisa, Wisconsin Math 542, Lecture 11 (standard reference, not scraped)
- K. Conrad, Modules over a PID, Section 5 (standard reference, not scraped)