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.
A nonzero PID submodule has a maximal coordinate ideal and a primitive pivot
Statement
Let be a PID, let be a nonzero finite free -module, and let . A nonzero submodule of a finite free PID module admits a primitive pivot splitting both the ambient module and submodule. More precisely, there are , , a nonzero , and such that , the ideal is maximal among value ideals containing a fixed nonzero value ideal, and
Moreover belongs to a basis of , and is free of rank one less than the rank of .
The maximality is taken among all functional value ideals, so it remains available after the pivot is split off.
Facts & Assumptions
Given: The dual module of The -module over a commutative ring and coordinate functionals from a finite free basis (The free module on a set and its standard basis).
Every principal ideal domain is a unique factorisation domain (Every principal ideal domain is a unique factorisation domain).
Proof
Some coordinate functional has a nonzero value on . Fix one such nonzero value ideal . By [L1], a nonzero generator of has only finitely many divisor classes, so only finitely many principal ideals can contain . Choose a maximal value ideal among them, write it as with , and choose with .
For any coordinate functional , let generate and choose with . The functional takes to , so its value ideal contains ; maximality in step 1.1 forces , hence .
Divisibility of every coordinate of gives for some . Since and , cancellation gives , so is primitive.
The ideal generated by the coordinates of in a basis of is , so it does not depend on the basis, and makes it all of . Fix a basis of and let be the coordinates of in it. For let generate . If then and nothing is done; otherwise write and put , whose entries lie in and whose determinant is , so has entries in as well. Replacing the basis pair by the pair whose coordinates are the columns of again gives a basis of , in which the coordinates of at and are the entries of and the other coordinates are unchanged. Doing this for in turn clears the coordinates , so the resulting basis has with the coordinate ideal, which is . Hence is a unit and is a basis of .
Put for . The passage from to is triangular with on the diagonal, so the latter is again a basis of , and each lies in . If lies in , applying gives ; hence is a basis of , which is therefore free of rank , and zero when . Every is with the second summand in , and because , so . For one has , say , and then with ; also , since and in the domain . Hence . When is a unit, and generate the same submodule and the second decomposition reads .
Depends on
Used by
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
- K. Conrad, Modules over a PID, Theorem 2.14 (standard reference, not scraped)