[proofplan] Fix $c \in C$ and a monic polynomial $f \in B[x]$ with $f(c) = 0$, witnessing integrality of $c$ over $B$. Let $B_0 = A[b_0, \ldots, b_N]$ be the $A$-algebra generated by the coefficients of $f$. Because each $b_i$ is integral over $A$ (by the integrality of $B$ over $A$), [Integral Implies Finitely Generated](/theorems/1565) shows $B_0$ is finitely generated as an $A$-module. The element $c$ is integral over $B_0$ (since $f$, now viewed as lying in $B_0[x]$, is a monic polynomial annihilating $c$), so [Integral Implies Finitely Generated](/theorems/1565) again shows $B_0[c]$ is finitely generated over $B_0$. Transitivity of finite generation gives $B_0[c]$ finitely generated over $A$; [Finitely Generated Implies Integral](/theorems/1566) then produces a monic polynomial in $A[x]$ annihilating $c$. Since $c$ was arbitrary, $C$ is integral over $A$. [/proofplan] [step:Fix $c \in C$ and extract a monic polynomial witnessing integrality of $c$ over $B$] Let $c \in C$. By hypothesis, $C$ is integral over $B$, so $c$ is integral over $B$: there exist $N \geq 1$ and $b_0, b_1, \ldots, b_{N-1} \in B$ with \begin{align*} f(x) = x^N + b_{N-1} x^{N-1} + \cdots + b_1 x + b_0 \in B[x], \qquad f(c) = 0. \end{align*} (We write $b_N = 1$ for uniformity but will not usually include it in the list of non-trivial coefficients since it is already in $A \subseteq B$.) [guided] Fix an arbitrary $c \in C$. Our goal is to show $c$ is integral over $A$, i.e., to produce a monic polynomial $g \in A[x]$ with $g(c) = 0$. The difficulty is that we only have a monic polynomial $f \in B[x]$ with $f(c) = 0$ — the coefficients live in the larger ring $B$, not in $A$. By hypothesis, $C$ is integral over $B$, so $c$ is integral over $B$: there exist $N \geq 1$ and $b_0, b_1, \ldots, b_{N-1} \in B$ with \begin{align*} f(x) = x^N + b_{N-1} x^{N-1} + \cdots + b_1 x + b_0 \in B[x], \qquad f(c) = 0. \end{align*} These coefficients $b_0, \ldots, b_{N-1}$ are finitely many elements of $B$. Because $B$ is integral over $A$ (the other hypothesis), each $b_i$ is integral over $A$. This is the toehold we will exploit. [/guided] [/step] [step:Form $B_0 = A[b_0, \ldots, b_{N-1}]$ and show it is finitely generated over $A$] Let $B_0 = A[b_0, b_1, \ldots, b_{N-1}] \subseteq B$, the $A$-subalgebra generated by the coefficients of $f$. We apply [Integral Implies Finitely Generated](/theorems/1565), part (2), to the ring extension $A \subseteq B_0$. The hypotheses are: 1. **Ring extension**: $A \subseteq B_0 \subseteq B$, and $B_0$ is a commutative ring (a subring of the commutative ring $B$). 2. **$B_0 = A[s_1, \ldots, s_n]$ with each $s_i$ integral over $A$**: here $n = N$, $s_i = b_{i-1}$; each $b_{i-1}$ is integral over $A$ because $b_{i-1} \in B$ and $B$ is integral over $A$ by hypothesis. The theorem concludes $B_0$ is finitely generated as an $A$-module. [guided] Collect the coefficients of $f$ into an $A$-algebra: \begin{align*} B_0 := A[b_0, b_1, \ldots, b_{N-1}] \subseteq B. \end{align*} This is the smallest $A$-subalgebra of $B$ containing $\{b_0, \ldots, b_{N-1}\}$. We claim $B_0$ is finitely generated as an $A$-module. This is the content of [Integral Implies Finitely Generated](/theorems/1565), part (2), which states: if $S = R[s_1, \ldots, s_n]$ with each $s_i$ integral over $R$, then $S$ is finitely generated as an $R$-module. We verify the hypotheses: - **Ring extension $A \subseteq B_0$**: $A$ is a subring of $B_0$ by construction, and $B_0$ is a commutative ring (a subring of the commutative ring $B$). - **Each generator is integral over $A$**: the generators of $B_0$ over $A$ are $b_0, b_1, \ldots, b_{N-1}$. By the hypothesis "$B$ is integral over $A$", every element of $B$ is integral over $A$, so each $b_i$ is integral over $A$. Both hypotheses hold, so the theorem applies: $B_0$ is finitely generated as an $A$-module. Why did we isolate the coefficients $b_0, \ldots, b_{N-1}$ instead of using all of $B$? Because $B$ itself need not be finitely generated as an $A$-module (integrality does not imply finite generation as a module — only for finitely-generated sub-algebras). By restricting to the finitely many $b_i$ we actually need, we reduce to a situation where part (2) of [Integral Implies Finitely Generated](/theorems/1565) directly applies. [/guided] [/step] [step:Show that $c$ is integral over $B_0$, and hence $B_0[c]$ is finitely generated over $B_0$] The polynomial $f \in B[x]$ has coefficients $b_0, \ldots, b_{N-1} \in B_0$ by construction of $B_0$, and its leading coefficient $1$ also lies in $B_0$ (which contains $A \ni 1$). Hence $f \in B_0[x]$ via the inclusion $B_0[x] \hookrightarrow B[x]$, and $f$ remains monic (its leading coefficient is $1$, the identity of both $B_0$ and $B$). Since $f(c) = 0$ in $B$ (and hence in $C \supseteq B$), we conclude that $c$ is integral over $B_0$. We apply [Integral Implies Finitely Generated](/theorems/1565), part (1), to the ring extension $B_0 \subseteq B_0[c] \subseteq C$. The hypotheses: 1. **Ring extension**: $B_0 \subseteq B_0[c]$, with $B_0[c]$ a commutative ring (a subring of the commutative ring $C$). 2. **$B_0[c]$ is generated over $B_0$ by a single element $c$ that is integral over $B_0$**: verified above. The theorem concludes $B_0[c]$ is finitely generated as a $B_0$-module. [guided] The polynomial $f(x) = x^N + b_{N-1} x^{N-1} + \cdots + b_0$ has coefficients $b_0, \ldots, b_{N-1}$ all lying in $B_0$ (this was the point of the construction of $B_0$), and leading coefficient $1 \in B_0$. So $f$, originally a polynomial in $B[x]$, can equally be regarded as a polynomial in $B_0[x]$ via the inclusion $B_0[x] \subseteq B[x]$. Monicity is preserved because the leading coefficient is still $1$. Since $f(c) = 0$, the element $c$ is integral over $B_0$. Now we apply [Integral Implies Finitely Generated](/theorems/1565), part (1): if $S = R[s]$ with $s$ integral over $R$, then $S$ is finitely generated as an $R$-module. Here $R = B_0$, $s = c$, $S = B_0[c]$. The hypotheses: - Ring extension $B_0 \subseteq B_0[c]$: yes, $B_0[c]$ is the $B_0$-subalgebra of $C$ generated by $c$. - $c$ is integral over $B_0$: just verified. Conclusion: $B_0[c]$ is finitely generated as a $B_0$-module. Explicitly, it is generated by $\{1, c, c^2, \ldots, c^{N-1}\}$. [/guided] [/step] [step:Apply transitivity of finite generation to conclude $B_0[c]$ is finitely generated over $A$] [claim:Tower of finite generation yields joint finite generation] If $A \subseteq B_0 \subseteq B_0[c]$ are ring extensions with $B_0$ finitely generated as an $A$-module and $B_0[c]$ finitely generated as a $B_0$-module, then $B_0[c]$ is finitely generated as an $A$-module. [/claim] [proof] Let $v_1, \ldots, v_p \in B_0$ generate $B_0$ as an $A$-module, and let $u_1, \ldots, u_m \in B_0[c]$ generate $B_0[c]$ as a $B_0$-module. We show the finite set \begin{align*} \{v_q u_r : 1 \leq q \leq p, \; 1 \leq r \leq m\} \end{align*} generates $B_0[c]$ as an $A$-module. Given $w \in B_0[c]$, write $w = \sum_{r=1}^m t_r u_r$ with $t_r \in B_0$; then expand each $t_r = \sum_{q=1}^p a_{r,q} v_q$ with $a_{r,q} \in A$. Substituting: \begin{align*} w = \sum_{r=1}^m \left( \sum_{q=1}^p a_{r,q} v_q \right) u_r = \sum_{q,r} a_{r,q} (v_q u_r), \end{align*} using associativity and commutativity in the commutative ring $B_0[c]$. This expresses $w$ as an $A$-linear combination of the $v_q u_r$. [/proof] Applying the claim with the finite generating sets from the previous two steps: $B_0[c]$ is finitely generated as an $A$-module. [guided] We have assembled two finite-generation facts: - $B_0$ is finitely generated as an $A$-module (from the $b_i$ being integral over $A$). - $B_0[c]$ is finitely generated as a $B_0$-module (from $c$ being integral over $B_0$). We now need: $B_0[c]$ is finitely generated as an $A$-module. This is the content of the claim — transitivity of finite generation along a tower of ring extensions. The argument (given in the proof of the claim) takes a $B_0$-generating set $\{u_1, \ldots, u_m\}$ for $B_0[c]$ and an $A$-generating set $\{v_1, \ldots, v_p\}$ for $B_0$, and shows that the $pm$ products $\{v_q u_r\}$ generate $B_0[c]$ as an $A$-module. Explicitly, any $w \in B_0[c]$ is a $B_0$-combination of the $u_r$, and each $B_0$-coefficient is an $A$-combination of the $v_q$; substituting and using associativity/commutativity in the commutative ring $B_0[c]$ gives $w$ as an $A$-combination of the products. So $B_0[c]$ is generated over $A$ by at most $Np$ elements, where $N = \deg f$ and $p$ is the number of $A$-generators of $B_0$. [/guided] [/step] [step:Apply [Finitely Generated Implies Integral](/theorems/1566) to conclude $c$ is integral over $A$] We apply [Finitely Generated Implies Integral](/theorems/1566) to the ring extension $A \subseteq B_0[c]$. The hypothesis requires: 1. **$B_0[c]$ is finitely generated as an $A$-module**: verified in the previous step. The theorem concludes that every element of $B_0[c]$ is integral over $A$; in particular $c \in B_0[c]$ is integral over $A$. Since $c \in C$ was arbitrary, every element of $C$ is integral over $A$. By definition, $C$ is integral over $A$. [guided] We have $B_0[c]$ finitely generated as an $A$-module. By [Finitely Generated Implies Integral](/theorems/1566), which says "if $S$ is finitely generated as an $R$-module, then $S$ is integral over $R$", every element of $B_0[c]$ is integral over $A$. In particular, $c \in B_0[c]$ is integral over $A$: there exists a monic polynomial $g \in A[x]$ with $g(c) = 0$. The determinant trick in [Finitely Generated Implies Integral](/theorems/1566) even gives us a degree bound: $\deg g \leq $ (number of $A$-generators of $B_0[c]$) $\leq Np$. Since $c \in C$ was arbitrary, every element of $C$ is integral over $A$: $C$ is integral over $A$. This completes the proof. A final remark: the entire proof has a satisfying structure. The obstacle to direct manipulation (coefficients of the polynomial for $c$ live in $B$, not $A$) is dissolved by passing to a **finitely generated** $A$-sub-algebra $B_0$ that captures exactly the finitely many coefficients needed. Finite generation propagates up the tower $A \subseteq B_0 \subseteq B_0[c]$, and then [Finitely Generated Implies Integral](/theorems/1566) closes the loop and produces the desired $A$-monic polynomial. The technique — "isolate finitely many elements of the witnessing data, then apply the module-theoretic equivalence" — is a recurring pattern in commutative algebra. [/guided] [/step]