LemmaStatement: 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.

The localised scalar action is independent of representatives

Statement

If $a / u = a^{'} / u^{'}$ in $S^{- 1} R$ and $m / s = m^{'} / s^{'}$ in $S^{- 1} M$ , then $\frac{a m}{u s} = \frac{a^{'} m^{'}}{u^{'} s^{'}} .$ So the scalar action of Localisation of a module at a multiplicative subset is independent of both ring-fraction and module-fraction representatives.

Facts & Assumptions

Given: A commutative ring $R$ , a multiplicative subset $S \subseteq R$ , a left $R$ -module $M$ , and equalities $a / u = a^{'} / u^{'}$ in $S^{- 1} R$ and $m / s = m^{'} / s^{'}$ in $S^{- 1} M$ .

[L1]

In $S^{- 1} M$ , the equality $x / r = y / t$ means that $q (t x - r y) = 0$ for some $q \in S$ , and the proposed scalar action is $(b / v) (x / r) = b x / (v r)$ (Localisation of a module at a multiplicative subset).

[L2]

In $S^{- 1} R$ , the equality $b / v = c / w$ means that $q (w b - v c) = 0$ for some $q \in S$ (Multiplicative subsets and the localisation $S^{- 1} R$ as equivalence classes of fractions).

Proof

technique · direct

1.1givenL1L2choose

By [L1] and [L2], choose $v, w \in S$ with $v (u^{'} a - u a^{'}) = 0$ and $w (s^{'} m - s m^{'}) = 0$ .

2.1step 1.1algebra

Multiplying the module-fraction equality by $a u v$ and the ring-fraction equality by $u s m^{'} w$ , then adding, gives $u v w (u^{'} s^{'} a m - u s a^{'} m^{'}) = a u^{'} v w (s^{'} m - s m^{'}) + u s m^{'} v w (u^{'} a - u a^{'}) = 0.$ So $u v w (u^{'} s^{'} a m - u s a^{'} m^{'}) = 0$ .

3.1step 2.1L1∎

Step 2.1 is exactly the relation witnessing $a m / (u s) = a^{'} m^{'} / (u^{'} s^{'})$ , so the scalar action is independent of representatives.

Depends on

Used by

Universal property of localisation for modules Theorem

Cited to discharge well-definedness by Localisation of a module at a multiplicative subset.

Dependency tree · two levels

6 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., Section 12 (standard reference, not scraped)
The Stacks Project, Section 10.9: Localization (standard reference, not scraped)