LemmaStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + 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.

Every generating set of a finitely generated module contains a finite generating subset

Statement

Let $R$ be a ring, let $M$ be a finitely generated left $R$ -module (Generated submodule, cyclic and finitely generated modules, module basis and free module) and let $S \subseteq M$ satisfy $⟨ S ⟩_{R} = M$ . Then some finite subset $S^{'} \subseteq S$ already satisfies $⟨ S^{'} ⟩_{R} = M$ .

No hypothesis is placed on $S$ itself, which may be infinite, and none on $R$ beyond being a ring.

Facts & Assumptions

Given: A ring $R$ , a finitely generated left $R$ -module $M$ , and a subset $S \subseteq M$ generating $M$ .

[L1]

$M$ is finitely generated when $M = ⟨ T ⟩_{R}$ for some finite $T$ , and $⟨ T ⟩_{R}$ is the smallest submodule of $M$ containing $T$ (Generated submodule, cyclic and finitely generated modules, module basis and free module).

[L2]

For a ring $R$ , a left $R$ -module $M$ and a subset $S \subseteq M$ , the submodule $⟨ S ⟩_{R}$ is the set of finite sums $\sum_{i = 1}^{k} r_{i} s_{i}$ with $k \in N$ , $r_{i} \in R$ and $s_{i} \in S$ , the term with $k = 0$ being $0_{M}$ (The submodule generated by a subset consists of the finite $R$ -linear combinations of that subset).

Proof

technique · direct

1.1

Fix a finite $T \subseteq M$ with $⟨ T ⟩_{R} = M$ , available because $M$ is finitely generated, and recall the hypothesis $⟨ S ⟩_{R} = M$ .

L1given

2.1

For each $t \in T$ we have $t \in M = ⟨ S ⟩_{R}$ , so $t = \sum_{i = 1}^{k} r_{i} s_{i}$ for some $k \in N$ , some $r_{1}, \dots, r_{k} \in R$ and some $s_{1}, \dots, s_{k} \in S$ ; write $S_{t} : = {s_{1}, \dots, s_{k}} \subseteq S$ , a finite set with $t \in ⟨ S_{t} ⟩_{R}$ . One such expression is selected for each of the finitely many elements of $T$ , so this is a finite sequence of selections and no choice axiom is used.

L2step 1.1given

3.1

Put $S^{'} : = ⋃_{t \in T} S_{t}$ . This is a union of finitely many finite sets, hence finite, and $S^{'} \subseteq S$ ; moreover $S_{t} \subseteq S^{'}$ gives $⟨ S_{t} ⟩_{R} \subseteq ⟨ S^{'} ⟩_{R}$ , so $t \in ⟨ S^{'} ⟩_{R}$ for every $t \in T$ , that is $T \subseteq ⟨ S^{'} ⟩_{R}$ .

step 2.1algebra

4.1

$⟨ S^{'} ⟩_{R}$ is a submodule of $M$ containing $T$ , so it contains the smallest such submodule, namely $⟨ T ⟩_{R} = M$ ; and $⟨ S^{'} ⟩_{R} \subseteq M$ always. Hence $⟨ S^{'} ⟩_{R} = M$ with $S^{'} \subseteq S$ finite.

L1step 1.1step 3.1∎

Remarks

The finite generating subset depends on the chosen $T$ , and no smallest one is claimed. Different finite generating sets $T$ produce different subsets $S^{'}$ , and the lemma asserts only that some finite subset of $S$ generates. It says nothing about the least possible size of such a subset.
The hypothesis that $M$ is finitely generated cannot be dropped. Without it the conclusion is the assertion that every generating set of every module has a finite generating subset, which would make every module finitely generated, since a module always generates itself.

Depends on

Used by

A subring that admits a module retraction from a Noetherian ring is Noetherian Lemma

Dependency tree · two levels

7 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, §3 (3.15) (standard reference, not scraped)
A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise (16.2) (standard reference, not scraped)