TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (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.

Localisation of Hom for finite and finitely presented modules

Statement

Let $R$ be a commutative ring, let $S \subseteq R$ be multiplicative, and let $M, N$ be left $R$ -modules. The natural map $θ_{M, N} : S^{- 1} ⁣ {Hom}_{R} (M, N) ⟶ {Hom}_{S^{- 1} R} (S^{- 1} M, S^{- 1} N)$ is injective when $M$ is finitely generated, and it is an isomorphism when $M$ is finitely presented.

Facts & Assumptions

Given: A commutative ring $R$ , a multiplicative subset $S \subseteq R$ , and left $R$ -modules $M, N$ .

[L1]

The natural localisation map on Hom satisfies $θ_{M, N} (f / s) (m / u) = f (m) / (s u)$ (There is a natural localisation map on Hom).

[L2]

A finitely generated module has a finite generating set, and a finitely presented module admits a finite presentation by finite free modules (Generated submodule, cyclic and finitely generated modules, module basis and free module, Finitely presented modules and finitely presented algebras).

[L3]

A localised fraction is zero exactly when one denominator kills its numerator (A localised module fraction is zero exactly when one denominator kills its numerator).

[L4]

The group ${Hom}_{R} (M, N)$ is an $R$ -module (Over a commutative ring the homomorphism group ${Hom}_{R} (M, N)$ is an $R$ -module).

[L5]

The natural localisation map on Hom is an isomorphism for finite free sources (The localised Hom map is an isomorphism for finite free sources).

[L6]

A finite presentation reduces the Hom-localisation comparison to the finite free case (A finite presentation reduces localised Hom to the finite free case).

Proof

technique · direct

1.1L1L2L3L4choose

Suppose that $M$ is generated by $m_{1}, \dots, m_{r}$ and that $θ_{M, N} (f / s) = 0$ . Then $f (m_{i}) / s = 0$ for each $i$ by [L1], so [L3] gives $u_{i} \in S$ with $u_{i} f (m_{i}) = 0$ . Let $u = u_{1} \dots u_{r}$ . Then $u f (m_{i}) = 0$ for every generator, hence $u f = 0$ as a homomorphism $M \to N$ . Since ${Hom}_{R} (M, N)$ is an $R$ -module by [L4], [L3] applied there gives $f / s = 0$ . Therefore $θ_{M, N}$ is injective whenever $M$ is finitely generated.

1.2L2L5L6

If $M$ is finitely presented, [L2] supplies a finite presentation $R^{m} \to R^{n} \to M \to 0$ . The free modules $R^{m}$ and $R^{n}$ satisfy the isomorphism hypothesis of [L6] by [L5], so [L6] makes $θ_{M, N}$ an isomorphism.

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 prove the injective and finitely presented claims.

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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Proposition 12.25 (standard reference, not scraped)