TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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.

Completion of a finite module is extension of scalars

Statement

Assume the Axiom of Choice.

Let $R$ be a Noetherian commutative ring, let $I \subseteq R$ be an ideal, and let $M$ be a finitely generated $R$ -module. Then the canonical $R$ -linear map $θ_{M} ⁣ : M \otimes_{R} \hat{R} ⟶ \hat{M}, m \otimes (r_{n})_{n} \mapsto (m r_{n} m o d I^{n} M)_{n},$ is an isomorphism.

Facts & Assumptions

Given: A Noetherian commutative ring $R$ , an ideal $I \subseteq R$ , and a finitely generated $R$ -module $M$ .

[L1]

Completion is exact on finitely generated modules over a Noetherian ring (Adic completion is exact on finite modules over a Noetherian ring).

[L2]

Tensor products are right exact (Tensoring is right exact).

[L3]

For every module $N$ , the canonical map $N \otimes_{R} R \to N$ is an isomorphism, and tensor products commute with finite direct sums (The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

Proof

technique · direct

1.1

If $M = R$ , then $R \otimes_{R} \hat{R} ≅ \hat{R}$ by [L3], and this is exactly $θ_{R}$ . Therefore $θ_{R}$ is an isomorphism.

1.2

Choose an exact sequence $F_{1} \overset{u}{\to} F_{0} \to M \to 0$ with $F_{0}$ and $F_{1}$ finite free. Tensoring with $\hat{R}$ and using [L2] gives an exact row $F_{1} \otimes_{R} \hat{R} \overset{u \otimes 1}{\to} F_{0} \otimes_{R} \hat{R} \to M \otimes_{R} \hat{R} \to 0.$ Completing the exact sequence $F_{1} \overset{u}{\to} F_{0} \to M \to 0$ and using [L1] gives another exact row $\hat{F_{1}} \overset{\hat{u}}{\to} \hat{F_{0}} \to \hat{M} \to 0.$

L1L2choose

2.1

Since tensor products commute with finite direct sums by [L3], the same is true for finite free modules: $R^{m} \otimes_{R} \hat{R} ≅ {\hat{R}}^{m} ≅ \hat{R^{m}} .$ Thus $θ_{F}$ is an isomorphism for every finite free module $F$ . In particular, $θ_{F_{0}}$ and $θ_{F_{1}}$ are isomorphisms in step 1.2.

step 1.1L3

3.1

The maps $θ_{F_{1}}$ , $θ_{F_{0}}$ , and $θ_{M}$ form a commutative diagram between the two exact rows of step 1.2. Since the first two vertical maps are isomorphisms by step 2.1, the two rows present $M \otimes_{R} \hat{R} and \hat{M}$ as cokernels of isomorphic maps. Therefore $θ_{M}$ is an isomorphism.

step 1.2step 2.1

4.1

So the completion of a finite module is obtained by extension of scalars from $R$ to $\hat{R}$ .

step 3.1∎

Depends on

Used by

Dependency tree · two levels

20 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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Corollary 22.20 (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, Proposition 24.5 (standard reference, not scraped)