CorollaryStatement: 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.

The fundamental theorem of finitely generated abelian groups from PID modules

Statement

Every finitely generated abelian group $G$ has unique canonical decompositions

$G ≅ Z^{r} \oplus Z / (n_{1}) \oplus \dots \oplus Z / (n_{t}), 1 < n_{1} ∣ \dots ∣ n_{t},$

and

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

where $r$ and the finite torsion data are unique up to the stated order. The torsion summand is finite. The trivial group has $r = 0$ and empty torsion data.

Facts & Assumptions

Given: The PID definition of Principal ideal domain.

[L1]

Abelian groups and $Z$ -modules have the same objects and morphisms; their subgroups, generated subobjects, cyclic objects, finite generation, and quotients agree (Abelian groups and $Z$ -modules have the same objects and morphisms).

[L2]

The integers form a commutative ring with multiplicative identity (The integers form a commutative ring).

[L3]

If $x, y \in Z$ are nonzero, then $x y \neq 0$ (The integers have no zero divisors; multiplicative cancellation).

[L4]

Every subgroup of $(Z, +)$ is cyclic (Every subgroup of $(Z, +)$ is $⟨ n ⟩ = n Z$ for exactly one natural number $n$ ).

[L5]

A finitely generated PID module is classified by its free rank and invariant factors, equivalently its elementary divisors: 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 such modules are isomorphic exactly when these data agree (Uniqueness of invariant factors and elementary divisors over a PID).

[L6]

Every finitely generated module over a PID $R$ is isomorphic to $R^{s} \oplus R / (a_{1}) \oplus \dots \oplus R / (a_{t})$ with each $a_{i}$ a nonzero nonunit and $a_{1} ∣ \dots ∣ a_{t}$ , and also to $R^{r} \oplus ⨁_{p, j} R / (p^{e_{p, j}})$ with finitely many nonzero prime-power summands (Invariant-factor decomposition of a finitely generated module over a PID, Primary decomposition and elementary-divisor form for finitely generated PID modules).

Proof

technique · constructive

1.1

By [L2] and [L3], $Z$ is a commutative unital ring without zero divisors, hence an integral domain.

L2L3

1.2

Every ideal of $Z$ is an additive subgroup and is cyclic by [L4], so it is generated by one integer.

L4algebra

2.1

Steps 1.1 and 1.2 verify the domain and principal-ideal clauses, so $Z$ is a PID.

step 1.1step 1.2given

3.1

Regard $G$ as the canonical finitely generated $Z$ -module from [L1]. Applying [L6] over the PID in step 2.1 gives the free summand and the invariant-factor and elementary-divisor decompositions, and [L5] makes the free rank and the torsion data unique; [L1] translates the cyclic quotients back to cyclic abelian groups. Uniqueness and the converse construction are preserved by the dictionary.

step 2.1L1L5L6construct

4.1

Each torsion summand $Z / (n)$ is finite, and only finitely many occur, so their direct sum is finite. The free rank may be zero, and empty torsion data gives a finitely generated free abelian group.

step 3.1algebradischarge-construct∎

Depends on

Used by

The PID-module and finite-abelian-group classifications have the same canonical data Proposition

Dependency tree · two levels

54 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.2 (standard reference, not scraped)
M. Brussel, Finitely Generated Modules over a PID, Section 4 (standard reference, not scraped)
K. Conrad, Introductory Notes on Modules, Section 4 (standard reference, not scraped)