PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Extension to the fraction field recovers the free rank of a finitely generated PID module

Statement

Let $R$ be a PID, $Q = Frac (R)$ , and $M$ a finitely generated $R$ -module. Then

$\dim_{Q} (Q \otimes_{R} M) = {rank}_{R} M .$

Thus $\dim_{Frac (R)} (Frac (R) \otimes_{R} M)$ equals the free rank of $M$ .

Facts & Assumptions

Given: The free-rank definition of The free rank of a finitely generated module over a PID, fraction fields and extension of scalars (The field of fractions $Frac (D) = (D ∖ {0})^{- 1} D$ of an integral domain, Restriction of scalars and extension of scalars $S \otimes_{R} M$ along a ring homomorphism $R \to S$ ), and vector-space dimension (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

[L1]

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}$ (Invariant-factor decomposition of a finitely generated module over a PID).

[L2]

For every integral domain $D$ , the localisation $Frac (D)$ is a field and contains an embedded copy of $D$ ( $Frac (D)$ is a field and $d \mapsto d / 1$ embeds the integral domain $D$ ).

[L3]

The unit tensor maps are module isomorphisms and respect every displayed outer module structure (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

[L4]

Tensor products commute with arbitrary direct sums in either variable, including the empty sum (Tensor products commute with arbitrary direct sums).

Proof

technique · direct

1.1L1L4given

Write $M ≅ R^{r} \oplus T$ by [L1], with $T = ⨁_{i = 1}^{t} R / (a_{i})$ and each $a_{i}$ a nonzero nonunit. This is an invariant-factor decomposition, so $r = {rank}_{R} M$ by the free-rank definition in the Given. Extension of scalars and [L4] give $Q \otimes_{R} M ≅ (Q \otimes_{R} T) \oplus (Q \otimes_{R} R^{r})$ .

2.1step 1.1L2algebra

Every $m \in T$ is killed by the nonzero product $a_{1} \dots a_{t} \in R$ ; in $Q$ that scalar is invertible by [L2], so each simple tensor satisfies $q \otimes m = a^{- 1} q \otimes a m = 0$ for that $a$ . Simple tensors generate the tensor product, hence $Q \otimes_{R} T = 0$ .

3.1step 1.1step 2.1L3L4∎

By [L3] and [L4], $Q \otimes_{R} R^{r} ≅ Q^{r}$ . Therefore $Q \otimes_{R} M ≅ Q^{r}$ and its $Q$ -dimension is $r$ , which step 1.1 identified with ${rank}_{R} M$ . This includes $r = 0$ , pure torsion, pure free, rank one, and the zero module, where $t = 0$ makes $T$ the zero module.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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, Lemma 1.2 and rank discussion (standard reference, not scraped)