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.

Complete Nakayama lemma

Statement

Assume the Axiom of Dependent Choice.

Let $R$ be a commutative ring, let $I \subseteq R$ be an ideal, and let $M$ be an $R$ -module. Assume that $R$ is $I$ -adically complete and that $M$ is $I$ -adically separated.

If $m_{1}, \dots, m_{r} \in M$ have images that generate $M / I M$ as an $R / I$ -module, then $m_{1}, \dots, m_{r}$ generate $M$ as an $R$ -module.

Facts & Assumptions

Given: A commutative ring $R$ , an ideal $I \subseteq R$ , an $R$ -module $M$ with $R$ $I$ -adically complete and $M$ $I$ -adically separated, and elements $m_{1}, \dots, m_{r} \in M$ whose classes generate $M / I M$ .

[L1]

An $I$ -adically complete module is identified with the inverse limit of its quotients, and separated means $⋂_{n \geq 0} I^{n} M = 0$ (Separated and complete filtered modules).

Proof

technique · direct

1.1

Let $N : = R m_{1} + \dots + R m_{r}$ . We prove $M = N$ . Fix $x \in M$ . Since the classes of the $m_{i}$ generate $M / I M$ , choose coefficients $a_{i, 0} \in R$ and an element $x_{1} \in I M$ such that $x = \sum_{i = 1}^{r} a_{i, 0} m_{i} + x_{1} .$

givenchoose

2.1

Suppose $x_{n} \in I^{n} M$ has been constructed. Because multiplication by elements of $I^{n}$ shows that the classes of the $m_{i}$ also generate $I^{n} M / I^{n + 1} M$ , choose coefficients $a_{i, n} \in I^{n}$ and $x_{n + 1} \in I^{n + 1} M$ such that $x_{n} = \sum_{i = 1}^{r} a_{i, n} m_{i} + x_{n + 1} .$ Inductively, for every $N \geq 0$ , $x = \sum_{n = 0}^{N} \sum_{i = 1}^{r} a_{i, n} m_{i} + x_{N + 1}$ with $x_{N + 1} \in I^{N + 1} M$ .

step 1.1choose

3.1

For each $i$ , the partial sums $A_{i, N} : = \sum_{n = 0}^{N} a_{i, n}$ form a Cauchy sequence in the $I$ -adic topology on $R$ , because $A_{i, N^{'}} - A_{i, N} \in I^{N + 1}$ for $N^{'} \geq N$ . Since $R$ is complete, there is $A_{i} \in R$ with $A_{i} - A_{i, N} \in I^{N + 1}$ for every $N$ .

L1step 2.1choose

4.1

Set $y : = \sum_{i = 1}^{r} A_{i} m_{i} \in N .$ Using the identity in step 2.1, $x - y = (x - \sum_{i = 1}^{r} A_{i, N} m_{i}) - \sum_{i = 1}^{r} (A_{i} - A_{i, N}) m_{i} .$ The first term lies in $I^{N + 1} M$ because it equals $x_{N + 1}$ , and the second term also lies in $I^{N + 1} M$ because each $A_{i} - A_{i, N} \in I^{N + 1}$ . Hence $x - y \in I^{N + 1} M$ for every $N$ . By separatedness and [L1], $x - y \in ⋂_{N \geq 0} I^{N + 1} M = 0,$ so $x = y \in N$ .

L1step 2.1step 3.1algebra

5.1

Since every $x \in M$ lies in $N$ , one has $M = N$ , so $m_{1}, \dots, m_{r}$ generate $M$ .

step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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., Exercise 22.28 (standard reference, not scraped)
The Stacks Project, Lemma 10.96.12 (standard reference, not scraped)