Finite morphisms survive base change and composition

Let $f:X\to S$ be finite and $g:T\to S$ any morphism; the fibre product $P=X{\times }_{S}T$ exists by [F4]. Index a family by all pairs $(U,W)$ where $U=\mathrm{Spec}A\subseteq S$ is affine, $W\subseteq T$ is affine open, and $g(W)\subseteq U$. These opens cover $T$: for each $t\in T$, an affine neighbourhood $U$ of $g(t)$ exists, and the open subscheme $g^{-1}(U)$ has an affine neighbourhood $W$ of $t$ by [F3]. Taking all such pairs makes no simultaneous pointwise choice.

Let $X\stackrel{f}{\to }Y\stackrel{g}{\to }S$ be finite, without assuming AC, and fix an arbitrary affine open $U=\mathrm{Spec}A\subseteq S$. By [F1], write $g^{-1}(U)=\mathrm{Spec}B$ with $B$ finite over $A$. This is an affine open of $Y$, so [F1] applied to $f$ gives $f^{-1}(g^{-1}(U))=\mathrm{Spec}C$ with $C$ finite over $B$. Fix finite module generating lists $b_1,\dots ,b_m$ for $B\mathrm{/}A$ and $c_1,\dots ,c_n$ for $C\mathrm{/}B$. The products $b_i{c}_j$ generate $C$ over $A$: for $c={\sum }_j{d}_j{c}_j$, write each $d_j={\sum }_i{a}_{ij}{b}_i$ to obtain $c={\sum }_{i,j}{a}_{ij}{b}_i{c}_j$. Thus the inverse image of every affine $U$ is affine and finite over $A$, so [F1] proves $g\circ f$ finite. Only two finite generating lists are fixed, with no choice from an arbitrary family.

Fix one pair from step 1.1, with $W=\mathrm{Spec}{A}^{\mathrm{\prime }}$ and $U=\mathrm{Spec}A$. By [F1], write $f^{-1}(U)=\mathrm{Spec}B$ with $B$ finite over $A$. The inverse image $P{\times }_{T}W$ identifies with $f^{-1}(U){\times }_{U}W$ by [F6], and hence with $\mathrm{Spec}(B{\otimes }_A{A}^{\mathrm{\prime }})$ by [F5]. If $b_1,\dots ,b_n$ generate $B$ as an $A$-module, then $b_1\otimes 1,\dots ,b_n\otimes 1$ generate $B{\otimes }_A{A}^{\mathrm{\prime }}$ as an $A^{\mathrm{\prime }}$-module, since if $b={\sum }_i{a}_i{b}_i$ with $a_i\in A$, then $b\otimes a^{\mathrm{\prime }}={\sum }_i(b_i\otimes 1)(1\otimes \rho (a_i)a^{\mathrm{\prime }})$, where $\rho :A\to A^{\mathrm{\prime }}$ is the base-change map, and every tensor is a finite sum of pure tensors. Thus the pullback over each $W$ is affine and finite.

The affine opens from step 1.1 cover $T$, and step 2.1 verifies the affine and module-finite conditions on every member. Assuming AC, the converse in [F2] therefore shows that $P\to T$ is finite. This is the only choice-dependent step in the base-change assertion.

If $T=\mathrm{\varnothing }$, then $P=\mathrm{\varnothing }$ and the base-changed map is finite. On an empty affine chart or a chart whose pullback is empty, the coordinate ring is $0$, generated as a module by the empty set; tensoring with the zero ring again gives zero. Identity maps are finite because their affine chart module is generated by $1$, and the composition argument includes identity factors. There is no endpoint parameter or iff claim. The base-change conclusion carries AC exactly as stated, while the composition proof is choice-free. [F1, F5, step 1.2, step 2.1, step 3.1] $\mathrm{\square }$