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.

Addition of localised module fractions is independent of representatives

Statement

If $m / s = m^{'} / s^{'}$ and $n / t = n^{'} / t^{'}$ in $S^{- 1} M$ , then $\frac{t m + s n}{s t} = \frac{t^{'} m^{'} + s^{'} n^{'}}{s^{'} t^{'}} .$ So the addition formula of Localisation of a module at a multiplicative subset is independent of the chosen representatives.

Facts & Assumptions

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

[L1]

In $S^{- 1} M$ , the equality $x / u = y / v$ means that $q (v x - u y) = 0$ for some $q \in S$ , and addition is defined by $(x / u) + (y / v) = (v x + u y) / (u v)$ (Localisation of a module at a multiplicative subset).

[L2]

The relation defining $S^{- 1} M$ is an equivalence relation (The module-fraction relation is an equivalence relation).

Proof

technique · direct

1.1givenL1L2choose

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

2.1step 1.1algebra

Multiplying the first equality by $v t t^{'}$ and the second by $u s s^{'}$ and then adding gives $u v (s^{'} t^{'} (t m + s n) - s t (t^{'} m^{'} + s^{'} n^{'})) = 0$ .

3.1step 2.1L1∎

Step 2.1 is exactly the relation witnessing $(t m + s n) / (s t) = (t^{'} m^{'} + s^{'} n^{'}) / (s^{'} t^{'})$ , so the addition formula 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

4 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)