Flat closed immersion of finite presentation (source code)

= Flat closed immersion of finite presentation

A nonempty flat <closed immersion> of finite presentation into a connected <scheme> is an <isomorphism>. On a chart it is $A\to A/I$ with $I$ finitely generated. At a prime containing $I$, the quotient is a finite flat module over the <local ring>, hence free of rank one, so $I$ vanishes there. Finite generation extends this vanishing to a neighbourhood. Thus the image is open as well as closed; connectedness makes it all of the target, and the ideal is everywhere zero. Without finite presentation the conclusion can fail.