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.
Assuming the Axiom of Choice, generators modulo an ideal in the Jacobson radical lift to generators
Statement
Assume the Axiom of Choice.
Let be a commutative ring, let satisfy , and let be a finitely generated left -module. If elements generate , then generate .
Facts & Assumptions
Given: The Axiom of Choice (The Axiom of Choice), a commutative ring , an ideal with , a finitely generated left -module , and elements whose images generate .
Under AC, if a finite module satisfies and , then (Assuming the Axiom of Choice, Nakayama's lemma); applying this supplier in step 2.1 is the sole inherited use of AC here.
The submodule consists of finite sums of products with and (The submodule generated by products of elements of an ideal with elements of a module ).
A finite list of elements generates the submodule it spans (Generated submodule, cyclic and finitely generated modules, module basis and free module).
Proof
Let be the submodule of generated by . The hypothesis on means every element of is congruent modulo to an element of , so .
Passing to the quotient , step 1.1 gives . Since is a quotient of the finite module , it is finite, so [L1] gives .
The equality means , so generate .
Depends on
Used by
- Assuming the Axiom of Choice, minimal generators over a local ring are exactly residue-field bases Corollary
- Euler characteristic in a proper flat family is locally constant Corollary
- For a nonzero finite module and an ideal of definition, Hilbert-Samuel multiplicity is a positive integer Corollary
- Upper semicontinuity of fibre cohomology dimensions Corollary
- Contact order of two regular components at a point Definition
- Blowing up a multiple point separates pairwise transverse components Lemma
- Embedded flat deformations of a smooth hypersurface are deformations of its equation Lemma
- embedding dimension is minimal maximal ideal generator number Lemma
- Finite étale algebras have finite locally free underlying modules Lemma
- Finite étale algebras over a complete local ring are determined by reduction Lemma
- Finite-free local criterion for cohomology and base change Lemma
- regular system of parameters equivalent basis Lemma
- The Cohen map is surjective modulo every power of the maximal ideal Lemma
- A finite flat module over a local ring is free Theorem
- Cohomology and base change for proper flat coherent families Theorem
- Finite étale algebras lift uniquely through nilpotent thickenings Theorem
- Finite étale covers of a projective flat family over a complete DVR lift uniquely Theorem
- For an R-finite module over a local map, flatness modulo I and injectivity of I ⊗ M → M imply flatness Theorem
Dependency tree · two levels
12 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
- J. S. Milne, A Primer of Commutative Algebra, v4.03, Lemma 3.9 (standard reference, not scraped)
- The Stacks Project, Lemma 10.20.1 (standard reference, not scraped)