 Upper semicontinuity of local fibre dimension

For a finite-type morphism of schemes, local fibre dimension is upper semicontinuous on the source, in the displayed sense. If the morphism is proper, the maximal fibre dimension is also upper semicontinuous on the target. Without properness a component of a large fibre can disappear from the source over a special point, so the target statement is not valid in that generality. The Stacks Project: dimension of fibres distinguishes these statements.