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 torsion-free module over a PID is free
Statement
False claim. Every torsion-free module over a principal ideal domain is free, without a finite-generation hypothesis.
Facts & Assumptions
Given: The rational field (The rationals form a field), bases and free modules (Generated submodule, cyclic and finitely generated modules, module basis and free module), the integer ring and cancellation law (The integers form a commutative ring, The integers have no zero divisors; multiplicative cancellation), the fact that every additive subgroup of is cyclic (Every subgroup of is for exactly one natural number ), the PID definition (Principal ideal domain), and the valid finitely generated theorem Every finitely generated torsion-free module over a PID is free. These integer facts show that is a PID.
A module is torsion-free when its torsion subset is (Annihilators, torsion elements and the torsion subset of a module).
Refutation
Under the usual integer action, is a -module. If with , field cancellation gives , so it is torsion-free by [F1].
Suppose, for contradiction, that has a -basis . It cannot be empty because , so choose . Express as a finite integer linear combination of basis elements and multiply by . Uniqueness of basis coordinates would make the coefficient of simultaneously and an even integer, which is impossible.
Step 2.1 rules out every nonempty basis, and the empty basis cannot span the nonzero module. Thus is torsion-free over the PID but is not free; finite generation is essential.
Depends on
- Annihilators, torsion elements and the torsion subset of a module
- Generated submodule, cyclic and finitely generated modules, module basis and free module
- The rationals form a field
- Every finitely generated torsion-free module over a PID is free
- The integers form a commutative ring
- The integers have no zero divisors; multiplicative cancellation
- Every subgroup of $(\mathbb{Z}, +)$ is $\langle n \rangle = n\mathbb{Z}$ for exactly one natural number $n$
- Principal ideal domain
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
43 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, warning after Corollary 2.6 (standard reference, not scraped)