Dan Edidin points out that Proposition 2.10
is a weak version of one of Chevalley's theorems.
"In particular it holds with the assumption
that the map \pi is finite and surjective (no flatness or
condition on the degree required). I couldn't find
the statement in EGA, but it does appear (for maps
of an affine scheme to a separated algebraic space)
in Knutson's book Algebraic Spaces (Chapter III, Theorem 4.1). The proof
is fairly straightforward Noetherian induction using the
fact that the hypothesis ensures that \pi_*O_Y = O_X^n
on a small enough open set.
Speaking of algebraic spaces, it seems that your definition
makes sense for algebraic spaces, though it's not clear
if the extension any use."
---
Burt Totaro points out they we made a foolish mistake; we haven't
actually shown that our proper integral variety (announced in the
abstract) doesn't embed in a smooth algebraic space; we've only
shown that it doesn't embed in a smooth scheme.
Thanks Burt and Dan!