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 S⊆R be a multiplicative set.

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

Facts & Assumptions

Given: A commutative ring R and a multiplicative subset S⊆R.

[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: S−1N≅S−1R⊗RN (Localisation of modules is extension of scalars).

[L4]

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

Proof

technique · direct
1.1L1L2L3given

For an exact sequence A→B→C of R-modules, [L2] gives an exact sequence S−1A→S−1B→S−1C. By [L3] this is (S−1R⊗RA)→(S−1R⊗RB)→(S−1R⊗RC), so S−1R is flat over R by [L1].

2.1L1L3step 1.1algebra

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

3.1L3step 2.1

If N is flat over R, then S−1N≅S−1R⊗RN by [L3]. Applying step 2.1 to the S−1R-module S−1N proves it is flat over S−1R.

3.2L4

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

4.1algebra∎

Therefore all three claims hold.

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