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.
Flatness is equivalent to preserving injections and to the ideal and finitely generated ideal tests
Statement
Let be a commutative ring and let be an -module. The following are equivalent:
- is flat.
- For every injection , the induced map is injective.
- For every ideal , the multiplication map , , is injective.
- The map in claim 3 is injective for every finitely generated ideal .
Facts & Assumptions
Given: A commutative ring and an -module .
Flatness means that preserves exact sequences (Flat and faithfully flat modules and ring homomorphisms).
Tensoring is right exact (Tensoring is right exact).
Tensor products commute with direct sums and ; consequently (Tensor products commute with arbitrary direct sums, The regular module is a tensor unit: and ).
A finite list in a module determines a homomorphism taking to ; if the list generates , this map is surjective. Also (The free module on a set and its standard basis, Universal property of the free module on a set).
In a commutative ring, every submodule of the regular module is an ideal (Left, right and two-sided ideals).
A tensor product is the quotient of the free -module on pairs by the subgroup generated by the additive and balance relations (The tensor product from the additive group underlying the free -module on , elementary tensors, and finite tensor sums). Consequently, a tensor expression and a derivation that it is zero involve only finitely many generators and defining relations.
Proof
Claim 1 implies claim 2 by applying [L1] to ; claim 2 implies claim 3 by taking the inclusion and using ; claim 3 implies claim 4 by restriction to finitely generated ideals.
Assume claim 4. Claim 3 follows: an element is represented by finitely many coefficients from , hence comes from for the finitely generated ideal they generate; if its image in is zero, injectivity for makes its representative zero, so .
Let be injective and let map to zero. By [L6], the tensor uses finitely many elements of , and a derivation of its zero image uses only finitely many generators and defining relations in . Hence there are finitely generated submodules and with for which comes from an element killed in .
Under claim 3, for every submodule , the map is injective, by induction on . For it is the unique map ; for it is claim 3 by [L5].
Present using [L4], and let be the inverse image of . Right exactness identifies with and with the quotient of by .
For the induction step, let , put , and let be the image of in . Tensoring the exact rows and gives right-exact rows by [L2]; the left and right vertical maps are injective by the case and the induction hypothesis from step 2.1.
If maps to zero in , its image in maps to zero in and hence is zero by the right vertical injection in step 3.1. Right exactness of the top row lifts from some . The image of in maps to the zero image of in ; the left vertical injection in step 3.1 makes , and therefore . This completes the induction of step 2.1.
By step 4.1, both and inject into . Therefore the induced map of the quotients in step 2.2 is injective, so . This proves claim 2 from claim 4.
Finally claim 2 and right exactness [L2] imply claim 1: for an exact sequence, replace the left map by the injection of its image into the middle term; tensoring preserves that injection by claim 2 and preserves the remaining image and cokernel statements by right exactness.
Steps 1.1 through 6.1 prove the cycle of equivalences. The zero ideal, , and zero module cases occur explicitly in steps 1.2 and 2.1; no choice is made, and both directions of every equivalence have been supplied.
Depends on
- Flat and faithfully flat modules and ring homomorphisms
- Tensoring is right exact
- Tensor products commute with arbitrary direct sums
- The regular module is a tensor unit: $R\otimes_RN\cong N$ and $M\otimes_RR\cong M$
- The free module on a set and its standard basis
- Universal property of the free module on a set
- Left, right and two-sided ideals
- The tensor product $M\otimes_R N$ from the additive group underlying the free $\mathbb Z$-module on $M\times N$, elementary tensors, and finite tensor sums
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 47 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Stacks Project, Lemma 10.39.5 (standard reference, not scraped)