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.
FALSE: every finitely generated module over a domain is a direct sum of cyclic modules
Statement
False claim. Every finitely generated module over an integral domain is a direct sum of cyclic modules.
Facts & Assumptions
Given: Cyclic and finitely generated modules (Generated submodule, cyclic and finitely generated modules, module basis and free module), torsion over a domain (Annihilators, torsion elements and the torsion subset of a module), the integer ring and its cancellation law (The integers form a commutative ring, The integers have no zero divisors; multiplicative cancellation), the fact that a polynomial ring over a domain is a domain (A polynomial ring over an integral domain is an integral domain), and the valid classification under the stronger PID hypothesis (Invariant-factor decomposition of a finitely generated module over a PID).
For , the ideal is written and is called principal (The ideal generated by a subset and principal ideals).
Refutation
Let and . The ring is a domain, and is generated by the displayed elements, so it is a two-generated torsion-free -module.
Any nonzero cyclic submodule of the torsion-free ideal is isomorphic to . If a direct-sum decomposition contained two nonzero cyclic summands with nonzero generators , the relation would be a nontrivial relation between them, contradicting directness. Thus a cyclic decomposition could have at most one nonzero summand.
A single nonzero cyclic summand would make principal by [F1]. But a generator would divide both and in , hence would be a unit; that would give , while reduction modulo shows . Thus is not cyclic and has no direct-sum decomposition into cyclic modules, refuting the claim and isolating the PID hypothesis.
Depends on
- Generated submodule, cyclic and finitely generated modules, module basis and free module
- The ideal generated by a subset and principal ideals
- Annihilators, torsion elements and the torsion subset of a module
- Invariant-factor decomposition of a finitely generated module over a PID
- The integers form a commutative ring
- The integers have no zero divisors; multiplicative cancellation
- A polynomial ring over an integral domain is an integral domain
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
32 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, Example 4.9 and Remark 4.10 (standard reference, not scraped)