Alphabeta Math
LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck passaudited 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.

The localised Hom map is an isomorphism for finite free sources

Statement

Let R be a commutative ring, let S⊆R be multiplicative, let M be a finite free R-module, and let N be a left R-module. Then the natural map θM,N:S−1 ⁣Hom⁡R(M,N)⟶Hom⁡S−1R(S−1M,S−1N) from There is a natural localisation map on Hom is an isomorphism.

Facts & Assumptions

Given: A commutative ring R, a multiplicative subset S⊆R, a finite free R-module M with basis e1,…,en, and a left R-module N.

[L1]

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

[L2]

A basis means that every element of M has a unique finite linear combination in the basis elements (Generated submodule, cyclic and finitely generated modules, module basis and free module).

[L3]

A homomorphism from a finite free module is uniquely determined by its basis values, and every tuple of target values occurs as those basis values (For a commutative ring, Hom⁡R(Rn,N)≅Nn).

[L4]

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

[L5]
[L6]

In S−1M, addition and scalar multiplication satisfy m/u=∑i(ai/u)(ei/1) whenever m=∑iaiei in M (Localisation of a module at a multiplicative subset).

Proof

technique · direct
1.1L2L6algebra

By [L2] and [L6], every element of S−1M is an S−1R-linear combination of e1/1,…,en/1, so two S−1R-linear maps S−1M→S−1N that agree on all ei/1 are equal.

1.2L1L3L4L5choose

If θM,N(f/s)=0, then f(ei)/s=0 for each i, so [L4] gives ui∈S with uif(ei)=0. Let u=u1⋯un. Then uf(ei)=0 for every i, hence uf=0 by [L3]. Since Hom⁡R(M,N) is an R-module by [L5], [L4] applied there gives f/s=0. Thus θM,N is injective.

1.3L3choose

Let φ:S−1M→S−1N be S−1R-linear. Write φ(ei/1)=ni/si with ni∈N and si∈S, set s=s1⋯sn, and set mi=(s/si)ni. By [L3], there is a unique R-linear map f:M→N with f(ei)=mi for all i.

2.1L1step 1.1step 1.3algebra

For each basis vector, θM,N(f/s)(ei/1)=f(ei)/s=(s/si)ni/s=ni/si=φ(ei/1), so step 1.1 gives θM,N(f/s)=φ. Thus θM,N is surjective.

3.1step 1.2step 2.1∎

Steps 1.2 and 2.1 prove that θM,N is an isomorphism.

Depends on

Used by

Dependency tree · two levels

18 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