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.
Integral extensions are transitive
Statement
Let and be integral ring maps. Then the composite map is integral.
Facts & Assumptions
Given: Integral ring maps and .
A ring map is integral exactly when every element of the target ring is integral over the source ring (Integral ring maps and integral extensions).
A subalgebra generated by finitely many integral elements is module-finite over the base ring (A subalgebra generated by finitely many integral elements is module-finite).
If is module-finite over and is module-finite over , then is module-finite over (Module finiteness is transitive along a tower of algebras).
For a nonzero commutative ring and in an -algebra, the following are equivalent: is integral over ; is a finitely generated -module; and there exists a faithful -module finitely generated over (Integrality and finite-module characterizations for one element).
Proof
If , then , so every unital image of is the zero ring; hence and then , making the composite integral trivially. For the rest of the proof assume .
Let . By [L1], the element is integral over , so there is a monic equation with . Again by [L1], each coefficient is integral over , so [L2] makes the -subalgebra module-finite over .
The same equation for has coefficients in , so is integral over . Because is an -subalgebra of , it contains the image of , so it is nonzero. Therefore [L4] makes a finitely generated -module, and then [L3] gives that is a finitely generated -module.
The ring is a faithful module over the subring , and step 2.1 shows that this faithful -module is finitely generated over . By [L4], is integral over . Since was arbitrary, the map is integral.
Depends on
Used by
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
- Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem (10.27) (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, Proposition 6.4 (standard reference, not scraped)