TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-31

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.

Finite torsion-free Dedekind modules split into invertible ideal summands

Statement

Assume the Axiom of Choice. Let $R$ be a Dedekind domain and let $M$ be a finite torsion-free $R$ -module. Then there exist invertible fractional ideals $I_{1}, \dots, I_{r}$ such that $M ≅ I_{1} \oplus \dots \oplus I_{r}$ . In particular, every finite torsion-free module over a Dedekind domain is projective.

Facts & Assumptions

Given: A Dedekind domain $R$ , its fraction field $K$ , and a finite torsion-free $R$ -module $M$ .

[L1]

Every finite torsion-free module over a Dedekind domain is projective (Finite torsion-free modules over Dedekind domains are projective).

[L2]

A nonzero finite projective Dedekind module splits as $N \oplus I$ with $I$ an invertible fractional ideal (A nonzero finite projective module over a Dedekind domain splits off a rank-one summand).

[L3]

Invertible fractional ideals are exactly the finite rank-one projective modules (Invertible fractional ideals are exactly the rank-one projective modules).

Proof

technique · direct

1.1givenalgebra

Let $r : = \dim_{K} (M \otimes_{R} K)$ . If $r = 0$ , then $M = 0$ because $M$ is torsion-free, so the empty direct sum gives the claim.

2.1L1L2L3step 1.1induction

Suppose $r > 0$ . By [L1], the module $M$ is projective. If $r = 1$ , then [L3] identifies $M$ itself with an invertible fractional ideal, and we are done. If $r > 1$ , apply [L2] to write $M ≅ N \oplus I$ with $I$ invertible. Then $N$ is finite torsion-free and satisfies $\dim_{K} (N \otimes_{R} K) = r - 1$ . By induction on $r$ , the module $N$ is a finite direct sum of invertible fractional ideals, and adjoining the summand $I$ gives the same conclusion for $M$ .

3.1L3step 2.1∎

Every summand $I_{j}$ is projective by [L3], so the displayed decomposition also shows that $M$ is projective.

Remarks

This draft item deliberately stops at the decomposition into invertible ideal summands. It does not claim the stronger Steinitz normal form $R^{r - 1} \oplus I$ or uniqueness of the final ideal class, because those extra moves were not rebuilt here from the present dependency budget.

Depends on

Used by

Dependency tree · two levels

14 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

J. P. May, Notes on Dedekind Rings (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, §20 (standard reference, not scraped)
The Stacks Project, Lemma 15.22.11 (standard reference, not scraped)