Products preserve smoothness

Let $P=X{\times }_{k}Y$ be the scheme-theoretic product of finite-type $k$-schemes smooth over $k$. For affine neighbourhoods $\mathrm{Spec}A$ and $\mathrm{Spec}B$ of the projections of any point, [F3] gives the product chart $\mathrm{Spec}(A{\otimes }_{k}B)$. Finite generating lists for $A$ and $B$ generate $A{\otimes }_{k}B$, so $P$ is locally of finite type. Each factor has a finite affine cover because its structure morphism is quasi-compact; the resulting finite family of product charts covers $P$, so $P$ is quasi-compact. Thus [F10] makes $P$ finite type. Fix $z\in P$ and write $x,y$ for its projections. Smoothness and [F1] give affine neighbourhoods $U=\mathrm{Spec}A$ of $x$ and $V=\mathrm{Spec}B$ of $y$ where $k\to A$ and $k\to B$ are standard smooth at the corresponding primes; shrink by the principal opens witnessing the presentations. By [F3], $U{\times }_{k}V=\mathrm{Spec}(A{\otimes }_{k}B)$ is an open affine neighbourhood of $z$. The map $A\to A{\otimes }_{k}B$ is the base change of $k\to B$, so [F4] makes it standard smooth at the prime for $z$. Its composite with $k\to A$ is standard smooth there by [F5]. Hence $P\to \mathrm{Spec}k$ is locally standard smooth at $z$.

Suppose $X$ and $Y$ are nonempty. By [F7], write them as finite unions of irreducible components $X={\bigcup }_i{X}_i$ and $Y={\bigcup }_j{Y}_j$. A point of either factor is a morphism from the one-point affine variety. Given $x\in X$ and $y\in Y$, [F8] gives a unique point of the product whose projections are $x,y$; conversely, the projections of a product point determine it uniquely by the same universal property. Thus product points are pairs, and each $(x,y)$ belongs to some $X_i{\times }_k{Y}_j$, so these products cover $X{\times }_{k}Y$. Each product is closed as the intersection of the inverse images of the closed sets $X_i$ and $Y_j$ under the continuous projections [F15]; there are finitely many by [F7]. Each $X_i{\times }_k{Y}_j$ is irreducible by [F6]. Fix one point in each of the two nonempty factors; pairing that fixed point with an arbitrary point of the other factor shows that both product projections are surjective. If $X_i{\times }_k{Y}_j\subseteq X_{i^{\mathrm{\prime }}}{\times }_k{Y}_{j^{\mathrm{\prime }}}$, surjectivity gives $X_i\subseteq X_{i^{\mathrm{\prime }}}$ and $Y_j\subseteq Y_{j^{\mathrm{\prime }}}$, so maximality of the original components forces equality in both coordinates. Conversely, an irreducible closed subset of a finite union of closed sets lies in one member of that union, so every irreducible component of $X{\times }_{k}Y$ is one of these products. Applying [F6] to each irreducible pair gives $\dim (X_i{\times }_k{Y}_j)=\dim X_i+\dim Y_j$. If one factor is empty, the product and the component-pair list are empty by [F8].

Since $z$ was arbitrary, [F1] gives smoothness of $P$ over $k$. If either factor is empty, then $P$ is empty and smoothness is vacuous, proving the general finite-type-scheme claim. For the classical product, [F14] gives finite affine covers; each affine chart has a finite-type coordinate algebra by [F2], so [F10] makes its associated scheme finite type. Fix a product point $z$ with projections $x,y$, and choose affine neighbourhoods $U=\mathrm{Spec}A$ and $V=\mathrm{Spec}B$. The open set $p^{-1}(U)\cap q^{-1}(V)$ in the classical product is itself the classical product $U{\times }_{k}V$: a pair of maps into $U,V$ gives a unique map into the global product by [F6], and its image lies in this open set; uniqueness is inherited. By [F13] its coordinate ring is $A{\otimes }_{k}B$, so its associated affine scheme is the same chart as the scheme product chart supplied by [F3]. The principal-open restrictions agree because both invert $f\otimes 1$ and $1\otimes g$ on a product of $D(f)$ and $D(g)$; the resulting ring is $(A{\otimes }_{k}B{)}_{f\otimes 1,1\otimes g}$. Therefore the local chart calculation in step 1.1 applies at every classical product point, and [F1] gives smoothness.

The product with the zero-dimensional point $\mathrm{Spec}k$ is the other factor by [F8], and dimensions add as $0+d=d$; its map to $\mathrm{Spec}k$ has the zero-variable, zero-equation standard-smooth presentation allowed by [F11]. The one-dimensional example ${\mathbb{A}}_k^1{\times }_k{\mathbb{A}}_k^1={\mathbb{A}}_k^2$ has the standard-smooth presentation with two variables and no equations by [F11], and its component dimension is $1+1=2$ by [F6]. If a factor is the empty scheme $\mathrm{Spec}0$, its tensor-product chart is empty and no point requires a smoothness check [F3]. AC is propagated because the smooth-morphism convention [F1] and the classical component and dimension suppliers [F6, F7] are stated under AC [F9]; the pointwise standard-smooth argument makes no simultaneous chart choice. There is no interval endpoint, and neither smoothness preservation nor the component-dimension assertion is an iff.