CorollaryStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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.

Assuming the Axiom of Choice, generators modulo an ideal in the Jacobson radical lift to generators

Statement

Assume the Axiom of Choice.

Let $R$ be a commutative ring, let $I ⊴ R$ satisfy $I \subseteq J (R)$ , and let $M$ be a finitely generated left $R$ -module. If elements $x_{1}, \dots, x_{r} \in M$ generate $M / I M$ , then $x_{1}, \dots, x_{r}$ generate $M$ .

Facts & Assumptions

Given: A commutative ring $R$ , an ideal $I ⊴ R$ with $I \subseteq J (R)$ , a finitely generated left $R$ -module $M$ , and elements $x_{1}, \dots, x_{r} \in M$ whose images generate $M / I M$ .

[L1]

If a finite module $Q$ satisfies $I Q = Q$ and $I \subseteq J (R)$ , then $Q = 0$ (Assuming the Axiom of Choice, Nakayama's lemma).

[L2]

The submodule $I M$ consists of finite sums of products $i m$ with $i \in I$ and $m \in M$ (The submodule $I M$ generated by products of elements of an ideal $I$ with elements of a module $M$ ).

[L3]

A finite list of elements generates the submodule it spans (Generated submodule, cyclic and finitely generated modules, module basis and free module).

Proof

technique · direct

1.1

Let $N$ be the submodule of $M$ generated by $x_{1}, \dots, x_{r}$ . The hypothesis on $M / I M$ means every element of $M$ is congruent modulo $I M$ to an element of $N$ , so $M = N + I M$ .

L2L3given

2.1

Passing to the quotient $Q = M / N$ , step 1.1 gives $I Q = Q$ . Since $Q$ is a quotient of the finite module $M$ , it is finite, so [L1] gives $Q = 0$ .

step 1.1L1

3.1

The equality $Q = 0$ means $M = N$ , so $x_{1}, \dots, x_{r}$ generate $M$ .

step 2.1L3∎

Depends on

Used by

Assuming the Axiom of Choice, minimal generators over a local ring are exactly residue-field bases Corollary

Dependency tree · two levels

10 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. S. Milne, A Primer of Commutative Algebra, v4.03, Lemma 3.9 (standard reference, not scraped)
The Stacks Project, Lemma 10.20.1 (standard reference, not scraped)