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.
The submodule generated by a subset consists of the finite -linear combinations of that subset
Statement
Let be a ring, let be a left -module and let . Then the submodule generated by (Generated submodule, cyclic and finitely generated modules, module basis and free module) is the set of finite -linear combinations of elements of :
where the term with is the empty sum . In particular . Commutativity of is not used, and the elements are not required to be distinct.
Facts & Assumptions
Given: A ring , a left -module and a subset . Write for the set displayed in the Statement.
The submodule generated by is , the family being nonempty because ; thus is the smallest submodule of containing (Generated submodule, cyclic and finitely generated modules, module basis and free module).
For a left -module , a nonempty subset is a submodule if and only if for all and (The one-step submodule criterion; intersections and sums of submodules are submodules).
A left -module is an abelian group with an action satisfying , , and (Unital left and right modules over a ring; unqualified module means left module).
In a commutative ring, consists of finite sums , and (In a commutative ring, consists of finite sums , and ).
Proof
Let be the set of all sums with , and , the value at being the empty sum ; in particular , so is nonempty even when is empty.
Every lies in , being the one-term sum , which equals by the unitality axiom of a module; hence .
is a submodule of : it is nonempty, and for and , in the element is the sum , again a finite -linear combination of elements of with terms, so and the submodule criterion applies.
Every submodule with contains : each lies in , so repeated use of the submodule criterion [L2] puts every and every finite sum of those elements in ; the case gives .
: by steps 2.1 and 2.2 the set is one of the submodules over which the intersection defining runs, so ; and is itself a submodule containing , so step 2.3 applied to it gives .
Two consequences follow by reading the description at its extreme cases. Taking leaves only the empty sum, so . Taking to be the regular module over a commutative , where the submodules are the ideals, the description becomes the finite-sum description of the ideal generated by , so the two agree and this lemma extends that one from ideals to modules rather than competing with it.
Remarks
-
Unitality is where the containment comes from. Step 2.1 writes , which is available because Unital left and right modules over a ring; unqualified module means left module builds into the definition of a module. Over a non-unital action the set of finite -linear combinations need not contain , and then it is not the generated submodule.
-
No finiteness is assumed of . Each element of carries its own finite list of coefficients and elements; different elements may use different lists, and no bound on the length is claimed.
Depends on
- Generated submodule, cyclic and finitely generated modules, module basis and free module
- The one-step submodule criterion; intersections and sums of submodules are submodules
- Unital left and right modules over a ring; unqualified module means left module
- In a commutative ring, $(S)$ consists of finite sums $\sum r_i s_i$, and $(a)=Ra$
Used by
- Over a Noetherian ring the homomorphism module between two finitely generated modules is finitely generated Corollary
- A subring that admits a module retraction from a Noetherian ring is Noetherian Lemma
- Every generating set of a finitely generated module contains a finite generating subset Lemma
- In the Artin–Tate setup the intermediate ring is module-finite over the coefficient subalgebra Lemma
- Module finiteness is transitive along a tower of algebras Lemma
- The Artin–Tate coefficient subalgebra is a Noetherian algebra of finite type Lemma
- A commutative ring is Noetherian exactly when every ideal is finitely generated, exactly when its ideals satisfy the ascending chain condition, and exactly when every nonempty set of ideals has a maximal member Theorem
- Artin–Tate lemma: an intermediate ring over which a finite-type algebra is module-finite is itself of finite type Theorem
- Over a Noetherian ring a module is Noetherian exactly when it is finitely generated, exactly when it is finitely presented Theorem
Dependency tree · two levels
13 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
- A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., §4 and §16 (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, §3 (standard reference, not scraped)