Alphabeta Math
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.

A finitely generated PID module is its torsion submodule direct-summed with a finite free module

Statement

If M is finitely generated over a PID R, then

MTor(M)Rr

for some r0. A finitely generated PID module is its torsion submodule direct-summed with a finite free module. The torsion submodule is canonical; a free complement need not be.

Facts & Assumptions

[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).

Proof

technique · direct
1.1

In [L1], every cyclic quotient R/(ai) is torsion, and every torsion element has zero component in the free summand because a free module over a domain is torsion-free. Thus the direct sum of the cyclic quotients is exactly Tor(M).

L1givenalgebra
2.1

Substituting that identification into the invariant-factor decomposition gives MTor(M)Rr. It includes pure torsion when r=0, pure free modules when Tor(M)=0, and the zero module when both vanish.

step 1.1
3.1

The torsion submodule is canonical because it is defined by M alone, while a free complement is not. Suppose aR is a nonzero nonunit and put M=RR/(a). Since R is a domain, an element (x,y+(a)) killed by some nonzero scalar has x=0, and a kills every (0,y+(a)); hence Tor(M)=0R/(a). Both C1=R(1,0+(a)) and C2=R(1,1+(a)) are free of rank one, because r(1,)=0 forces r=0, and each meets Tor(M) only in 0 while (x,y+(a))=(0,(yx)+(a))+x(1,1+(a)) shows Tor(M)+C2=M and likewise for C1. They are distinct: (1,1+(a))C2 lies in C1 only if a1, contrary to a being a nonunit.

step 2.1givenalgebra

Depends on

Used by

Dependency tree · two levels

12 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