TheoremStatement: Literature-sourcedProof: AI-adaptedSession-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.

Over a Noetherian ring a module is Noetherian exactly when it is finitely generated, exactly when it is finitely presented

Statement

Let $R$ be a Noetherian commutative ring and let $M$ be an $R$ -module. The following are equivalent.

$M$ is a Noetherian module (Noetherian modules: every submodule is finitely generated).
$M$ is finitely generated (Generated submodule, cyclic and finitely generated modules, module basis and free module).
$M$ is finitely presented (Finitely presented modules and finitely presented algebras).

The proof below shows exactly where the Noetherian hypothesis is used to make conditions 2 and 3 agree.

Facts & Assumptions

Given: A Noetherian commutative ring $R$ and an $R$ -module $M$ . For $n \in N$ , $R^{n}$ denotes the free module on an $n$ -element set with standard basis $e_{1}, \dots, e_{n}$ .

[L1]

A left $R$ -module $M$ is Noetherian when every submodule of $M$ is finitely generated (Noetherian modules: every submodule is finitely generated).

[L2]

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

[L3]

Every finitely generated left module over a left Noetherian ring is Noetherian (Finitely generated modules over a left Noetherian ring are Noetherian).

[L4]

In the free module $R^{(X)}$ every element has a unique expression $\sum_{x \in F} r_{x} e_{x}$ with $F \subseteq X$ finite, where $e_{x}$ has coordinate $1_{R}$ at $x$ and zero elsewhere; for $X = \emptyset$ the module is $0$ (The free module on a set and its standard basis).

[L5]

Every set map $u ⁣ : X \to M$ extends uniquely to an $R$ -module homomorphism $\overset{ˉ}{u} ⁣ : R^{(X)} \to M$ with $\overset{ˉ}{u} (e_{x}) = u (x)$ , given by $\overset{ˉ}{u} (\sum_{x \in F} r_{x} e_{x}) = \sum_{x \in F} r_{x} u (x)$ (Universal property of the free module on a set).

[L6]

For a ring $R$ , a left $R$ -module $M$ and $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).

[L7]

A sequence of modules and homomorphisms is exact at a module where two arrows meet when the image of the incoming map equals the kernel of the outgoing one (Exact sequences and short exact sequences of modules).

[L8]

An $R$ -module $M$ is finitely presented when there are $m, n \in N$ and an exact sequence $R^{m} \to R^{n} \to M \to 0$ (Finitely presented modules and finitely presented algebras).

Proof

technique · direct

1.1

Condition 1 implies condition 2, because $M$ is a submodule of itself and a Noetherian module has all of its submodules finitely generated.

L1L2given

1.2

Condition 2 implies condition 1, since $R$ is a Noetherian ring and a finitely generated module over such a ring is Noetherian.

L3given

1.3

Condition 3 implies condition 2: an exact sequence $R^{m} \to R^{n} \to M \to 0$ has its right-hand map $β$ surjective, because exactness at $M$ says the image of $β$ is the kernel of the zero map $M \to 0$ , which is all of $M$ ; every element of $R^{n}$ is $\sum_{i = 1}^{n} r_{i} e_{i}$ , so every element of $M$ is $\sum_{i = 1}^{n} r_{i} β (e_{i})$ and $M$ is generated by the finite set ${β (e_{1}), \dots, β (e_{n})}$ .

L2L4L6L7L8given

1.4

Assume condition 2 and fix a finite generating set $m_{1}, \dots, m_{n}$ of $M$ , with $n \in N$ . The universal property of the free module gives an $R$ -module homomorphism $β ⁣ : R^{n} \to M$ with $β (e_{i}) = m_{i}$ , and its image is the set of all finite sums $\sum_{i} r_{i} m_{i}$ , which is $⟨ m_{1}, \dots, m_{n} ⟩_{R} = M$ ; so $β$ is surjective.

L2L4L5L6given

2.1

Still assuming condition 2, the module $R^{n}$ is generated by the finite set ${e_{1}, \dots, e_{n}}$ , hence is Noetherian over the Noetherian ring $R$ ; therefore its submodule $K : = \ker β$ is finitely generated, say by $k_{1}, \dots, k_{m}$ with $m \in N$ .

L1L2L3L4step 1.4

3.1

Still assuming condition 2, the universal property gives $α ⁣ : R^{m} \to R^{n}$ with $α (e_{j}) = k_{j}$ , whose image is $⟨ k_{1}, \dots, k_{m} ⟩_{R} = K = \ker β$ ; together with the surjectivity of $β$ this makes $R^{m} \to R^{n} \to M \to 0$ exact, so $M$ is finitely presented and condition 2 implies condition 3.

L5L6L7L8step 1.4step 2.1

4.1

Steps 1.1, 1.2, 1.3 and 3.1 close the cycle: condition 1 gives condition 2, condition 2 gives condition 1 and condition 3, and condition 3 gives condition 2. The three conditions are therefore equivalent.

step 1.1step 1.2step 1.3step 3.1∎

Remarks

Where the Noetherian hypothesis is spent. Only in step 1.2, through Finitely generated modules over a left Noetherian ring are Noetherian, and in step 2.1, to make $\ker β$ finitely generated. Step 1.3 and step 1.4 hold over any commutative ring.
The presentation is not canonical. It depends on the chosen generating set of $M$ and on the chosen generating set of $\ker β$ ; different choices give different $m$ and $n$ , and nothing above claims either is minimal.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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., (16.19) (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, v4.03, §1 and §3 (standard reference, not scraped)