A transverse hyperplane slice is smooth at the chosen point

Setup. The closed subvariety $X\subseteq {\mathbf{A}}_k^n$ is an affine model with its reduced finite-type structure and function sheaf [F2], and its coordinate ring $k[X]=k[x_1,\dots ,x_n]\mathrm{/}I(X)$ is reduced and generated as a $k$-algebra by the finitely many classes ${\bar{x}}_1,\dots ,{\bar{x}}_n$ [F3]. Its points have residue field $k$ [F2], so $x$ is a $k$-rational point. The variety $X$ is Noetherian with finitely many irreducible components [F23], and [F5] with [F4] gives $\dim {\mathcal{O}}_{X,x}={\max }_{x\in X_i}\dim X_i={\dim }_{x}X=d,$ the maximum being over the components containing $x$, a nonempty finite family. Smoothness of $X$ at $x$ means that the structure morphism $X\to \mathrm{Spec}k$ is locally standard smooth at $x$ [F6]; fix an affine chart $\mathrm{Spec}A$ containing $x$ on which $k\to A$ is standard smooth [F7], and write $\mathfrak{m}$ for the prime of $x$ in $A$, so that ${\mathcal{O}}_{X,x}\cong A_{\mathfrak{m}}$ [F9]. The subscheme $H=V(h)$ is cut out by the principal ideal $(h)\subseteq k[x_1,\dots ,x_n]$, and its defining equation vanishes at $x$: $h(x)=0$.

The differential of $h{\mathrm{\mid }}_X$. Write $f=h{\mathrm{\mid }}_X$. Every $v\in T_{x}X$ is represented by a based dual-number point $\gamma :D_k\to X$ at $x$ [F11]. Its composite ${\gamma }^{\mathrm{\prime }}=\iota \circ \gamma :D_k\to {\mathbf{A}}_k^n$ corresponds to a $k$-algebra map $k[X_1,\dots ,X_n]\to k[ϵ]\mathrm{/}({ϵ}^2)$ [F25]. By [F12] this map is uniquely determined by the images of the $X_i$. Since reduction modulo $ϵ$ gives the point $x=(x_1,\dots ,x_n)$, these images have the unique form $X_i\mapsto x_i+ϵw_i$ for $w=(w_1,\dots ,w_n)\in k^n$. Conversely every $w\in k^n$ gives such a based point by [F12], and the $k$-linear dual-number correspondence [F11] identifies $T_x{\mathbf{A}}_k^n$ with $k^n$ in these coordinates. Call $w$ the image of $v$ under $d_x\iota$. By [F13] the differential $d_{x}f(v)$ is represented by the composite $f\circ \gamma$, and substituting ${\gamma }^{\mathrm{\prime }}$ in the affine-linear form $h=\mathrm{\ell }-c$ gives $h(x+ϵw)=h(x)+ϵ\mathrm{\ell }(w)=ϵ\mathrm{\ell }(w),$ because $h(x)=0$ and $\mathrm{\ell }$ is $k$-linear. Hence $d_{x}f(v)=\mathrm{\ell }(w)$, that is, $d_{x}f=\mathrm{\ell }\circ d_x\iota$ and $d{h}_x=\mathrm{\ell }$; the transversality hypothesis is therefore exactly the condition $d_{x}f\mathrm{\ne }0$. Taking $n=1$ in the same calculation gives $T_0{\mathbf{A}}_k^1=k$, which is one-dimensional, and $T_{x}X$ is finite-dimensional [F10]. Thus a nonzero $d_{x}f$ is surjective, and by [F13] the induced cotangent map ${\mathfrak{m}}_0\mathrm{/}{\mathfrak{m}}_0^2\to {\mathfrak{m}}_x\mathrm{/}{\mathfrak{m}}_x^2$ is its dual, hence injective.

The morphism $f$ is of finite type. The affine model $X$ has coordinate ring $k[X]=k[x_1,\dots ,x_n]\mathrm{/}I(X)$, generated as a $k$-algebra by the finitely many classes ${\bar{x}}_1,\dots ,{\bar{x}}_n$ [F3], and the affine line ${\mathbf{A}}_k^1$ has coordinate ring $k[t]$ [F24]; by [F25] the $k$-morphism $f=h{\mathrm{\mid }}_X$ from the affine chart $X$ to ${\mathbf{A}}_k^1$ corresponds to the $k$-algebra map $k[t]\to k[X]$ sending $t$ to the class $\bar{h}$ of $h$, the pullback of the coordinate function. This ring map is of finite type: the same finite family generates $k[X]$ over $k$ [F3], hence over $k[t]$ [F22]. By [F26] finiteness of type may be tested over each affine target open on a finite affine source cover; the target $\mathrm{Spec}k[t]={\mathbf{A}}_k^1$ is affine and the single chart $X$ is such a cover, so $f$ is of finite type.

Regularity of $X$ at $x$ and of the affine line at the origin. The coordinate ring $A$ of the chart of step 1.1 is a finitely generated $k$-algebra [F3], hence a Noetherian ring by [F28] because $k$ is a field and therefore Noetherian; so $\mathrm{Spec}A$ is locally Noetherian [F29]. Applying clause 1 of [F8] to the standard smooth presentation of step 1.1 with $R=k$, $\mathfrak{p}=(0)$ and $K=k$ shows that every local ring of that chart, in particular ${\mathcal{O}}_{X,x}=A_{\mathfrak{m}}$, is a regular local ring; by [F10] therefore ${\dim }_k{T}_{x}X=\dim {\mathcal{O}}_{X,x}=d$, so $T_{x}X\mathrm{\ne }0$ because $d\ge 1$. The affine line has coordinate ring $k[t]$ and local ring $k[t{]}_{(t)}$ at the origin with residue field $k$ [F24], and $k\to k[t]$ is standard smooth with one variable and no equation [F7]; hence ${\mathbf{A}}_k^1\to \mathrm{Spec}k$ is locally standard smooth at $0$ [F6] and ${\mathcal{O}}_{{\mathbf{A}}_k^1,0}$ is a regular local ring [F8]. The affine line is irreducible with $\dim {\mathbf{A}}_k^1=1$ [F27], so [F5] with [F4] gives $\dim {\mathcal{O}}_{{\mathbf{A}}_k^1,0}={\dim }_0{\mathbf{A}}_k^1=1$. [F3, F4, F5, F6, F7, F8, F10, F24, F27, F28, F29, step 1.1, given, algebra] 2.2 The slice is the fibre. First, $H=V(h)$ is the fibre of $h$ over the origin: the fibre product of $h:{\mathbf{A}}_k^n\to {\mathbf{A}}_k^1$ and the point $0:\mathrm{Spec}k\to {\mathbf{A}}_k^1$ is $\mathrm{Spec}(k[x_1,\dots ,x_n]{\otimes }_{k[t]}k)$ with the projections of [F17], and [F18] identifies $k[x_1,\dots ,x_n]{\otimes }_{k[t]}k\cong k[x_1,\dots ,x_n]\mathrm{/}(h)$, where $k[x_1,\dots ,x_n]$ is a $k[t]$-algebra through $t\mapsto h$, the ideal $IM$ is generated by $h$ for $I=(t)$ and $M=k[x_1,\dots ,x_n]$, and the isomorphism is one of $k$-algebras; hence $H=\mathrm{Spec}(k[x_1,\dots ,x_n]\mathrm{/}(h))$ is this fibre, with projections $\pi :H\to {\mathbf{A}}_k^n$ and $\rho :H\to \mathrm{Spec}k$ satisfying $h\circ \pi =(0)\circ \rho$ [F16]. Second, $Z=X{\times }_{{\mathbf{A}}_k^n}H$ is the scheme-theoretic intersection of the closed subschemes $X$ and $H$ of affine space, with projections ${\pi }_X:Z\to X$, ${\pi }_H:Z\to H$ satisfying $\iota \circ {\pi }_X=\pi \circ {\pi }_H$ [F15]. Third, the fibre $X_0=X{\times }_{{\mathbf{A}}_k^1}\mathrm{Spec}k$ of $f$ over $0$ has projections $p:X_0\to X$, $q:X_0\to \mathrm{Spec}k$ satisfying $f\circ p=(0)\circ q$ [F14]. All three fibre products exist, and a morphism into any of them is determined by its projections [F16]. The morphisms $\iota \circ p$ and $q$ have equal composites to ${\mathbf{A}}_k^1$, namely $h\circ \iota \circ p=f\circ p=(0)\circ q$, so the universal property of $H$ gives a unique ${\theta }_H:X_0\to H$ with $\pi \circ {\theta }_H=\iota \circ p$ and $\rho \circ {\theta }_H=q$; since $\iota \circ p=\pi \circ {\theta }_H$, the pair $(p,{\theta }_H)$ induces a unique $\theta :X_0\to Z$ with ${\pi }_X\circ \theta =p$ and ${\pi }_H\circ \theta ={\theta }_H$. Conversely the morphisms ${\pi }_X$ and $\rho \circ {\pi }_H$ have equal composites to ${\mathbf{A}}_k^1$, namely $f\circ {\pi }_X=h\circ \iota \circ {\pi }_X=h\circ \pi \circ {\pi }_H=(0)\circ \rho \circ {\pi }_H$, so the universal property of $X_0$ gives a unique $\psi :Z\to X_0$ with $p\circ \psi ={\pi }_X$ and $q\circ \psi =\rho \circ {\pi }_H$. By the uniqueness clauses $\psi \circ \theta ={\mathrm{id}}_{X_0}$ and $\theta \circ \psi ={\mathrm{id}}_Z$: both composites induce the same projections, and a morphism into $H$ is determined by its composites with $\pi$ and $\rho$. Hence $\theta$ is a canonical isomorphism $X_0\to Z$ over $X$ and over $\mathrm{Spec}k$. The $k$-point $x:\mathrm{Spec}k\to X$ satisfies $f\circ x=(0)\circ (\text{structure map})$ because $h(x)=0$, so it induces a $k$-point of $X_0$, carried by $\theta$ to a $k$-point of $Z$ mapping to $x$; this is the point at which all local statements are taken. Finally the tangent space. A $k$-morphism $D_k\to X_0$ is by the universal property a pair $(\gamma ,\delta )$ with $\gamma :D_k\to X$ and $\delta :D_k\to \mathrm{Spec}k$ such that $f\circ \gamma =(0)\circ \delta$ [F16]; the morphism $\delta$ is unique, and being based at $x$ means that $\gamma$ is based at $x$ and $\delta$ is the structure morphism. Hence based dual-number points of $X_0$ at $x$ correspond bijectively to based dual-number points $\gamma :D_k\to X$ of $X$ at $x$ whose composite $f\circ \gamma$ is the constant point at $0$. Under the identifications of [F11] this correspondence is $k$-linear and identifies $T_x{X}_0$ with $\ker (d_{x}f)$: by [F13], $d_{x}f(v)$ is represented by $f\circ \gamma$, and the constant point at $0$ represents the zero vector of $T_0{\mathbf{A}}_k^1$ [F12]. Since $\theta$ is an isomorphism, its differential at $x$ is an isomorphism [F13], so $T_{x}Z=\ker (d_{x}f)\mathrm{.}$

The submersion criterion. Take $Y={\mathbf{A}}_k^1$ and $y=0=f(x)$: the point $y$ has residue field $k$ [F24], and both $x$ and $y$ are $k$-rational [step 1.1]. The schemes $X$ and $Y$ are locally standard smooth over $k$ at $x$ and $y$ [step 1.1, step 2.1], the morphism $f$ is of finite type [step 1.3], and the cotangent map ${\mathfrak{m}}_y\mathrm{/}{\mathfrak{m}}_y^2\to {\mathfrak{m}}_x\mathrm{/}{\mathfrak{m}}_x^2$ of [F20] is injective by [step 1.2]. Clause 1 of [F20] therefore makes $f$ locally standard smooth at $x$, that is, smooth at $x$ in the sense of [F6]. [F6, F20, F24, step 1.1, step 2.1, step 1.2, step 1.3, given, algebra] 4.1 Dimension of the slice. By step 3.1, clause 2 of [F20] applies at $x$ with $S={\mathcal{O}}_{X,x}$, $A={\mathcal{O}}_{{\mathbf{A}}_k^1,0}$, $m=\dim S=\dim {\mathcal{O}}_{X,x}=d$ [step 1.1] and $n=\dim A=\dim {\mathcal{O}}_{{\mathbf{A}}_k^1,0}=1$ [step 2.1]; it makes the local ring $S\mathrm{/}{\mathfrak{m}}_{y}S={\mathcal{O}}_{X_0,x}$ of the fibre at $x$ a regular local ring of dimension $m-n=d-1$. By step 2.2, ${\mathcal{O}}_{Z,x}\cong {\mathcal{O}}_{X_0,x}$, so ${\mathcal{O}}_{Z,x}$ is a regular local ring of dimension $d-1$ in the sense of [F21]. Consistently, rank-nullity for the surjective differential [step 1.2] gives ${\dim }_k\ker (d_{x}f)={\dim }_k{T}_{x}X-1=d-1$ [step 2.1], and ${\dim }_k{T}_{x}Z={\dim }_k\ker (d_{x}f)$ by step 2.2, so the tangent dimension of the slice agrees with the local dimension. [F20, F21, step 2.1, step 1.2, step 3.1, step 2.2, given, algebra] 5.1 Smoothness of the slice and conclusion. Since $f$ is smooth at $x$ [step 3.1] and $Z\cong X_0$ is the base change of $f$ along the point $0:\mathrm{Spec}k\to {\mathbf{A}}_k^1$ [step 2.2], clause 1 of [F19] makes $Z\to \mathrm{Spec}k$ locally standard smooth at $x$, so the slice is smooth at $x$ [F6]. Together with steps 3.1, 2.2 and 4.1 this proves the assertions of the statement, including $T_{x}Z=\ker (d_x(h{\mathrm{\mid }}_X))$ and its description as the set of $v\in T_{x}X$ with $d_x(h{\mathrm{\mid }}_X)(v)=0$. Boundaries. The hypothesis $d\ge 1$ guards against vacuity: if $d=0$ then ${\dim }_k{T}_{x}X=d=0$ [step 2.1], so $T_{x}X$ carries no nonzero linear functional and the transversality hypothesis fails. For $d=1$ the conclusion gives $\dim {\mathcal{O}}_{Z,x}=0$ [step 4.1], so the slice is isolated at $x$ in the local sense. The ambient endpoint $n=1$ forces $d\le 1$, hence $d=1$ and the same zero-dimensional conclusion. For $X={\mathbf{A}}_k^n$ the inclusion is the identity, the slice $Z\cong H$ is the hyperplane itself (the projection $Z\to H$ is an isomorphism by the universal property [F16] applied to ${\mathrm{id}}_{{\mathbf{A}}_k^n}$), the transversality condition is exactly $\mathrm{\ell }\mathrm{\ne }0$, and step 2.2 gives $T_{x}Z=\ker (\mathrm{\ell })$. No characteristic hypothesis is used: the argument never divides by an integer, so all characteristics are covered. The variety $X$ may be reducible, and nothing is asserted in the nontransverse case where $\mathrm{\ell }$ vanishes on $T_{x}X$. AC enters the statement through [F1] and is used only through the suppliers that assume it, namely [F5], [F6], [F8], [F20], [F23] and [F24], each cited at the step that uses it; the affine chart, its presentation, the polynomial $h$ and the point $x$ are single given objects, so no further selection is made and [F13], [F15], [F16] and [F18] are choice-free.