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.
Modules over a field are projective, flat, and injective
Statement
Assume the Axiom of Choice. Every module over a field is free, hence projective and flat, and is also injective.
Proof
Given: a -vector space , under Choice.
By Every vector space has a basis, Choice supplies a basis of . It identifies with a direct sum of copies of , so is free and therefore projective and flat.
Under Choice a subspace has a vector-space complement. Therefore every map from a subspace into extends across an inclusion, which is the injectivity criterion.
Depends on
Used by
- Kunneth over a field Corollary
- Geometric genus of a singular curve Definition
- Over a field the cross product itself is a natural isomorphism Example
- Riemann-Hurwitz for a tame double cover with 2r branch points Example
- RᵖG(R^qF) is the E1 page False statement
- Finite-type field extensions with zero Ω Lemma
- Fixed loci are closed and a normal subgroup fixing a point fixes the orbit closure Lemma
- Flat field extension commutes with coherent cohomology Lemma
- Multiplicity one is the smooth hypersurface test Lemma
- Collapsed vector-space spectral sequences split noncanonically Proposition
- Line bundles of degree at least 2g are base-point-free Theorem
- Line bundles of degree at least 2g+1 are very ample Theorem
- Locally standard smooth iff flat with geometrically regular fibres Theorem
- Smooth proper curves, dominant morphisms and function fields Theorem
Dependency tree · two levels
19 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
- Weibel, An Introduction to Homological Algebra (standard reference, not scraped)