Norm detects proper closed subsets under finite normalization (source code)

= Norm detects proper closed subsets under finite normalization

For a finite integral inclusion $A=k[t_1,\ldots,t_r]\subset B$ of domains, a nonzero $b\in B$ has a monic <minimal polynomial> over the fraction field with nonzero constant term $a_0\in A$. Its equation gives $a_0\in bB\cap A$. Consequently the image of $V_B(b)$ under the <finite morphism> to $\mathbb A^r$ is contained in the proper <Zariski-closed set> $V_A(a_0)$. Finite morphisms preserve the dimension of a closed subvariety and its image, so this proves dimension drops for proper closed subsets after <Noether normalization>. A power of $a_0$, up to sign, is the <field norm> of $b$.