CorollaryStatement: 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 commutes with finite quotients and induced submodules

Statement

Assume the Axiom of Choice.

Let $R$ be a Noetherian commutative ring, let $I \subseteq R$ be an ideal, and let $N \subseteq M$ be finitely generated $R$ -modules.

The natural map $\hat{M} / \hat{N} ⟶ \hat{M / N}$ is an isomorphism.
Under the natural map $\hat{N} \to \hat{M}$ , the image of $\hat{N}$ is the $\hat{R}$ -submodule $N \hat{R} \subseteq \hat{M}$ . In particular, for every ideal $J \subseteq R$ , $\hat{J M} ≅ J \hat{M} .$
For every $n \geq 0$ , $\hat{M} / I^{n} \hat{M} ≅ M / I^{n} M .$

Facts & Assumptions

Given: A Noetherian commutative ring $R$ , an ideal $I \subseteq R$ , and finite $R$ -modules $N \subseteq M$ .

[L1]

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

[L2]

For a finite module $X$ , one has $\hat{X} ≅ X \otimes_{R} \hat{R}$ (Completion of a finite module is extension of scalars).

Proof

technique · direct

1.1

Apply [L1] to the short exact sequence $0 \to N \to M \to M / N \to 0.$ This gives an exact sequence $0 \to \hat{N} \to \hat{M} \to \hat{M / N} \to 0.$ Therefore $\hat{M} / \hat{N} ≅ \hat{M / N},$ proving part 1.

1.2

By [L2], the map $\hat{N} \to \hat{M}$ identifies with $N \otimes_{R} \hat{R} ⟶ M \otimes_{R} \hat{R} .$ Its image is, by definition, the $\hat{R}$ -submodule generated by the image of $N$ , namely $N \hat{R}$ . Hence the image of $\hat{N}$ in $\hat{M}$ is $N \hat{R}$ . Taking $N = J M$ yields $\hat{J M} ≅ J \hat{M} .$

L2algebra

2.1

Apply part 1 to the submodule $I^{n} M \subseteq M$ . Then $\hat{M} / \hat{I^{n} M} ≅ \hat{M / I^{n} M} .$ By step 1.2, $\hat{I^{n} M}$ identifies with $I^{n} \hat{M}$ . Also $M / I^{n} M$ is annihilated by $I^{n}$ , so its $I$ -adic filtration reaches $0$ after stage $n$ and its completion is canonically itself. Hence $\hat{M / I^{n} M} ≅ M / I^{n} M,$ which proves part 3.

step 1.1step 1.2algebra

3.1

Parts 1, 2, and 3 are exactly the three displayed conclusions above.

step 1.1step 1.2step 2.1∎

Depends on

Used by

Dependency tree · two levels

13 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., Corollaries 22.20-22.22 (standard reference, not scraped)
The Stacks Project, Lemma 10.97.4 (standard reference, not scraped)