Isolated fibre point forces dominance in equal dimensions (source code)

= Isolated fibre point forces dominance in equal dimensions

Let $f:X\to Y$ be a <proper morphism> of irreducible <algebraic varieties> with equal dimension. If some fibre has an isolated point, its corresponding irreducible component has dimension zero. Apply the <fiber dimension theorem> to $X\to f(X)$: $0\ge\dim X-\dim f(X)$. Thus the closed image has dimension $\dim Y$ and equals $Y$. The <incidence proof that a cubic surface contains a line> is an application; the entire witness fibre need not be finite.