Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01
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.

Every localization is flat, and localizing a flat module preserves flatness

Statement

Let R be a commutative ring and let SR be a multiplicative set.

  1. The localization S1R is a flat R-algebra.
  2. If M is an S1R-module, then M is flat over R if and only if it is flat over S1R.
  3. In particular, if N is a flat R-module, then S1N is flat over S1R.

Facts & Assumptions

Given: A commutative ring R and a multiplicative subset SR.

[L1]

Flatness means exactness of tensoring (Flat and faithfully flat modules and ring homomorphisms).

[L2]

Localization of modules preserves exact sequences (Localisation of modules is exact).

[L3]

Localization of modules is tensor product: S1NS1RRN (Localisation of modules is extension of scalars).

[L4]

Localization at a prime ideal is the special case S=Rp (Localisation at a prime ideal: Rp=(Rp)1R).

Proof

technique · direct
1.1

For an exact sequence ABC of R-modules, [L2] gives an exact sequence S1AS1BS1C. By [L3] this is (S1RRA)(S1RRB)(S1RRC), so S1R is flat over R by [L1].

L1L2L3given
2.1

Let M be an S1R-module. If M is flat over S1R, then for any exact sequence over R we first tensor with S1R as in step 1.1 and then tensor over S1R with M; the result is exact, so M is flat over R. Conversely, if M is flat over R, then every exact sequence of S1R-modules is in particular exact over R, and tensoring it with M over R agrees with tensoring over S1R because the scalars already act through the localization. Hence M is flat over S1R.

L1L3step 1.1algebra
3.1

If N is flat over R, then S1NS1RRN by [L3]. Applying step 2.1 to the S1R-module S1N proves it is flat over S1R.

L3step 2.1
3.2

Step 2.1 applies in particular to localization at a prime ideal by [L4].

L4
4.1

Therefore all three claims hold.

algebra

Depends on

Used by

Dependency tree · two levels

15 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