Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-29
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 AB and BC be integral ring maps. Then the composite map AC is integral.

Facts & Assumptions

Given: Integral ring maps AB and BC.

[L1]

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).

[L2]

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).

[L3]

If B is module-finite over A and M is module-finite over B, then M is module-finite over A (Module finiteness is transitive along a tower of algebras).

[L4]

For a nonzero commutative ring R and c in an R-algebra, the following are equivalent: c is integral over R; R[c] is a finitely generated R-module; and there exists a faithful R[c]-module finitely generated over R (Integrality and finite-module characterizations for one element).

Proof

technique · direct
1.1

If A=0, then 1A=0A, so every unital image of A is the zero ring; hence B=0 and then C=0, making the composite integral trivially. For the rest of the proof assume A0.

L1givenalgebra
1.2

Let cC. By [L1], the element c is integral over B, so there is a monic equation cn+bn1cn1++b0=0 with biB. Again by [L1], each coefficient bi is integral over A, so [L2] makes the A-subalgebra D:=A[b0,,bn1] module-finite over A.

L1L2given
2.1

The same equation for c has coefficients in D, so c is integral over D. Because D is an A-subalgebra of B, it contains the image of 1A=1B, so it is nonzero. Therefore [L4] makes D[c] a finitely generated D-module, and then [L3] gives that D[c] is a finitely generated A-module.

L3L4step 1.2given
3.1

The ring D[c] is a faithful module over the subring A[c], and step 2.1 shows that this faithful A[c]-module is finitely generated over A. By [L4], c is integral over A. Since cC was arbitrary, the map AC is integral.

L4step 2.1given

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