Alphabeta MathHow 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.
Under the stated choice boundary, free modules are projective and hence flat
Statement
Let be a commutative ring and let be a free -module with basis indexed by .
- Assuming the Axiom of Choice, is projective and therefore flat.
- If is finite, only finite choice is needed for projectivity; if , no choice is needed.
- Regardless of choice, is flat, because tensoring with is a direct sum of copies of the identity tensor functor.
Facts & Assumptions
Given: A commutative ring and a free -module with basis indexed by .
Under AC every free module is projective; a finite basis requires only finite choice, and an empty basis requires none (Free modules are projective, with the exact choice boundary).
Every projective module over a commutative ring is flat without choice (Every projective module over a commutative ring is flat).
Tensor products commute with arbitrary direct sums in either variable; in particular (Tensor products commute with arbitrary direct sums).
The regular module is a tensor unit (The regular module is a tensor unit: and ).
Proof
Under AC, [L1] makes projective and [L2] then makes it flat. The refined finite and empty-basis choice bounds are exactly those stated in [L1].
Independently of AC, write . By [L3] and [L4], tensoring an exact sequence with gives the direct sum, over , of the original exact sequence; kernels and images are computed coordinatewise, so the result remains exact. Thus is flat without any choice principle.
Step 1.1 establishes the projective route with its precise choice boundary, while step 1.2 establishes flatness unconditionally; the two routes are logically distinct.
Depends on
Used by
- Frobenius on the affine line is finite flat but not smooth Counterexample
- A polynomial algebra is free and therefore faithfully flat over its coefficient ring Example
- An upper jump of h0 in a flat projective family Example
- Polynomial rings are flat and smooth Example
- Flatness criteria and canonical epimorphisms from flat abelian sheaves Lemma
- High-degree section module is finite graded Lemma
- Standard smooth algebras are finitely presented and flat Lemma
- Support dimension under field extension Lemma
- Modules over a field are projective, flat, and injective Proposition
- Flatness does not force isomorphic or smooth fibres Remark
- A short exact sequence with flat quotient remains short exact after tensoring Theorem
- Degree of the coherent Hilbert polynomial Theorem
- Euler characteristic is a Hilbert polynomial Theorem
- Euler-Poincare formula for finite free complexes Theorem
- Every matrix over a PID has a Smith normal form Theorem
- Finite and finite type etale schemes over an algebraically closed field Theorem
- Functoriality and coefficient long exact sequences for Hochschild homology Theorem
- Generic flatness for finite type morphisms over Noetherian integral bases Theorem
Dependency tree · two levels
17 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
- C. Dennis, Week 4 on tensor products and flatness (standard reference, not scraped)
- W. Li, Commutative Algebra, Lectures 9-10 (standard reference, not scraped)