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 be a Noetherian commutative ring and let be finitely generated -modules. Then , with the -module structure of Over a commutative ring the homomorphism group is an -module, is a finitely generated -module.
The proof exhibits as isomorphic to a submodule of for a suitable . It does not assert that the embedding is onto, and in general it is not.
Facts & Assumptions
Given: A Noetherian commutative ring and finitely generated -modules and .
A module is finitely generated when it equals for some finite subset (Generated submodule, cyclic and finitely generated modules, module basis and free module).
Every set map extends uniquely to an -module homomorphism with (Universal property of the free module on a set).
For a ring , a left -module and , the submodule is the set of finite sums with , and (The submodule generated by a subset consists of the finite -linear combinations of that subset).
For a homomorphism and a module , precomposition gives a map , (The abelian group and maps induced by pre- and postcomposition).
For a commutative ring and -modules , the abelian group is an -module under (Over a commutative ring the homomorphism group is an -module).
For a commutative ring , and an -module , the map is an isomorphism of -modules (For a commutative ring, ).
Every finitely generated left module over a left Noetherian ring is Noetherian (Finitely generated modules over a left Noetherian ring are Noetherian).
A finite direct sum is Noetherian if and only if every summand is Noetherian (Finite direct sums preserve and reflect Noetherian and Artinian conditions).
In the standard basis vector has coordinate at and zero elsewhere, and every element is uniquely a finite -linear combination of them (The free module on a set and its standard basis).
A left -module is Noetherian when every submodule of it is finitely generated (Noetherian modules: every submodule is finitely generated).
Proof
Fix a finite generating set of , with . The universal property of the free module gives with , and its image is the set of finite sums , that is ; so is surjective.
Precomposition with gives , . It is -linear for the module structures above, since and , both by evaluating at a point of . It is injective: if then vanishes on , so .
The module is Noetherian. Indeed is finitely generated over the Noetherian ring , hence a Noetherian module; the finite direct sum of copies of is then Noetherian; and is isomorphic to , while an isomorphism of modules carries submodules to submodules and finite generating sets to finite generating sets, so the isomorphic module is Noetherian too.
The image is a submodule of the Noetherian module , hence finitely generated; and is injective and -linear, so is isomorphic to that image and is therefore finitely generated as well.
Remarks
-
The injectivity of is an instance of left exactness. Covariant and contravariant are left exact gives it for any exact ; 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 descends to exactly when it kills , and most do not; the corollary needs only the embedding.
-
Both hypotheses of finite generation are used, and for different reasons. Finite generation of produces the free cover in step 1.1; finite generation of makes the target Noetherian in step 2.2.
Depends on
- Over a commutative ring the homomorphism group $\operatorname{Hom}_R(M,N)$ is an $R$-module
- For a commutative ring, $\operatorname{Hom}_R(R^n,N)\cong N^n$
- Finitely generated modules over a left Noetherian ring are Noetherian
- Noetherian modules: every submodule is finitely generated
- Finite direct sums preserve and reflect Noetherian and Artinian conditions
- Universal property of the free module on a set
- The submodule generated by a subset consists of the finite $R$-linear combinations of that subset
- The free module on a set and its standard basis
- Generated submodule, cyclic and finitely generated modules, module basis and free module
- The abelian group $\operatorname{Hom}_R(M,N)$ and maps induced by pre- and postcomposition
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
- A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise (16.20) (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, §1 and §3 (standard reference, not scraped)