Alphabeta Math
CorollaryStatement: 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 the homomorphism module between two finitely generated modules is finitely generated

Statement

Let R be a Noetherian commutative ring and let M,N be finitely generated R-modules. Then HomR(M,N), with the R-module structure of Over a commutative ring the homomorphism group HomR(M,N) is an R-module, is a finitely generated R-module.

The proof exhibits HomR(M,N) as isomorphic to a submodule of Nn for a suitable nN. It does not assert that the embedding is onto, and in general it is not.

Facts & Assumptions

Given: A Noetherian commutative ring R and finitely generated R-modules M and N.

[L1]

A module is finitely generated when it equals SR for some finite subset S (Generated submodule, cyclic and finitely generated modules, module basis and free module).

[L2]

Every set map u ⁣:XM extends uniquely to an R-module homomorphism uˉ ⁣:R(X)M with uˉ(ex)=u(x) (Universal property of the free module on a set).

[L3]

For a ring R, a left R-module M and SM, the submodule SR is the set of finite sums i=1krisi with kN, riR and siS (The submodule generated by a subset consists of the finite R-linear combinations of that subset).

[L4]

For a homomorphism u ⁣:MN and a module X, precomposition gives a map u ⁣:HomR(N,X)HomR(M,X), ggu (The abelian group HomR(M,N) and maps induced by pre- and postcomposition).

[L5]

For a commutative ring R and R-modules M,N, the abelian group HomR(M,N) is an R-module under (rf)(m)=rf(m) (Over a commutative ring the homomorphism group HomR(M,N) is an R-module).

[L6]

For a commutative ring R, nN and an R-module N, the map f(f(e1),,f(en)) is an isomorphism of R-modules HomR(Rn,N)Nn (For a commutative ring, HomR(Rn,N)Nn).

[L7]

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

[L8]

A finite direct sum is Noetherian if and only if every summand is Noetherian (Finite direct sums preserve and reflect Noetherian and Artinian conditions).

[L9]

In R(X) the standard basis vector ex has coordinate 1R at x and zero elsewhere, and every element is uniquely a finite R-linear combination of them (The free module on a set and its standard basis).

[L10]

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

Proof

technique · direct
1.1

Fix a finite generating set m1,,mn of M, with nN. The universal property of the free module gives π ⁣:RnM with π(ei)=mi, and its image is the set of finite sums irimi, that is m1,,mnR=M; so π is surjective.

L1L2L3L9given
2.1

Precomposition with π gives π ⁣:HomR(M,N)HomR(Rn,N), ggπ. It is R-linear for the module structures above, since (g+g)π=gπ+gπ and (rg)π=r(gπ), both by evaluating at a point of Rn. It is injective: if gπ=0 then g vanishes on imπ=M, so g=0.

L4L5step 1.1
2.2

The module HomR(Rn,N) is Noetherian. Indeed N is finitely generated over the Noetherian ring R, hence a Noetherian module; the finite direct sum Nn of copies of N is then Noetherian; and HomR(Rn,N) is isomorphic to Nn, while an isomorphism of modules carries submodules to submodules and finite generating sets to finite generating sets, so the isomorphic module is Noetherian too.

L6L7L8L10step 1.1
3.1

The image π(HomR(M,N)) is a submodule of the Noetherian module HomR(Rn,N), hence finitely generated; and π is injective and R-linear, so HomR(M,N) is isomorphic to that image and is therefore finitely generated as well.

L10step 2.1step 2.2

Remarks

  • The injectivity of π is an instance of left exactness. Covariant and contravariant Hom are left exact gives it for any exact ABC0; step 2.1 writes out the case needed here, which uses only that π is surjective and so does not require assembling the exact sequence first.

  • No claim of surjectivity. A homomorphism RnN descends to M exactly when it kills kerπ, and most do not; the corollary needs only the embedding.

  • Both hypotheses of finite generation are used, and for different reasons. Finite generation of M produces the free cover in step 1.1; finite generation of N makes the target Noetherian in step 2.2.

Depends on

Used by

Dependency tree · two levels

23 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