Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

  1. M is a Noetherian module (Noetherian modules: every submodule is finitely generated).
  2. M is finitely generated (Generated submodule, cyclic and finitely generated modules, module basis and free module).
  3. 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∈N, Rn denotes the free module on an n-element set with standard basis e1,…,en.

[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⊆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 ∑x∈Frxex with F⊆X finite, where ex has coordinate 1R at x and zero elsewhere; for X=∅ the module is 0 (The free module on a set and its standard basis).

[L5]

Every set map u ⁣:X→M extends uniquely to an R-module homomorphism uˉ ⁣:R(X)→M with uˉ(ex)=u(x), given by uˉ(∑x∈Frxex)=∑x∈Frxu(x) (Universal property of the free module on a set).

[L6]

For a ring R, a left R-module M and S⊆M, the submodule ⟨S⟩R is the set of finite sums ∑i=1krisi with k∈N, ri∈R and si∈S, the term with k=0 being 0M (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∈N and an exact sequence Rm→Rn→M→0 (Finitely presented modules and finitely presented algebras).

Proof

technique · direct
1.1L1L2given

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

1.2L3given

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

1.3L2L4L6L7L8given

Condition 3 implies condition 2: an exact sequence Rm→Rn→M→0 has its right-hand map β surjective, because exactness at M says the image of β is the kernel of the zero map M→0, which is all of M; every element of Rn is ∑i=1nriei, so every element of M is ∑i=1nriβ(ei) and M is generated by the finite set {β(e1),…,β(en)}.

1.4L2L4L5L6given

Assume condition 2 and fix a finite generating set m1,…,mn of M, with n∈N. The universal property of the free module gives an R-module homomorphism β ⁣:Rn→M with β(ei)=mi, and its image is the set of all finite sums ∑irimi, which is ⟨m1,…,mn⟩R=M; so β is surjective.

2.1L1L2L3L4step 1.4

Still assuming condition 2, the module Rn is generated by the finite set {e1,…,en}, hence is Noetherian over the Noetherian ring R; therefore its submodule K:=ker⁡β is finitely generated, say by k1,…,km with m∈N.

3.1L5L6L7L8step 1.4step 2.1

Still assuming condition 2, the universal property gives α ⁣:Rm→Rn with α(ej)=kj, whose image is ⟨k1,…,km⟩R=K=ker⁡β; together with the surjectivity of β this makes Rm→Rn→M→0 exact, so M is finitely presented and condition 2 implies condition 3.

4.1step 1.1step 1.2step 1.3step 3.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.

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

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