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.
Affine-local flatness
Statement
Assume the Axiom of Choice for the converse direction of the second assertion; the pointwise equivalence and the forward direction use no choice.
Let be a morphism of schemes, let and be affine open subschemes with , and let correspond to with . Then is flat at if and only if is flat over . Moreover is flat at every point of if and only if is flat over , and these tests agree when the affine charts are refined to smaller affine charts.
Facts & Assumptions
Given: A morphism , affine open subschemes and with , and a point with corresponding primes , ; AC is assumed only for the converse of the on- assertion.
For there is a canonical isomorphism (The stalk of the affine structure sheaf at a prime is A_p).
A morphism is flat at when is a flat module over for the local ring map, and flat when this holds at every point of (Flat morphism of schemes).
For an -module : is flat if and only if for every finitely generated ideal the multiplication map is injective (Flatness is equivalent to preserving injections and to the ideal and finitely generated ideal tests, criterion 4).
Let be a multiplicative set. The localisation is a flat -algebra, and if is a flat -module then is flat over (Every localization is flat, and localizing a flat module preserves flatness).
Localisation is exact: a short exact sequence of -modules remains short exact after applying ; consequently kernels and images localise (Localisation of modules is exact).
The spectrum construction is a contravariant equivalence between rings and affine schemes, so an open immersion of affine schemes is induced by a ring map , and affine charts of a morphism compose to ring maps with compatible localisations (Affine schemes are contravariantly equivalent to commutative rings).
Assume the Axiom of Choice: every proper ideal of a nonzero commutative ring is contained in a maximal ideal (In a nonzero commutative ring, every proper ideal is contained in a maximal ideal, The Axiom of Choice).
Proof
Fix affine opens and with ; by [F6] the restriction corresponds to a ring map . Let correspond to and put , so corresponds to . By [F1], and , and the local ring map is the localisation of at . Hence by [F2], is flat at if and only if is flat over .
If is flat over , then is flat over for every : localising at the multiplicative set gives the flat -module , and localising that further at the image of gives , flat over by [F4] applied twice. Thus flat over implies is flat at every point of .
Conversely assume flat over for every . To prove flat over it suffices by [F3] to show that for every finitely generated ideal the kernel of is zero. By exactness of localisation [F5], for we have , and this vanishes: is flat over , so the multiplication map is injective by [F3], and . If , then choosing a maximal ideal of containing the annihilator of a nonzero element of — here the Axiom of Choice is used, [F7] — produces with . Hence for every finitely generated ideal , and is flat over by [F3].
The last sentence of the statement: if , is a refinement of affine charts with , then for the local rings computed in the small and large charts are canonically the same local rings by [F1] applied to the two affine descriptions of the same open neighbourhoods, so the test of step 1.1 gives the same answer for the two charts. Hence flatness of at is independent of the chosen affine charts, flatness on is exactly flatness of over by steps 1.2 and 2.1, and the affine tests are compatible on refinements. [F1, step 1.1, step 1.2, step 2.1]
Depends on
- Flat morphism of schemes
- Flatness is equivalent to preserving injections and to the ideal and finitely generated ideal tests
- Affine schemes are contravariantly equivalent to commutative rings
- Localisation of modules is exact
- The stalk of the affine structure sheaf at a prime is A_p
- Every localization is flat, and localizing a flat module preserves flatness
- The Axiom of Choice
- In a nonzero commutative ring, every proper ideal is contained in a maximal ideal
Used by
- A flat family with a nodal special fibre is not smooth at the node Counterexample
- Flat and finite type is not open without finite presentation Counterexample
- Frobenius on the affine line is finite flat but not smooth Counterexample
- Polynomial rings are flat and smooth Example
- The family xy=t Example
- Flatness is stable under arbitrary base change Lemma
- Flatness is stable under composition Lemma
- Flat finite-presentation morphisms are open Theorem
- Generic flatness for finite type morphisms over Noetherian integral bases Theorem
Dependency tree · two levels
36 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
- The Stacks Project, Morphisms of Schemes, Section 29.25 (standard reference, not scraped)
- The Stacks Project, Commutative Algebra, Section 10.39 and Lemma 10.18.7 (standard reference, not scraped)