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 be a commutative ring and let be a multiplicative set.
- The localization is a flat -algebra.
- If is an -module, then is flat over if and only if it is flat over .
- In particular, if is a flat -module, then is flat over .
Facts & Assumptions
Given: A commutative ring and a multiplicative subset .
Flatness means exactness of tensoring (Flat and faithfully flat modules and ring homomorphisms).
Localization of modules preserves exact sequences (Localisation of modules is exact).
Localization of modules is tensor product: (Localisation of modules is extension of scalars).
Localization at a prime ideal is the special case (Localisation at a prime ideal: ).
Proof
For an exact sequence of -modules, [L2] gives an exact sequence By [L3] this is so is flat over by [L1].
Let be an -module. If is flat over , then for any exact sequence over we first tensor with as in step 1.1 and then tensor over with ; the result is exact, so is flat over . Conversely, if is flat over , then every exact sequence of -modules is in particular exact over , and tensoring it with over agrees with tensoring over because the scalars already act through the localization. Hence is flat over .
If is flat over , then by [L3]. Applying step 2.1 to the -module proves it is flat over .
Step 2.1 applies in particular to localization at a prime ideal by [L4].
Therefore all three claims hold.
Depends on
Used by
- A finite product of principal localizations covering the spectrum is faithfully flat Example
- A fraction field is flat over its domain and may fail to be projective Example
- A proper localization is flat but need not be faithfully flat Example
- A module is flat if and only if all prime localizations are flat, equivalently all maximal localizations are flat Theorem
- Every flat ring map satisfies going down Theorem
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
- Stacks Project, Lemma 10.39.18 (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, §11 (standard reference, not scraped)