TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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 $A \to B$ and $B \to C$ be integral ring maps. Then the composite map $A \to C$ is integral.

Facts & Assumptions

Given: Integral ring maps $A \to B$ and $B \to C$ .

[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.1L1givenalgebra

If $A = 0$ , then $1_{A} = 0_{A}$ , 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 $A \neq 0$ .

1.2L1L2given

Let $c \in C$ . By [L1], the element $c$ is integral over $B$ , so there is a monic equation $c^{n} + b_{n - 1} c^{n - 1} + \dots + b_{0} = 0$ with $b_{i} \in B$ . Again by [L1], each coefficient $b_{i}$ is integral over $A$ , so [L2] makes the $A$ -subalgebra $D : = A [b_{0}, \dots, b_{n - 1}]$ module-finite over $A$ .

2.1L3L4step 1.2given

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 $1_{A} = 1_{B}$ , 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.

3.1L4step 2.1given∎

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 $c \in C$ was arbitrary, the map $A \to C$ is integral.

Integral extensions are transitive

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources