TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Primary decomposition and elementary-divisor form for finitely generated PID modules

Statement

Let $M$ be finitely generated over a PID $R$ . For each irreducible $p$ , the $p$ -primary component is a finite direct sum of modules $R / (p^{e})$ . A finitely generated torsion PID module is the direct sum of its prime-power cyclic elementary-divisor summands. In general,

$M ≅ R^{r} \oplus ⨁_{p} ⨁_{j} R / (p^{e_{p, j}}),$

with only finitely many nonzero summands. Conversely, aligning the prime powers into divisibility columns reconstructs an invariant-factor decomposition.

Facts & Assumptions

Given: The elementary-divisor convention of Invariant factors and elementary divisors of a finitely generated module over a PID, the UFD property of a PID (Every principal ideal domain is a unique factorisation domain), and the fact that primary elements form submodules (Torsion elements and $p$ -primary elements form submodules over a domain).

[L1]

Every finitely generated PID module is a finite free module direct-summed with cyclic torsion quotients (Invariant-factor decomposition of a finitely generated module over a PID).

[L2]

Coprime cyclic quotients split by the Chinese remainder map (Coprime cyclic quotients over a PID split by the Chinese remainder map).

Proof

technique · constructive

1.1

Take the invariant-factor decomposition from [L1]. Factor each nonunit $a_{i}$ uniquely up to associates as a finite product of powers of pairwise nonassociate irreducibles. The free part is kept separate, and no factorization is assigned to zero or to a unit.

L1given

2.1

The prime-power factors of one $a_{i}$ are pairwise coprime, so [L2] splits $R / (a_{i})$ into the corresponding quotients $R / (p^{e})$ . Applying this to every invariant factor gives a finite elementary-divisor direct sum.

step 1.1L2

3.1

Grouping the summands by the associate class of $p$ gives exactly $M [p^{\infty}]$ , because an element is killed by a power of $p$ precisely in those summands. Thus the torsion submodule is the direct sum of its primary components, each having the asserted form.

step 2.1algebra

4.1

Conversely, order the powers for each prime by exponent, align the largest powers in the last column, pad missing entries by units, and multiply down columns. Each column divides the next, and repeated use of [L2] recovers the original elementary-divisor sum. This constructs the invariant factors, including empty torsion data.

step 3.1L2constructdischarge-construct∎

Depends on

Used by

Dependency tree · two levels

19 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.5 (standard reference, not scraped)
A. Apisa, Wisconsin Math 542, Lecture 11 (standard reference, not scraped)