Closed-fibre lower bound by finite normalization (source code)

= Closed-fibre lower bound by finite normalization
{title2=$\dim X_y\ge\dim X-\dim Y$}

For a surjective morphism of irreducible varieties, choose an affine neighborhood of the target point and a finite <Noether normalization> to affine space of target dimension $r$. On an affine source neighborhood the composite fibre is cut out by $r$ functions, so repeated <principal hypersurface dimension lemma> gives dimension at least source dimension minus $r$ on every component. The normalization fibre is finite. The original fibre is therefore an open-and-closed union of components of that composite fibre, proving the bound without assuming target smoothness. For a reducible source the bound must instead be applied using the dimension of each source component.