Closed-point dimension lemma for affine domains (source code)

= Closed-point dimension lemma for affine domains
{title2=$\dim A_{\mathfrak m}=\dim A$}

If $A$ is a finite-type <integral domain> over an <algebraically closed field> and $\dim A=d$, every <maximal ideal> $\mathfrak m$ has <height of a prime ideal> $d$. Choose a <Noether normalization> $k[z_1,\ldots,z_d]\subset A$. The contraction of $\mathfrak m$ is a <maximal ideal> of the <polynomial ring> and has height $d$; <going-down theorem> lifts its full chain since the <polynomial ring> is <integrally closed domain>. The upper bound is $\dim A$. A <principal open subset> containing a <closed point> consequently has dimension $d$, because the whole chain under that point survives <localization>.