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.
Subalgebra generated by a subset, algebras of finite type, and module-finite algebras
Definition
Let be a commutative ring and let be a commutative -algebra with structure map (Algebras over a commutative ring, central structure maps, and algebra homomorphisms).
The subalgebra generated by finitely many elements. Let and . Iterating the universal property of a polynomial ring (Universal property of : a coefficient homomorphism and the image of determine a unique ring homomorphism) along the recursion of Polynomial rings in finitely many commuting indeterminates by iteration gives a unique unital ring homomorphism
that agrees with on constants and sends to for each ; at each step of the recursion the one-variable universal property supplies existence and uniqueness of the extension, and at the map is itself. Its image is written and is called the -subalgebra of generated by . It is a subring of containing , and it is the smallest such subring containing , since any subring with those properties is closed under the sums and products that make up a polynomial expression. At it is , the image of in .
Finite type. is of finite type over , equivalently a finitely generated -algebra, when for some and some . Equivalently, is isomorphic as an -algebra to a quotient for some and some ideal : the map above is then surjective, and First isomorphism theorem for rings: identifies with ; conversely the composite of the canonical projection with the inclusion of the indeterminates exhibits any such quotient as generated by the residues of .
Module-finite. is module-finite over , equivalently a finite -algebra, when is finitely generated as an -module (Generated submodule, cyclic and finitely generated modules, module basis and free module) for the action .
Module-finite implies finite type. If generate as an -module then , being a subring of that contains and every , contains every -linear combination and hence all of ; so . The converse fails, and the companion examples page carries a witness.
Remarks
-
Three conditions, three rings. "Finitely generated" is ambiguous on its own: an ideal may be finitely generated as an ideal, a module as a module, and an algebra as an algebra, and the three are different requirements. This page writes "of finite type" for the algebra condition and "module-finite" for the module condition, and always names the ring over which the condition is taken. Sources differ in vocabulary: Totaro and Milne write "finite algebra" for what is called module-finite here, and Altman–Kleiman write "module finite" and "algebra finite".
-
The generators need not be algebraically independent. Nothing above asks to be injective. When it is, is a polynomial ring and the ideal is zero; that is a special case, not the definition.
-
The empty list is allowed and is not the same as . At the subalgebra generated is , which is a quotient of rather than a copy of it unless is injective.
Depends on
- Algebras over a commutative ring, central structure maps, and algebra homomorphisms
- Generated submodule, cyclic and finitely generated modules, module basis and free module
- Polynomial rings in finitely many commuting indeterminates by iteration
- Universal property of $R[x]$: a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism
- First isomorphism theorem for rings: $R/\ker f\cong\operatorname{im}f$
Used by
- Every algebra of finite type over a Noetherian ring is a Noetherian ring Corollary
- Every algebra of finite type over a Noetherian ring is finitely presented Corollary
- Every algebra of finite type over a principal ideal domain is a Noetherian ring Corollary
- The Artin–Tate lemma with integrality in place of module finiteness Corollary
- Finitely presented modules and finitely presented algebras Definition
- An algebra that is finite dimensional as a vector space over a field is a Noetherian ring Example
- Identifying the coefficient algebra in a concrete Artin–Tate tower Example
- k[x,y]/(xy) and ℤ[x]/(x²-2) are Noetherian without classifying their ideals Example
- The subalgebra k[x,xy,xy²,…] of k[x,y] is not Noetherian Example
- The symmetric polynomials as the invariant ring of the symmetric group, seen through Noether's finiteness theorem Example
- A subalgebra generated by finitely many integral elements is module-finite 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 module-finite algebra over a Noetherian ring is a Noetherian ring, and so is every ring between the two Theorem
- Artin–Tate lemma: an intermediate ring over which a finite-type algebra is module-finite is itself of finite type Theorem
- Noether's finiteness theorem: the invariants of a finite group acting on a finite-type algebra over a Noetherian ring form an algebra of finite type 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
- B. Totaro, Commutative Algebra (Michaelmas 2011), notes by Z. Norwood, §8 (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, §1 (standard reference, not scraped)
- A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., §4 and §16 (standard reference, not scraped)