Closed-point local dimension equals ambient irreducible dimension

Given: The objects and hypotheses in the statement, including the Axiom of Choice (The Axiom of Choice).

If $X$ is an irreducible classical variety, then $\dim X={\mathrm{trdeg}}_{k}k(X)<\mathrm{\infty }$. Work over a fixed algebraically closed field $k$, with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points. (Dimension equals transcendence degree).

For a nonempty irreducible closed subvariety $Z$ of an irreducible classical variety $X$, define ${\mathrm{codim}}_{X}Z=\dim X-\dim Z$. These are finite integers. In a reducible ambient variety a difference of global dimensions must not be substituted for the height of a local prime; the containing component matters. Work over a fixed algebraically closed field $k$, with the Axiom of Choice. Classical varieties are separated and admit finite affine covers; they may be reducible or empty unless irreducibility is specified. Irreducible means nonempty. All fibres and points below are classical closed-point fibres and points. (Codimension of an irreducible closed subvariety).

Assume the Axiom of Choice. Let $X$ be a classical affine variety over an algebraically closed field $k$, let $x\in X$, and let ${\mathfrak{m}}_x:=\{\bar{f}\in k[X]:\bar{f}(x)=0\}\mathrm{.}$ Then there is a canonical isomorphism of local rings ${\mathcal{O}}_{X,x}\stackrel{\sim }{\to }k[X{]}_{{\mathfrak{m}}_x}\mathrm{.}$ (The local ring at a point of an affine variety is the localization at its maximal ideal).

Under the Axiom of Choice, if $k$ is a field, $A$ is a finite-type $k$-domain, and $\mathfrak{p}\in \mathrm{Spec}(A)$, then $\mathrm{ht}(\mathfrak{p})+\dim (A\mathrm{/}\mathfrak{p})=\dim A$ (Height plus quotient dimension equals ambient dimension in an affine domain).

Let $R$ be a commutative ring and let $\mathfrak{p}\in \mathrm{Spec}(R)$. The height of $\mathfrak{p}$ is the Krull dimension of the local ring $R_{\mathfrak{p}}$: $\mathrm{ht}(\mathfrak{p})=\dim (R_{\mathfrak{p}})\mathrm{.}$ (The height of a prime ideal).